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))
Used by 1
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)
Uses 1
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_compin TauCeti/RepresentationTheory/Spin/Polarization/Fock/Basic.lean - Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry
Uses 1
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
Uses 1
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
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
Uses 1
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
Uses 1
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
Uses 1
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
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 →ₗ[ℂ] ℂ
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_sesqComplexificationin TauCeti/Geometry/Symplectic/Complex/HermitianForm.lean - Tau Ceti roadmap status: Clifford bundles, spin structures, and Dirac geometry
Uses 1
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)
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.