The full-weight type-D spin carrier #
For 4 ≤ n, this file specializes the type-Dₙ spin representation to the canonical split
quadratic space M* × M, where M = Fin n → ℚ. Its exterior coordinate lattice has basis
indexed by the sign sets Finset (Fin n) and is stable under the type-D Serre Kostant form.
The corresponding spin weights span the full simply connected character lattice.
These data are fed into the Kostant toral-closure construction. The result is an explicit affine
group scheme over ℤ, cut out inside GL_(2^n) by the largest Hopf ideal killed by the numbered
simple-root subgroups and the represented rank-n split torus. In particular, the construction
uses the full spin module rather than one half-spin summand, so its weights see both spinor cosets
of the type-D root lattice.
Those data are then carried onto matrix-valued points: the numbered root subgroups and the weight
torus become homomorphisms into TauCeti.TypeDSpinCarrier.points, and conjugating one by the
other rescales its parameter through a character. That character is named: it is the positive or
negative i-th simple root of TauCeti.DynkinType.simplyConnectedRootDatum at
TauCeti.DynkinType.D n, the uniform pinned datum a consumer reaches holding only a Dynkin type.
That naming is what makes the carrier's pinning conventions statable without reference to its
2 ^ n-dimensional spin realization.
No smoothness, reductivity, maximality of the torus, or identification of the carrier's whole root datum is asserted here: the equations below concern the simple root characters alone, and exhibit neither a Borel subgroup nor a root subgroup for a non-simple root. Those are subsequent steps in the pinned Chevalley--Demazure construction.
Main declarations #
TauCeti.TypeDSpinCarrier.groupScheme: the full-weight spin carrier overℤ.TauCeti.TypeDSpinCarrier.rootSubgroup: its numbered simple-root subgroup morphisms.TauCeti.TypeDSpinCarrier.weightTorus: its closed rank-nsplit torus.TauCeti.TypeDSpinCarrier.points: its matrix-valued points over a commutative ring.TauCeti.TypeDSpinCarrier.rootSubgroupPointsandTauCeti.TypeDSpinCarrier.weightTorusPoints: the numbered root subgroups and the weight torus on those matrix-valued points.
Main results #
TauCeti.TypeDSpinCarrier.weightTorusPoints_conj_rootSubgroupPointsandTauCeti.TypeDSpinCarrier.weightTorus_conj_rootSubgroup: conjugation by the weight torus rescales the parameter of each numbered root subgroup through that character, on matrix-valued points and on scheme points respectively.TauCeti.TypeDSpinCarrier.weightTorusPoints_conj_rootSubgroupPoints_root_simpleIndex,TauCeti.TypeDSpinCarrier.weightTorus_conj_rootSubgroup_root_simpleIndex, and their negative-root counterparts: the same equations with the named simple root ofTauCeti.DynkinType.simplyConnectedRootDatumas their exponent.
References #
- C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§26--27.
- N. Bourbaki, Groupes et algèbres de Lie, Chapters 4--6, Plate IV.
- J. C. Jantzen, Representations of Algebraic Groups, II.1--2.
The carrier API follows the formal template of
TauCeti.Algebra.Lie.E6.Minuscule.GroupScheme and
TauCeti.Algebra.Lie.Symplectic.StandardCarrier.Scheme, and the pinning equations below follow
that of TauCeti.Algebra.Lie.Symplectic.StandardCarrier.RootDatum; the split spin representation,
exterior lattice, and type-D weights are specific to this construction. This advances Layer 9,
"The Chevalley--Demazure construction", of the ReductiveGroups roadmap and supplies the type-D
carrier required by milestone L0 of the CFSGStatement roadmap.
The split spin representation and its lattice #
The canonical split polarization used by the type-Dₙ spin carrier.
Instances For
The coordinate basis of the first isotropic summand in the split polarization.
Instances For
The rational spin representation of the type-Dₙ Serre presentation, extended to its
universal enveloping algebra.
Equations
Instances For
The integral exterior coordinate lattice in the split spin module.
Equations
Instances For
The dimension of the full spin module, expressed as the cardinality of its exterior basis.
Equations
Instances For
The exterior coordinate basis, reindexed by a finite ordinal for the general-linear carrier.
Equations
Instances For
The sign set represented by a finite-ordinal spin-basis index.
Equations
- TauCeti.TypeDSpinCarrier.signSet n i = (Fintype.equivFin (Finset (Fin n))).symm i
Instances For
The simply connected type-Dₙ weight of a finite-ordinal spin-basis vector.
Equations
Instances For
A reindexed lattice-basis vector is the exterior basis vector of its sign set.
Every represented numbered root generator is nilpotent.
Every represented numbered root generator has nilpotency class at most two: it squares to zero.
The represented positive and negative simple generators at a common type-D node, together
with the represented Cartan generator, form an sl_2 triple.
The type-D Serre Kostant form preserves the split exterior coordinate lattice.
The generic Kostant form for the numbered type-D generators preserves the split exterior
coordinate lattice.
Every finite-ordinal exterior basis vector has its named integral type-D spin weight.
The weights of the full spin basis span the simply connected type-D character lattice.
The closed carrier and its pinned generators #
The Hopf ideal cutting out the full-weight type-Dₙ spin carrier inside GL_(2^n).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining ideal is the one supplied by the generic Kostant toral-closure construction.
The full-weight type-Dₙ spin carrier over ℤ, obtained as the smallest closed subgroup
scheme containing the represented numbered root subgroups and weight torus.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The quotient-spectrum presentation of the type-Dₙ spin carrier.
The type-Dₙ carrier is the generic Kostant toral closure for its spin representation.
The canonical inclusion of the type-Dₙ spin carrier into GL_(2^n).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical inclusion is the generic Kostant toral-closure inclusion, read across the carrier's presentation as that closure.
The type-Dₙ spin carrier is a closed subgroup scheme of its ambient general linear group.
The root subgroup is the generic Kostant root subgroup, transported across the carrier's quotient-spectrum presentation.
Including a numbered root subgroup into the ambient general linear group recovers its represented Kostant root subgroup.
The represented rank-n split weight torus in the type-Dₙ spin carrier.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The represented weight torus is the generic factored Kostant torus at the type-Dₙ spin
data.
Including the weight torus into the ambient general linear group recovers the diagonal torus of the spin weights.
The full spin weights make the represented split torus a closed subgroup scheme of the carrier.
Two morphisms out of the type-Dₙ spin carrier agree when they agree on its numbered root
subgroups and represented split torus.
Matrix-valued points #
The carrier points are exactly the invertible matrices cut out by the defining Hopf ideal.
A matrix is a carrier point exactly when its associated convolution point kills the defining Hopf ideal.
The parametrized numbered root subgroup inside the type-Dₙ spin carrier points. The
parameter is read through the canonical multiplicative copy of the additive group of A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A numbered root-subgroup point is its represented divided-power exponential matrix.
A weight-torus point is the diagonal matrix obtained by evaluating each spin weight.
The pinning equation #
Conjugation by the spin weight torus acts on each numbered root subgroup through its
positive or negative simple-root character, on matrix-valued points. A torus point s carries
the root-subgroup point of parameter u to the one of parameter α_k(s) u.
Conjugation by the spin weight torus acts on each numbered root subgroup through its positive or negative simple-root character.
The numbered root subgroups sit at the named simple roots #
The two identifications the equations below rewrite with,
TauCeti.TypeDStd.rootGeneratorWeight_inl_eq_root_simpleIndex and its lowering counterpart, are
proved beside the weight they name, in
TauCeti/Algebra/Lie/Orthogonal/TypeD/Root/Generators.lean.
None of the equations below is a simp lemma. Their right-hand sides name the character through
TauCeti.DynkinType.simplyConnectedRootDatum, which simp unfolds at the D n branch, so they
are not simp-normal; the numbered equations above are, and these are explicit rewrite lemmas for
a consumer holding a Dynkin type, as in
TauCeti.SpStd.weightTorus_conj_rootSubgroup_root_simpleIndex.
On matrix-valued points, conjugation by the spin weight torus rescales the i-th raising root
subgroup through the i-th simple root of the pinned type-Dₙ datum.
On matrix-valued points, conjugation by the spin weight torus rescales the i-th lowering root
subgroup through the negative of the i-th simple root of the pinned type-Dₙ datum.
Conjugation by the spin weight torus rescales the i-th raising root subgroup through the
i-th simple root of the pinned type-Dₙ datum.
Conjugation by the spin weight torus rescales the i-th lowering root subgroup through the
negative of the i-th simple root of the pinned type-Dₙ datum.