The standard representation of the type-D spin carrier and its half-spin summands

The full-weight type-Dₙ spin carrier is a closed subgroup of GL_(2^n). After base change to a commutative ring R, its standard representation is therefore the corestriction of the standard general-linear comodule along the quotient coordinate morphism; it is the spin representation S = S⁺ ⊕ S⁻ of the carrier, on the coordinates indexed by sign sets.

This file proves that this representation is faithful over every commutative ring, and that its two half-spin summands are subcomodules over every commutative ring: the coordinates whose sign sets have even cardinality span S⁺, those of odd cardinality span S⁻, and the two are complementary. The input is that the carrier preserves the half-spin decomposition scheme-theoretically, TauCeti.TypeDSpinCarrier.coordinateMap_X_eq_zero.

Main declarations

• TauCeti.TypeDSpinCarrier.standardComodule: the standard comodule on R^(2^n).
• TauCeti.TypeDSpinCarrier.isFaithful_standardComodule: faithfulness of the standard comodule.
• TauCeti.TypeDSpinCarrier.coefficientMatrix_basisFun: its matrix coefficients.
• TauCeti.TypeDSpinCarrier.points_mulVec_mem: stability of subcomodules under carrier points.
• TauCeti.TypeDSpinCarrier.torusCorestrict_eq_ofWeights: restriction to the distinct spin weight lines of the weight torus.
• TauCeti.TypeDSpinCarrier.halfSpinSubcomodule: the half-spin summand of a given parity, as a subcomodule.
• TauCeti.TypeDSpinCarrier.mem_halfSpinSubcomodule: its vectors are those supported on sign sets of that parity.
• TauCeti.TypeDSpinCarrier.isCompl_halfSpinSubcomodule_toSubmodule: the two half-spin summands are complementary.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• W. Fulton and J. Harris, Representation Theory: A First Course, §20.2.
• J. C. Jantzen, Representations of Algebraic Groups, I.2.

The corestriction and faithfulness arguments follow the type-B spin carrier in TauCeti.Algebra.Lie.Orthogonal.TypeB.SpinCarrier.StandardComodule, and the summand subcomodules follow those of the tripled type-D₄ carrier in TauCeti.Algebra.Lie.D4.Tripled.StandardComodule.

@[instance_reducible]

noncomputable def TauCeti.TypeDSpinCarrier.standardComodule (n : ℕ) (hn : 4 ≤ n) (R : Type u) [CommRing R] : Comodule R (↑(coordinateHopfAlgebra n hn R)) (Fin (dimension n) → R)

The standard right comodule of the specialized type-Dₙ spin carrier.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.TypeDSpinCarrier.isFaithful_standardComodule (n : ℕ) (hn : 4 ≤ n) (R : Type u) [CommRing R] : Comodule.IsFaithful

The standard comodule of the specialized type-Dₙ spin carrier is faithful.

theorem TauCeti.TypeDSpinCarrier.coefficientMatrix_basisFun (n : ℕ) (hn : 4 ≤ n) (R : Type u) [CommRing R] (a b : Fin (dimension n)) : Comodule.coefficientMatrix (Pi.basisFun R (Fin (dimension n))) a b = (CommHopfAlgCat.Hom.hom (coordinateMap n hn R)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R (dimension n)) ((GeneralLinear.coordinateRingMap R (dimension n)) (MvPolynomial.X (a, b))))

The standard coefficient matrix is the image of the ambient matrix coordinates in the carrier coordinate algebra.

theorem TauCeti.TypeDSpinCarrier.points_mulVec_mem (n : ℕ) (hn : 4 ≤ n) (R : Type u) [CommRing R] (N : Subcomodule R (↑(coordinateHopfAlgebra n hn R)) (Fin (dimension n) → R)) (g : ↥(points n hn R)) {w : Fin (dimension n) → R} (hw : w ∈ N) : (↑↑g).mulVec w ∈ N

A subcomodule of the standard spin representation is stable under every concrete carrier point, over any commutative ring.

The weight torus

@[reducible, inline]

noncomputable abbrev TauCeti.TypeDSpinCarrier.basisCharacter (n : ℕ) (a : Fin (dimension n)) : Multiplicative (Fin n →₀ ℤ)

The character of the spin weight torus attached to a coordinate basis vector.

Equations

• TauCeti.TypeDSpinCarrier.basisCharacter n a = TauCeti.SplitTorus.weightCharacter (TauCeti.TypeDSpinCarrier.basisWeight n a)

theorem TauCeti.TypeDSpinCarrier.basisCharacter_injective (n : ℕ) : Function.Injective (basisCharacter n)

Distinct spin-basis indices define distinct characters, including between the two half-spin summands.

theorem TauCeti.TypeDSpinCarrier.torusCorestrict_eq_ofWeights (n : ℕ) (hn : 4 ≤ n) (R : Type u) [CommRing R] : have x := standardComodule n hn R; Comodule.Corestrict (CommHopfAlgCat.Hom.hom (weightTorusToBaseChangeCoordinateMap n hn R)).toCoalgHom = Comodule.ofWeights (Pi.basisFun R (Fin (dimension n))) (basisCharacter n)

Restriction of the standard spin comodule to the weight torus is the direct sum of the spin character lines. This equality holds over every commutative ring.

The half-spin subcomodules

noncomputable def TauCeti.TypeDSpinCarrier.halfSpinSubcomodule (n : ℕ) (hn : 4 ≤ n) (R : Type u) [CommRing R] (j : ZMod 2) : Subcomodule R (↑(coordinateHopfAlgebra n hn R)) (Fin (dimension n) → R)

The half-spin summand of parity j is a subcomodule of the standard carrier comodule, over every commutative ring. It is spanned by the coordinate vectors whose sign sets have cardinality of parity j: S⁺ for j = 0 and S⁻ for j = 1.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.TypeDSpinCarrier.halfSpinSubcomodule_toSubmodule (n : ℕ) (hn : 4 ≤ n) (R : Type u) [CommRing R] (j : ZMod 2) : (halfSpinSubcomodule n hn R j).toSubmodule = Submodule.span R (⇑(Pi.basisFun R (Fin (dimension n))) '' {a : Fin (dimension n) | ↑(signSet n a).card = j})

A half-spin subcomodule is the span of the coordinate vectors of its parity.

@[simp]

theorem TauCeti.TypeDSpinCarrier.mem_halfSpinSubcomodule (n : ℕ) (hn : 4 ≤ n) (R : Type u) [CommRing R] (j : ZMod 2) (v : Fin (dimension n) → R) : v ∈ halfSpinSubcomodule n hn R j ↔ ∀ (a : Fin (dimension n)), ↑(signSet n a).card ≠ j → v a = 0

Membership in a half-spin subcomodule means vanishing at every sign set of the other parity.

theorem TauCeti.TypeDSpinCarrier.isCompl_halfSpinSubcomodule_toSubmodule (n : ℕ) (hn : 4 ≤ n) (R : Type u) [CommRing R] : IsCompl (halfSpinSubcomodule n hn R 0).toSubmodule (halfSpinSubcomodule n hn R 1).toSubmodule

The two half-spin subcomodules are complementary: the standard carrier comodule is the direct sum S⁺ ⊕ S⁻ of its even and odd half-spin summands.