The standard representation of the type-B spin carrier

The full-weight type-Bₙ₊₁ spin carrier is a closed subgroup of GL_(2^(n+1)). 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.

This file proves that the resulting representation, the spin representation of the carrier, is faithful over every commutative ring and simple over every field. For simplicity, restriction to the spin weight torus separates a nonzero invariant vector into its one-dimensional weight components, since the spin weights are pairwise distinct. A numbered simple root generator acts on an exterior basis vector by creating and contracting coordinates, so whenever the corresponding spin weight pairs to ∓1 with the simple coroot, the positive or negative simple-root element at parameter one has image equal to the original basis vector plus its simple reflection, up to sign. Subtracting the original vector therefore gives the reflected vector up to sign. The spin weights form a single orbit of the simple reflections, so a coordinate vector reaches every other one.

Main declarations

• TauCeti.TypeBSpinCarrier.standardComodule: the standard comodule on R^(2^(n+1)).
• TauCeti.TypeBSpinCarrier.isFaithful_standardComodule: faithfulness of the standard comodule.
• TauCeti.TypeBSpinCarrier.mulVec_mem and TauCeti.TypeBSpinCarrier.points_mulVec_mem: subcomodules are stable under carrier-valued points and under concrete carrier points.
• TauCeti.TypeBSpinCarrier.torusCorestrict_eq_ofWeights: restricted to the weight torus, the standard comodule is the direct sum of the spin weight lines.
• TauCeti.TypeBSpinCarrier.isSimpleOrder_of_spinWeights_of_rootSubgroupPoints: a comodule with the spin weight decomposition whose subcomodules are stable under the numbered simple-root matrices is simple over a field.
• TauCeti.TypeBSpinCarrier.instIsSimpleOrderSubcomodule: simplicity over a field.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• J. E. Humphreys, Linear Algebraic Groups, §26.
• J. C. Jantzen, Representations of Algebraic Groups, I.2 and II.2.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate II.

The corestriction, faithfulness, and point-action arguments, and the shape of the simplicity proof, follow the type-E₆ minuscule carrier in TauCeti.Algebra.Lie.E6.Minuscule.StandardComodule.

@[instance_reducible]

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

The standard right comodule of the specialized type-Bₙ₊₁ spin carrier.

Equations

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

theorem TauCeti.TypeBSpinCarrier.isFaithful_standardComodule (n : ℕ) (R : Type u) [CommRing R] : Comodule.IsFaithful

The standard comodule of the specialized type-Bₙ₊₁ spin carrier is faithful.

theorem TauCeti.TypeBSpinCarrier.mulVec_mem (n : ℕ) (R : Type u) [CommRing R] (N : Subcomodule R (↑(coordinateHopfAlgebra n R)) (Fin (dimension n) → R)) (g : WithConv (↑(coordinateHopfAlgebra n R) →ₐ[R] R)) {w : Fin (dimension n) → R} (hw : w ∈ N) : (↑(GeneralLinear.pointToGeneralLinear (dimension n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R (dimension n)) (baseChangeDefiningIdeal n R) ↧R)) g))).mulVec w ∈ N

A subcomodule of the standard carrier comodule is stable under every carrier-valued point.

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

A subcomodule of the standard carrier comodule is stable under every concrete carrier point.

The numbered simple root generators on the coordinate basis

@[reducible, inline]

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

The character of the spin weight torus attached to a spin-basis index.

Equations

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

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

Distinct spin-basis indices give distinct characters of the weight torus.

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

Restricting the standard carrier comodule to the spin weight torus gives the direct sum of the distinct spin weight lines. Corestricting along weightTorusToBaseChangeCoordinateMap turns the standard comodule on Fin (dimension n) → R into the comodule in which the coordinate basis vector at a spans the weight line of the torus character basisCharacter n a.

Simplicity over a field

theorem TauCeti.TypeBSpinCarrier.isSimpleOrder_of_spinWeights_of_rootSubgroupPoints (n : ℕ) (k : Type u) [Field k] {H : Type u_1} [AddCommGroup H] [Module k H] [Coalgebra k H] [Comodule k H (Fin (dimension n) → k)] (f : H →ₗc[k] MonoidAlgebra k (Multiplicative (Fin (n + 1) →₀ ℤ))) (hweights : Comodule.Corestrict f = Comodule.ofWeights (Pi.basisFun k (Fin (dimension n))) (basisCharacter n)) (hroot : ∀ (N : Subcomodule k H (Fin (dimension n) → k)) (j : Fin (n + 1) ⊕ Fin (n + 1)), ∀ w ∈ N, (↑↑((rootSubgroupPoints n j k) (Multiplicative.ofAdd 1))).mulVec w ∈ N) : IsSimpleOrder (Subcomodule k H (Fin (dimension n) → k))

A comodule on k^(2^(n+1)) with the type-Bₙ₊₁ spin weight decomposition is simple if its subcomodules are stable under the numbered positive and negative simple-root matrices at parameter one. This applies both to the specialization of the integral carrier and to the subgroup generated directly over the field.

instance TauCeti.TypeBSpinCarrier.instIsSimpleOrderSubcomodule (n : ℕ) (k : Type u) [Field k] : IsSimpleOrder (Subcomodule k (↑(coordinateHopfAlgebra n k)) (Fin (dimension n) → k))

The standard comodule of the specialized type-Bₙ₊₁ spin carrier is simple over every field.