Generation of the tripled type-D4 weight torus by root subgroups

The tripled type-D₄ carrier is defined from its eight positive and negative numbered simple-root subgroups together with its rank-four 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₂ triple by TauCeti.D4Tripled.isSl2Triple_rep_serreRootGenerator, 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.

Testing that containment over the coordinate ring of the universal weight-torus point upgrades it to the scheme-theoretic statement: the toral-closure and root-generated defining ideals over ℤ agree, so the torus is redundant among the scheme-theoretic generators as well, and the canonical comparison of the two carriers is an isomorphism. The equality of ideals survives transport along ℤ → A. It does not say that the transported integral carrier is the subgroup generated anew by the root subgroups over a non-flat base.

Main results

• TauCeti.D4Tripled.weightTorusSubgroup_le_elementarySubgroup: the weight torus lies in the elementary subgroup over every commutative ring.
• TauCeti.D4Tripled.weightTorusSubsystemSubgroup_univ_eq_elementarySubgroup: adjoining the weight torus to all numbered root subgroups gives exactly the elementary subgroup.
• TauCeti.D4Tripled.definingIdeal_eq_kostantGeneratedDefiningIdeal: the integral toral-closure carrier is already the root-generated carrier.
• TauCeti.D4Tripled.groupScheme_eq_kostantGeneratedGroupScheme and TauCeti.D4Tripled.isIso_kostantGeneratedToToral: the corresponding group schemes agree and their canonical comparison is an isomorphism.
• TauCeti.D4Tripled.baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal: the corresponding equality in the transported presentation over every commutative ring.
• TauCeti.D4Tripled.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.
• TauCeti.Algebra.Lie.Orthogonal.TypeD.SpinCarrier.Generation, whose formal template this file follows with the tripled weights in place of the spin weights.

theorem TauCeti.D4Tripled.weightTorusSubgroup_le_elementarySubgroup (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubgroup lattice.toAddSubgroup latticeBasis DynkinType.d4TripledWeight ↑A ≤ UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator A

Over every commutative ring, the tripled type-D₄ 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.D4Tripled.weightTorusSubsystemSubgroup_univ_eq_elementarySubgroup (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.d4TripledWeight Set.univ A = UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator A

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

Scheme-theoretic generation

theorem TauCeti.D4Tripled.definingIdeal_eq_kostantGeneratedDefiningIdeal : definingIdeal = UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis

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

theorem TauCeti.D4Tripled.groupScheme_eq_kostantGeneratedGroupScheme : groupScheme = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis

The tripled type-D₄ carrier is the group scheme generated by its eight numbered positive and negative simple root subgroups.

instance TauCeti.D4Tripled.isIso_kostantGeneratedToToral : CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.d4TripledWeight)

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

theorem TauCeti.D4Tripled.baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal (A : Type v) [CommRing A] : baseChangeDefiningIdeal A = UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis A

After base change to any commutative ring, the transported tripled type-D₄ carrier ideal is the transport of the root-generated integral ideal. This does not identify it with the common kernel of the root-subgroup maps formed anew over that ring.

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

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