Generation of the type-D spin carrier by root subgroups

The full-weight type-D_n spin carrier is defined from its positive and negative numbered simple-root subgroups together with its split weight torus. This file proves that, over every commutative ring, the torus is already contained in the elementary subgroup generated by those root subgroups.

The represented simple generators at each node form an sl_2 triple by TauCeti.TypeDSpinCarrier.isSl2Triple_rep_rootGenerator, and every row of the type-D Cartan matrix has the explicit Bezout certificate TauCeti.sum_cartanMatrixD_mul_typeDCartanBezout, so every simple root is a primitive character of the weight torus. The generic Kostant coroot-generation theorem then makes the torus redundant in the pointwise generating family.

Applying the pointwise containment to the universal point of the torus, over the coordinate ring of the split torus itself, shows that the torus is also redundant scheme-theoretically: the toral-closure defining ideal over ℤ equals the ideal cut out by the numbered root subgroups alone, so the carrier is the root-generated Kostant group scheme. This is an equality of integral carriers; it does not say that the subgroup generated anew over a non-flat base is the base change of the integral carrier.

Main results

• TauCeti.TypeDSpinCarrier.weightTorusSubgroup_le_elementarySubgroup: the weight torus lies in the elementary subgroup over every commutative ring.
• TauCeti.TypeDSpinCarrier.weightTorusSubsystemSubgroup_univ_eq_elementarySubgroup: adjoining the weight torus to all numbered root subgroups gives exactly the elementary subgroup.
• TauCeti.TypeDSpinCarrier.definingIdeal_eq_kostantGeneratedDefiningIdeal: the integral toral-closure carrier is already cut out by the root subgroups alone.
• TauCeti.TypeDSpinCarrier.groupScheme_eq_kostantGeneratedGroupScheme and TauCeti.TypeDSpinCarrier.isIso_kostantGeneratedToToral: the carrier is the root-generated Kostant group scheme, and the canonical comparison between them is an isomorphism.
• TauCeti.TypeDSpinCarrier.groupScheme_hom_ext_of_rootSubgroup: a morphism out of the carrier is determined by its restrictions to the numbered root subgroups alone.

References

• R. Steinberg, Lectures on Chevalley Groups, Section 3.
• R. W. Carter, Simple Groups of Lie Type, Sections 6.4 and 7.1.

This file follows the formal template of TauCeti.Algebra.Lie.E7.Minuscule.Generation: the two specializations of the generic coroot-generation theorems are adapted from it, with the type-D Cartan matrix and spin weights in place of the type-E₇ data. The scheme-theoretic section follows TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLattice.SchemeGeneration.

theorem TauCeti.TypeDSpinCarrier.weightTorusSubgroup_le_elementarySubgroup (n : ℕ) (hn : 4 ≤ n) (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubgroup (lattice n).toAddSubgroup (latticeBasis n) (basisWeight n) ↑A ≤ UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ A

Over every commutative ring, the type-D full-spin weight torus on the base-changed admissible lattice is contained in the elementary group generated by the positive and negative numbered simple root subgroups.

theorem TauCeti.TypeDSpinCarrier.weightTorusSubsystemSubgroup_univ_eq_elementarySubgroup (n : ℕ) (hn : 4 ≤ n) (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) Set.univ A = UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ A

Over every commutative ring, adjoining the type-D full-spin weight torus to all positive and negative numbered simple root subgroups does not enlarge their elementary subgroup.

Scheme-theoretic generation

theorem TauCeti.TypeDSpinCarrier.definingIdeal_eq_kostantGeneratedDefiningIdeal (n : ℕ) (hn : 4 ≤ n) : definingIdeal n hn = UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n)

The full-weight type-Dₙ spin carrier is generated scheme-theoretically by its numbered root subgroups. Adjoining the represented weight torus does not change the integral defining Hopf ideal.

theorem TauCeti.TypeDSpinCarrier.groupScheme_eq_kostantGeneratedGroupScheme (n : ℕ) (hn : 4 ≤ n) : groupScheme n hn = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n)

The full-weight type-Dₙ spin carrier is the group scheme generated by its numbered positive and negative simple root subgroups.

instance TauCeti.TypeDSpinCarrier.isIso_kostantGeneratedToToral (n : ℕ) (hn : 4 ≤ n) : CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n))

The canonical inclusion of the root-generated type-Dₙ spin carrier into its toral closure is an isomorphism.

theorem TauCeti.TypeDSpinCarrier.groupScheme_hom_ext_of_rootSubgroup (n : ℕ) (hn : 4 ≤ n) {Y : CommHopfAlgCat ℤ} (f g : groupScheme n hn ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (k : Fin n ⊕ Fin n), CategoryTheory.CategoryStruct.comp (rootSubgroup n hn k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup n hn k) g) : f = g

Two morphisms out of the type-Dₙ spin carrier agree as soon as they agree on its numbered root subgroups. This drops the weight-torus hypothesis of TauCeti.TypeDSpinCarrier.groupScheme_hom_ext, which root generation of the carrier makes redundant.