Clifford bundles, spin structures, and Dirac geometry

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

DefinitionCliffordAlgebra.spinGroupEquivNeg#

The Spin groups of Q and -Q are isomorphic, through Mathlib's identification evenEquivEvenNeg of their even Clifford algebras. A product of two vectors ι Q a * ι Q b goes to -(ι (-Q) a * ι (-Q) b), and the vector actions agree.

CliffordAlgebra.spinGroupEquivNeg.{u, v} {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M]
  [_root_.Module R M] (Q : QuadraticForm R M) [Invertible 2] : ↥(spinGroup Q) ≃* ↥(spinGroup (-Q))

Lean

Formalized in Tau Ceti as CliffordAlgebra.spinGroupEquivNeg.

Sources

• Tau Ceti documentation: CliffordAlgebra.spinGroupEquivNeg
• Source of CliffordAlgebra.spinGroupEquivNeg in TauCeti/LinearAlgebra/CliffordAlgebra/Spin/Neg.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanCliffordAlgebra.spinGroupEquivNeg

Used by 1

Used byCliffordAlgebra.realCliffordSpinGroupEquivNeg

DefinitionCliffordAlgebra.realCliffordSpinGroupEquivNeg#

The Spin group of signature (p, q), transported into the Clifford algebra of the negated signature (q, p). For p = n and q = 0 this is the compact Spin group Spin(n) in the Clifford algebra of the negative-definite coordinate form realCliffordForm 0 n.

CliffordAlgebra.realCliffordSpinGroupEquivNeg (p q : ℕ) :
  ↥(CliffordAlgebra.realCliffordSpinGroup p q) ≃* ↥(CliffordAlgebra.realCliffordSpinGroup q p)

Lean

Formalized in Tau Ceti as CliffordAlgebra.realCliffordSpinGroupEquivNeg.

Sources

• Tau Ceti documentation: CliffordAlgebra.realCliffordSpinGroupEquivNeg
• Source of CliffordAlgebra.realCliffordSpinGroupEquivNeg in TauCeti/LinearAlgebra/CliffordAlgebra/Spin/Real/Neg.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanCliffordAlgebra.realCliffordSpinGroupEquivNeg

Uses 1

Statement usesCliffordAlgebra.spinGroupEquivNeg

TheoremThe degree scaling by √2 intertwines the native and the normalized Fock actions#

T ∘ spinAction a = fockAction a ∘ T, where T multiplies ⋀^p W by √2 ^ p (TauCeti.ExteriorAlgebra.degreeScaling_of_mem_exteriorPower).

TauCeti.AlmostComplexStructure.degreeScaling_comp_spinAction_eq_fockAction_comp.{u} {V : Type u}
  [AddCommGroup V] [_root_.Module ℝ V] (J : TauCeti.AlmostComplexStructure V)
  {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v)
  (hQ : QuadraticMap.Nondegenerate) {r : ℂˣ} (hr : ↑r = ↑√2)
  (a : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) :
  (TauCeti.ExteriorAlgebra.degreeScaling r).toLinearMap ∘ₗ
      (TauCeti.spinAction (QuadraticForm.baseChange ℂ Q) (J.spinPolarizationData hQJ hQ)) a =
    (J.fockAction hQJ hQ) a ∘ₗ (TauCeti.ExteriorAlgebra.degreeScaling r).toLinearMap

Lean

Formalized in Tau Ceti as TauCeti.AlmostComplexStructure.degreeScaling_comp_spinAction_eq_fockAction_comp.

Sources

• Tau Ceti documentation: TauCeti.AlmostComplexStructure.degreeScaling_comp_spinAction_eq_fockAction_comp
• Source of TauCeti.AlmostComplexStructure.degreeScaling_comp_spinAction_eq_fockAction_comp in TauCeti/RepresentationTheory/Spin/Polarization/Fock/Basic.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanTauCeti.AlmostComplexStructure.degreeScaling_comp_spinAction_eq_fockAction_comp

Uses 1

Statement usesThe polarization of a complexified quadratic space by a complex structure

TheoremThe normalized Fock action of a real vector#

c(v) is √2 times exterior multiplication by v^(1,0) plus √2 / 2 times contraction against QuadraticMap.polar (Q.baseChange ℂ) · v^(0,1). In the geometric convention Q (v) = -g (v, v) that contraction is -2 ι(v^(0,1)) for the contraction ι against g_ℂ, so this is c(v) = √2 (ε(v^(1,0)) - ι(v^(0,1))).

TauCeti.AlmostComplexStructure.fockAction_ι_one_tmul.{u} {V : Type u} [AddCommGroup V]
  [_root_.Module ℝ V] (J : TauCeti.AlmostComplexStructure V) {Q : QuadraticForm ℝ V}
  [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v)
  (hQ : QuadraticMap.Nondegenerate) (v : V) :
  (J.fockAction hQJ hQ) ((CliffordAlgebra.ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] v)) =
    ↑√2 •
      ((J.spinPolarizationData hQJ hQ).wedge ⟨J.holomorphicPart v, ⋯⟩ +
        2⁻¹ • (J.spinPolarizationData hQJ hQ).contract ⟨J.antiholomorphicPart v, ⋯⟩)

Lean

Formalized in Tau Ceti as TauCeti.AlmostComplexStructure.fockAction_ι_one_tmul.

Sources

• Tau Ceti documentation: TauCeti.AlmostComplexStructure.fockAction_ι_one_tmul
• Source of TauCeti.AlmostComplexStructure.fockAction_ι_one_tmul in TauCeti/RepresentationTheory/Spin/Polarization/Fock/Basic.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanTauCeti.AlmostComplexStructure.fockAction_ι_one_tmul

Uses 1

Statement usesThe polarization of a complexified quadratic space by a complex structure

DefinitionEvery module over A ≅ End_k S is S tensored with its multiplicity space#

Evaluation s ⊗ T ↦ T s is an isomorphism of A-modules S ⊗[k] (S →ₗ[A] M) ≃ₗ[A] M, with A acting on the left factor.

TauCeti.isotypicTensorEquivOfBijective.{u_1, u_2, u_3, u_4} {k : Type u_1} {A : Type u_2}
  {S : Type u_3} {M : Type u_4} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S]
  [_root_.Module k S] [_root_.Module A S] [IsScalarTower k A S] [AddCommMonoid M]
  [_root_.Module k M] [_root_.Module A M] [IsScalarTower k A M]
  (h : Function.Bijective ⇑(Algebra.lsmul k k S)) [Module.Finite k S] [Module.Projective k S] :
  TensorProduct k S (S →ₗ[A] M) ≃ₗ[A] M

Lean

Formalized in Tau Ceti as TauCeti.isotypicTensorEquivOfBijective.

Sources

• Tau Ceti documentation: TauCeti.isotypicTensorEquivOfBijective
• Source of TauCeti.isotypicTensorEquivOfBijective in TauCeti/RingTheory/Morita/ModuleEnd.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanTauCeti.isotypicTensorEquivOfBijective

TheoremThe scalar part is the normalized regular trace#

over a field in which 2 is invertible, for every quadratic form on a finite-dimensional space, trace (x * ·) = 2 ^ finrank K V * scalarTrace Q x. Every such form has an orthogonal basis, so CliffordAlgebra.trace_mulLeft_eq_finrank_mul_scalarTrace applies.

CliffordAlgebra.trace_mulLeft_eq_two_pow_mul_scalarTrace.{u, v} {K : Type u} {V : Type v} [Field K]
  [AddCommGroup V] [_root_.Module K V] [Invertible 2] [FiniteDimensional K V]
  {Q : QuadraticForm K V} (x : CliffordAlgebra Q) :
  (LinearMap.trace K (CliffordAlgebra Q)) (LinearMap.mulLeft K x) =
    2 ^ Module.finrank K V * (CliffordAlgebra.scalarTrace Q) x

Lean

Formalized in Tau Ceti as CliffordAlgebra.trace_mulLeft_eq_two_pow_mul_scalarTrace.

Sources

• Tau Ceti documentation: CliffordAlgebra.trace_mulLeft_eq_two_pow_mul_scalarTrace
• Source of CliffordAlgebra.trace_mulLeft_eq_two_pow_mul_scalarTrace in TauCeti/LinearAlgebra/CliffordAlgebra/ScalarTrace/Basic.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanCliffordAlgebra.trace_mulLeft_eq_two_pow_mul_scalarTrace

Uses 1

Statement usesCliffordAlgebra.scalarTrace

TheoremPositivity of the trace pairing#

if Q is nonnegative on an orthogonal basis, then τ (reverse x * x) ≥ 0 for every x.

CliffordAlgebra.scalarTrace_reverse_mul_self_nonneg.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2}
  [CommRing R] [AddCommGroup M] [_root_.Module R M] [Invertible 2] {Q : QuadraticForm R M}
  {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} [LinearOrder R] [IsOrderedRing R]
  (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (hQ : ∀ (i : I), 0 ≤ Q (b i))
  (x : CliffordAlgebra Q) : 0 ≤ (CliffordAlgebra.scalarTrace Q) (CliffordAlgebra.reverse x * x)

Lean

Formalized in Tau Ceti as CliffordAlgebra.scalarTrace_reverse_mul_self_nonneg.

Sources

• Tau Ceti documentation: CliffordAlgebra.scalarTrace_reverse_mul_self_nonneg
• Source of CliffordAlgebra.scalarTrace_reverse_mul_self_nonneg in TauCeti/LinearAlgebra/CliffordAlgebra/OrthogonalBasis.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanCliffordAlgebra.scalarTrace_reverse_mul_self_nonneg

Uses 1

Statement usesCliffordAlgebra.scalarTrace

TheoremFaithfulness of the trace pairing#

if Q is positive on an orthogonal basis, then τ (reverse x * x) = 0 only for x = 0.

CliffordAlgebra.scalarTrace_reverse_mul_self_eq_zero_iff.{u_1, u_2, u_3} {R : Type u_1}
  {M : Type u_2} [CommRing R] [AddCommGroup M] [_root_.Module R M] [Invertible 2]
  {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} [LinearOrder R]
  [IsStrictOrderedRing R] (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b)
  (hQ : ∀ (i : I), 0 < Q (b i)) {x : CliffordAlgebra Q} :
  (CliffordAlgebra.scalarTrace Q) (CliffordAlgebra.reverse x * x) = 0 ↔ x = 0

Lean

Formalized in Tau Ceti as CliffordAlgebra.scalarTrace_reverse_mul_self_eq_zero_iff.

Sources

• Tau Ceti documentation: CliffordAlgebra.scalarTrace_reverse_mul_self_eq_zero_iff
• Source of CliffordAlgebra.scalarTrace_reverse_mul_self_eq_zero_iff in TauCeti/LinearAlgebra/CliffordAlgebra/OrthogonalBasis.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanCliffordAlgebra.scalarTrace_reverse_mul_self_eq_zero_iff

Uses 1

Statement usesCliffordAlgebra.scalarTrace

DefinitionThe polarization of a complexified quadratic space by a complex structure#

For a nondegenerate quadratic form Q on a finite-dimensional real vector space and an almost complex structure J preserving Q, the i- and -i-eigenspaces of the complexification of J are the two isotropic summands of a polarization of Q.baseChange ℂ, with no orthogonal remainder. Its pairing field identifies the -i-eigenspace with the dual of the i-eigenspace through the polar form.

TauCeti.AlmostComplexStructure.spinPolarizationData.{u} {V : Type u} [AddCommGroup V]
  [_root_.Module ℝ V] (J : TauCeti.AlmostComplexStructure V) {Q : QuadraticForm ℝ V}
  [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v)
  (hQ : QuadraticMap.Nondegenerate) : TauCeti.SpinPolarizationData (QuadraticForm.baseChange ℂ Q)

Lean

Formalized in Tau Ceti as TauCeti.AlmostComplexStructure.spinPolarizationData.

Sources

• Tau Ceti documentation: TauCeti.AlmostComplexStructure.spinPolarizationData
• Source of TauCeti.AlmostComplexStructure.spinPolarizationData in TauCeti/RepresentationTheory/Spin/Polarization/ComplexStructure.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanTauCeti.AlmostComplexStructure.spinPolarizationData

Used by 2

Used byThe degree scaling by √2 intertwines the native and the normalized Fock actions · The normalized Fock action of a real vector

DefinitionThe sesquilinear complexification of a real bilinear form B#

the form h (x, y) = B_ℂ (conj x, y) on ℂ ⊗[ℝ] V, conjugate-linear in the first argument and linear in the second, with h (z ⊗ v, w ⊗ u) = conj z * w * B (v, u) (LinearMap.BilinForm.sesqComplexification_tmul_tmul). For a Euclidean metric it is the induced positive Hermitian form on the complexification.

LinearMap.BilinForm.sesqComplexification.{u_1} {V : Type u_1} [AddCommGroup V] [_root_.Module ℝ V]
  (B : LinearMap.BilinForm ℝ V) : TensorProduct ℝ ℂ V →ₗ⋆[ℂ] TensorProduct ℝ ℂ V →ₗ[ℂ] ℂ

Lean

Formalized in Tau Ceti as LinearMap.BilinForm.sesqComplexification.

Sources

• Tau Ceti documentation: LinearMap.BilinForm.sesqComplexification
• Source of LinearMap.BilinForm.sesqComplexification in TauCeti/LinearAlgebra/BilinearForm/Complexification.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanLinearMap.BilinForm.sesqComplexification

Used by 1

Used byThe Hermitian form of a J-invariant symplectic form is twice the pullback of the induced Hermitian form along v ↦ v^(1,0)

TheoremThe Hermitian form of a J-invariant symplectic form is twice the pullback of the induced Hermitian form along v ↦ v^(1,0)#

with g = ω (·, J ·) and h its sesquilinear complexification, ω (v, J w) + i ω (v, w) = 2 h (v^(1,0), w^(1,0)).

TauCeti.SymplecticForm.Invariant.complexAssociatedForm_eq_two_mul_sesqComplexification.{u_1}
  {V : Type u_1} [AddCommGroup V] [_root_.Module ℝ V] {ω : TauCeti.SymplecticForm V}
  {J : TauCeti.AlmostComplexStructure V} (hinv : ω.Invariant J) (v w : V) :
  ω.complexAssociatedForm J v w =
    2 * ((ω.associatedBilinForm J).sesqComplexification (J.holomorphicPart v)) (J.holomorphicPart w)

Lean

Formalized in Tau Ceti as TauCeti.SymplecticForm.Invariant.complexAssociatedForm_eq_two_mul_sesqComplexification.

Sources

• Tau Ceti documentation: TauCeti.SymplecticForm.Invariant.complexAssociatedForm_eq_two_mul_sesqComplexification
• Source of TauCeti.SymplecticForm.Invariant.complexAssociatedForm_eq_two_mul_sesqComplexification in TauCeti/Geometry/Symplectic/Complex/HermitianForm.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanTauCeti.SymplecticForm.Invariant.complexAssociatedForm_eq_two_mul_sesqComplexification

Uses 1

Statement usesThe sesquilinear complexification of a real bilinear form B

DefinitionCliffordAlgebra.conjStar#

The conjugate-linear Clifford involution of the complexified Clifford algebra: Clifford conjugation star = reverse ∘ involute followed by complex conjugation of the coefficients. It is an involutive anti-automorphism (CliffordAlgebra.conjStar_mul, CliffordAlgebra.conjStar_conjStar) negating the real vectors.

CliffordAlgebra.conjStar.{u_1} {V : Type u_1} [AddCommGroup V] [_root_.Module ℝ V]
  (Q : QuadraticForm ℝ V) :
  CliffordAlgebra (QuadraticForm.baseChange ℂ Q) →ₗ⋆[ℂ]
    CliffordAlgebra (QuadraticForm.baseChange ℂ Q)

Lean

Formalized in Tau Ceti as CliffordAlgebra.conjStar.

Sources

• Tau Ceti documentation: CliffordAlgebra.conjStar
• Source of CliffordAlgebra.conjStar in TauCeti/LinearAlgebra/CliffordAlgebra/Complexification.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanCliffordAlgebra.conjStar

DefinitionCliffordAlgebra.scalarTrace#

The scalar part of an element of a Clifford algebra: its degree-zero component under the module isomorphism CliffordAlgebra.equivExterior with the exterior algebra.

CliffordAlgebra.scalarTrace.{u, v} {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M]
  [_root_.Module R M] [Invertible 2] (Q : QuadraticForm R M) : CliffordAlgebra Q →ₗ[R] R

Lean

Formalized in Tau Ceti as CliffordAlgebra.scalarTrace.

Sources

• Tau Ceti documentation: CliffordAlgebra.scalarTrace
• Source of CliffordAlgebra.scalarTrace in TauCeti/LinearAlgebra/CliffordAlgebra/ScalarTrace/Basic.lean
• Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry

LeanCliffordAlgebra.scalarTrace

Used by 3

Used byFaithfulness of the trace pairing · Positivity of the trace pairing · The scalar part is the normalized regular trace

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.