Spin
Results named in Tau Ceti's TauCeti.RepresentationTheory.Spin modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
DefinitionThe even structure theorem#
for an even-dimensional polarized quadratic space the even Clifford subalgebra is the product of the endomorphism algebras of the two half-spin summands.
This is the even-subalgebra companion of TauCeti.SpinPolarizationData.cliffordEquivEnd. It gives
the invariant-subspace dichotomy for both summands, which is simplicity for S⁺ and, when
P.W ≠ ⊥, for S⁻; it also distinguishes their two even-Clifford actions.
TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd.{u, v} {K : Type u} [Field K] {V : Type v}
[AddCommGroup V] [_root_.Module K V] {Q : QuadraticForm K V} (P : TauCeti.SpinPolarizationData Q)
[Invertible 2] [FiniteDimensional K V] (hline : P.line = ⊥) :
↥(CliffordAlgebra.even Q) ≃ₐ[K]
Module.End K ↥(TauCeti.spinPlus Q P) × Module.End K ↥(TauCeti.spinMinus Q P)
Lean
Formalized in Tau Ceti as TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd.
Sources
Used by 1
DefinitionThe odd structure theorem in operator form#
for a polarized quadratic space of odd
dimension over a field of characteristic not two, the Fock action is an isomorphism of
F-algebras from the even Clifford subalgebra onto the endomorphism algebra of the spinor module
S = ⋀·W.
This is the odd-dimensional companion of
TauCeti.SpinPolarizationData.cliffordEquivEnd, one grade down: there the whole algebra is
Module.End F S, here only its even half is, the whole algebra being two copies of it.
TauCeti.SpinPolarizationData.evenCliffordEquivEnd.{u, v} {F : Type u} [Field F] [NeZero 2]
{V : Type v} [AddCommGroup V] [_root_.Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V}
(P : TauCeti.SpinPolarizationData Q) (hodd : Odd (Module.finrank F V)) :
↥(CliffordAlgebra.even Q) ≃ₐ[F] Module.End F (ExteriorAlgebra F ↥P.W)
Lean
Formalized in Tau Ceti as TauCeti.SpinPolarizationData.evenCliffordEquivEnd.
Other forms
The odd structure theorem, labelled by the two signs of the line coordinate. Formalized in Tau Ceti as TauCeti.SpinPolarizationData.cliffordEquivEndProd.
TauCeti.SpinPolarizationData.cliffordEquivEndProd.{u, v} {F : Type u} [Field F] {V : Type v}
[AddCommGroup V] [_root_.Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V}
(P : TauCeti.SpinPolarizationData Q) [NeZero 2] (hodd : Odd (Module.finrank F V)) :
CliffordAlgebra Q ≃ₐ[F]
Module.End F (ExteriorAlgebra F ↥P.W) × Module.End F (ExteriorAlgebra F ↥P.W)
Sources
DefinitionThe structure theorem#
the Clifford algebra of a polarized quadratic space of dimension
2 * l is the matrix algebra M_{2^l}(K), read in a basis of the spinor module ⋀·W, which has
dimension 2 ^ l.
TauCeti.SpinPolarizationData.cliffordEquivMatrix.{u, v} {K : Type u} [Field K] {V : Type v}
[AddCommGroup V] [_root_.Module K V] {Q : QuadraticForm K V} (P : TauCeti.SpinPolarizationData Q)
[Invertible 2] [FiniteDimensional K V] {l : ℕ} (hV : Module.finrank K V = 2 * l) :
CliffordAlgebra Q ≃ₐ[K] Matrix (Fin (2 ^ l)) (Fin (2 ^ l)) K
Lean
Formalized in Tau Ceti as TauCeti.SpinPolarizationData.cliffordEquivMatrix.
Sources
Uses 1 · Used by 1
TheoremThe structure theorem in odd dimension#
over a separably closed field of characteristic not
two, the Clifford algebra of a nondegenerate quadratic form on a space of dimension 2 * l + 1 is
the product of two copies of the matrix algebra M_{2^l}(F).
This is the odd-dimensional companion of
CliffordAlgebra.nonempty_algEquiv_matrix_of_finrank_eq_two_mul, and the two blocks are not an
artefact of the proof: the product displayed here has (1, 0) as a central idempotent other than
0 and 1, so the algebra is not simple, whereas in even dimension it is
(TauCeti.SpinPolarizationData.isSimpleRing_cliffordAlgebra).
CliffordAlgebra.nonempty_algEquiv_matrix_prod_of_finrank_eq_two_mul_add_one.{u, v} {F : Type u}
[Field F] [NeZero 2] {V : Type v} [AddCommGroup V] [_root_.Module F V] [FiniteDimensional F V]
{Q : QuadraticForm F V} [IsSepClosed F] {l : ℕ} (hQ : QuadraticMap.Nondegenerate)
(hV : Module.finrank F V = 2 * l + 1) :
Nonempty
(CliffordAlgebra Q ≃ₐ[F]
Matrix (Fin (2 ^ l)) (Fin (2 ^ l)) F × Matrix (Fin (2 ^ l)) (Fin (2 ^ l)) F)
Lean
Formalized in Tau Ceti as CliffordAlgebra.nonempty_algEquiv_matrix_prod_of_finrank_eq_two_mul_add_one.
Sources
DefinitionThe structure theorem in operator form#
for an even-dimensional polarized quadratic space,
the Fock action is an isomorphism of K-algebras from CliffordAlgebra Q onto the endomorphism
algebra of the spinor module S = ⋀·W.
TauCeti.SpinPolarizationData.cliffordEquivEnd.{u, v} {K : Type u} [Field K] {V : Type v}
[AddCommGroup V] [_root_.Module K V] {Q : QuadraticForm K V} (P : TauCeti.SpinPolarizationData Q)
[Invertible 2] [FiniteDimensional K V] (h : Even (Module.finrank K V)) :
CliffordAlgebra Q ≃ₐ[K] Module.End K (ExteriorAlgebra K ↥P.W)
TheoremThe structure theorem over a separably closed field#
the Clifford algebra of a
nondegenerate quadratic form on a 2l-dimensional space is the matrix algebra M_{2^l}(F).
The isomorphism is not canonical — it is read in a basis of the spinor module of a polarization,
and neither the polarization nor the basis is unique — so the statement is Nonempty. The
polarization-dependent isomorphism itself is
TauCeti.SpinPolarizationData.cliffordEquivMatrix.
CliffordAlgebra.nonempty_algEquiv_matrix_of_finrank_eq_two_mul.{u, v} {F : Type u} [Field F]
[NeZero 2] {V : Type v} [AddCommGroup V] [_root_.Module F V] [FiniteDimensional F V]
{Q : QuadraticForm F V} [IsSepClosed F] {l : ℕ} (hQ : QuadraticMap.Nondegenerate)
(hV : Module.finrank F V = 2 * l) :
Nonempty (CliffordAlgebra Q ≃ₐ[F] Matrix (Fin (2 ^ l)) (Fin (2 ^ l)) F)
Lean
Formalized in Tau Ceti as CliffordAlgebra.nonempty_algEquiv_matrix_of_finrank_eq_two_mul.
Sources
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.