Four-dimensional Seiberg–Witten theory

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremTauCeti.SeibergWitten.hasStrictFDerivAt_quadraticEnd#

The real Fréchet derivative of Q₀ at ψ is B(ψ, ·), that is DQ₀|_ψ (φ) = φψ* + ψφ* - Re⟪ψ, φ⟫ Id; this holds in the strict sense.

TauCeti.SeibergWitten.hasStrictFDerivAt_quadraticEnd.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℂ E] (ψ : E) :
  HasStrictFDerivAt TauCeti.SeibergWitten.quadraticEnd (TauCeti.SeibergWitten.quadraticEndPolar ψ) ψ
Lean

Formalized in Tau Ceti as TauCeti.SeibergWitten.hasStrictFDerivAt_quadraticEnd.

Sources
LeanTauCeti.SeibergWitten.hasStrictFDerivAt_quadraticEnd

TheoremTauCeti.SeibergWitten.trace_quadraticEndPolar_mul_of_mem_traceFreeSelfAdjoint#

Against a trace-free self-adjoint T, the polarization of Q₀ pairs as tr (B(ψ, φ) T) = 2 Re⟪T ψ, φ⟫: the formal adjoint of the derivative B(ψ, ·) of Q₀ is T ↦ 2 T ψ.

TauCeti.SeibergWitten.trace_quadraticEndPolar_mul_of_mem_traceFreeSelfAdjoint.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [CompleteSpace E]
  {T : E →L[ℂ] E} (hT : T ∈ TauCeti.traceFreeSelfAdjoint E) (ψ φ : E) :
  (LinearMap.trace ℂ E) (↑((TauCeti.SeibergWitten.quadraticEndPolar ψ) φ) * ↑T) =
    2 * ↑(inner ℂ (T ψ) φ).re
Lean

Formalized in Tau Ceti as TauCeti.SeibergWitten.trace_quadraticEndPolar_mul_of_mem_traceFreeSelfAdjoint.

Sources
LeanTauCeti.SeibergWitten.trace_quadraticEndPolar_mul_of_mem_traceFreeSelfAdjoint
Uses 1
Statement usesTauCeti.traceFreeSelfAdjoint

TheoremFrame independence of the chirality element#

Γ = -c(e₁) c(e₂) c(e₃) c(e₄) for every positively oriented orthonormal basis e.

CliffordAlgebra.chirality_eq.{u_1} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  {Q : QuadraticForm ℝ V} [Fact (Module.finrank ℝ V = 4)] (o : Orientation ℝ V (Fin 4))
  (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (b : OrthonormalBasis (Fin 4) ℝ V)
  (hb : b.toBasis.orientation = o) :
  CliffordAlgebra.chirality Q o =
    -((CliffordAlgebra.ι Q) (b 0) * (CliffordAlgebra.ι Q) (b 1) * (CliffordAlgebra.ι Q) (b 2) *
        (CliffordAlgebra.ι Q) (b 3))
Lean

Formalized in Tau Ceti as CliffordAlgebra.chirality_eq.

Sources
LeanCliffordAlgebra.chirality_eq

TheoremThe self-duality relation#

the Clifford action of the Hodge dual of a two-form is the chirality element times the action of the two-form, c₂(⋆α) = Γ c₂(α).

CliffordAlgebra.bivectorExterior_hodgeStar.{u_1} {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} [Fact (Module.finrank ℝ V = 4)]
  (o : Orientation ℝ V (Fin 4)) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (hkl : 2 + 2 = Module.finrank ℝ V)
  (x : ↥(⋀[ℝ]^2 V)) :
  (CliffordAlgebra.bivectorExterior Q) ((o.hodgeStar hkl) x) =
    CliffordAlgebra.chirality Q o * (CliffordAlgebra.bivectorExterior Q) x
Lean

Formalized in Tau Ceti as CliffordAlgebra.bivectorExterior_hodgeStar.

Sources
LeanCliffordAlgebra.bivectorExterior_hodgeStar
Uses 1
Statement usesOrientation.hodgeStar

TheoremThe anticommutator of two two-forms in the Clifford algebra of an oriented four-space#

c₂(α) c₂(β) + c₂(β) c₂(α) = -2 ⟪α, β⟫ - 2 ⟪⋆α, β⟫ Γ. Since α ∧ β = ⟪⋆α, β⟫ vol, the coefficient of Γ is minus twice the volume of α ∧ β.

CliffordAlgebra.bivectorExterior_mul_bivectorExterior_add_swap.{u_1} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V}
  [Fact (Module.finrank ℝ V = 4)] (o : Orientation ℝ V (Fin 4)) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2)
  (hkl : 2 + 2 = Module.finrank ℝ V) (x y : ↥(⋀[ℝ]^2 V)) :
  (CliffordAlgebra.bivectorExterior Q) x * (CliffordAlgebra.bivectorExterior Q) y +
      (CliffordAlgebra.bivectorExterior Q) y * (CliffordAlgebra.bivectorExterior Q) x =
    (algebraMap ℝ (CliffordAlgebra Q)) (-2 * inner ℝ x y) -
      (2 * inner ℝ ((o.hodgeStar hkl) x) y) • CliffordAlgebra.chirality Q o
Lean

Formalized in Tau Ceti as CliffordAlgebra.bivectorExterior_mul_bivectorExterior_add_swap.

Sources
LeanCliffordAlgebra.bivectorExterior_mul_bivectorExterior_add_swap
Uses 1
Statement usesOrientation.hodgeStar

DefinitionOrientation.hodgeStar#

The Hodge star ⋀ᵏ V ≃ ⋀ˡ V, k + l = finrank ℝ V, of an oriented real inner product space: Mathlib's exteriorPower.hodgeStar for the inner product and Orientation.volumeEquiv. It is characterized by ⟪⋆x, y⟫ = vol (x ∧ y) (Orientation.inner_hodgeStar_apply).

Orientation.hodgeStar.{u_1} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n))
  {k l : ℕ} (hkl : k + l = Module.finrank ℝ V) : ↥(⋀[ℝ]^k V) ≃ₗ[ℝ] ↥(⋀[ℝ]^l V)
Lean

Formalized in Tau Ceti as Orientation.hodgeStar.

Sources
LeanOrientation.hodgeStar
Used by 3
Used byThe anticommutator of two two-forms in the Clifford algebra of an oriented four-space · The self-duality relation · Green's formula for d*d

DefinitionTauCeti.traceFreeSelfAdjoint#

The real subspace {T : T* = T, tr T = 0} of trace-free self-adjoint endomorphisms of a complex inner product space.

TauCeti.traceFreeSelfAdjoint.{u_1} (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℂ E]
  [CompleteSpace E] : Submodule ℝ (E →L[ℂ] E)
Lean

Formalized in Tau Ceti as TauCeti.traceFreeSelfAdjoint.

Sources
LeanTauCeti.traceFreeSelfAdjoint
Used by 1
Used byTauCeti.SeibergWitten.trace_quadraticEndPolar_mul_of_mem_traceFreeSelfAdjoint

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.