Generation of the E₇ minuscule carrier by root subgroups

The type-E₇ minuscule carrier is defined using both its fourteen numbered simple root subgroups and its rank-seven weight torus. This file proves that, on the underlying base-changed lattice over any commutative ring, the torus is already contained in the elementary group generated by the root subgroups.

The represented simple generators at each node form an sl₂ triple by TauCeti.E7Minuscule.isSl2Triple_rep_serreRootGenerator. The remaining concrete input is supplied here: every row of the type-E₇ Cartan matrix contains -1, so its entries have an explicit integral linear combination equal to one. The generic coroot-generation theorem then puts every coordinate cocharacter, and hence the whole weight torus, in the elementary group.

The pointwise containment can be tested over the coordinate ring of the universal weight-torus point. This proves that the root-generated and toral-closure defining ideals over ℤ are equal, so the weight torus is also redundant scheme-theoretically. The equality persists after base change. It does not say that the transported integral carrier equals the subgroup generated anew over a non-flat base.

Main results

• TauCeti.E7Minuscule.weightTorusSubgroup_le_elementarySubgroup: the weight torus lies in the elementary subgroup over every commutative ring.
• TauCeti.E7Minuscule.weightTorusSubsystemSubgroup_univ_eq_elementarySubgroup: adjoining the weight torus to all numbered root subgroups gives exactly the elementary subgroup.
• TauCeti.E7Minuscule.definingIdeal_eq_kostantGeneratedDefiningIdeal: the integral toral-closure carrier is already the root-generated carrier.
• TauCeti.E7Minuscule.groupScheme_eq_kostantGeneratedGroupScheme and TauCeti.E7Minuscule.isIso_kostantGeneratedToToral: the corresponding group schemes agree and their canonical comparison is an isomorphism.
• TauCeti.E7Minuscule.baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal: the corresponding equality in the transported presentation over every commutative ring.
• TauCeti.E7Minuscule.groupScheme_hom_ext_of_rootSubgroup: a morphism out of the carrier is determined by its restrictions to the fourteen 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.

theorem TauCeti.E7Minuscule.weightTorusSubgroup_le_elementarySubgroup (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubgroup lattice.toAddSubgroup latticeBasis DynkinType.e7MinusculeWeight ↑A ≤ UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator A

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

theorem TauCeti.E7Minuscule.weightTorusSubsystemSubgroup_univ_eq_elementarySubgroup (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.e7MinusculeWeight Set.univ A = UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator A

Over every commutative ring, adjoining the type-E₇ minuscule weight torus to all fourteen numbered simple root subgroups does not enlarge their elementary subgroup.

Scheme-theoretic generation

theorem TauCeti.E7Minuscule.definingIdeal_eq_kostantGeneratedDefiningIdeal : definingIdeal = UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis

The full-weight type-E₇ toral closure is already generated scheme-theoretically by its fourteen numbered root subgroups. Equivalently, adjoining the represented weight torus does not change the integral defining Hopf ideal.

theorem TauCeti.E7Minuscule.groupScheme_eq_kostantGeneratedGroupScheme : groupScheme = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis

The type-E₇ toral-closure group scheme is the group scheme generated by the fourteen numbered root subgroups.

instance TauCeti.E7Minuscule.isIso_kostantGeneratedToToral : CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.e7MinusculeWeight)

The canonical inclusion of the root-generated type-E₇ carrier into its toral closure is an isomorphism.

theorem TauCeti.E7Minuscule.baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal (A : Type v) [CommRing A] : baseChangeDefiningIdeal A = UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIdeal (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis A

After base change to any commutative ring, the transported type-E₇ 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.E7Minuscule.groupScheme_hom_ext_of_rootSubgroup {Y : CommHopfAlgCat ℤ} (f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (k : Fin 7 ⊕ Fin 7), CategoryTheory.CategoryStruct.comp (rootSubgroup k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup k) g) : f = g

Two morphisms out of the full-weight type-E₇ minuscule carrier agree as soon as they agree on its fourteen numbered root subgroups. This drops the weight-torus hypothesis of TauCeti.E7Minuscule.groupScheme_hom_ext, which root generation of the carrier makes redundant.