Generation of the E₆ minuscule carrier by root subgroups

The type-E₆ minuscule carrier is defined from twelve numbered simple root subgroups together with its rank-six weight torus. Over every commutative ring, this file proves that the represented weight torus is already contained in the elementary group generated by those root subgroups.

The proof combines two concrete features of the minuscule carrier. The positive and negative generators at every node form an sl₂ triple after passing to the represented rational module. Also, every row of the type-E₆ Cartan matrix contains -1, giving an explicit integral Bézout witness for the corresponding root character. The generic coroot-generation theorem therefore puts every coordinate cocharacter, and hence every point of the weight torus, in the elementary group.

Testing this containment on the universal weight-torus point proves that the root-generated and toral-closure defining ideals over ℤ agree. Thus the weight torus is redundant not only in each group of points but in the integral group scheme itself. The equality persists in the transported presentation after arbitrary base change; it does not identify that presentation with the subgroup generated anew over a non-flat base.

Main results

• TauCeti.E6Minuscule.elementarySubgroup: the subgroup of carrier points generated by the ranges of the twelve named root-subgroup maps.
• TauCeti.E6Minuscule.elementarySubgroup_le_iff: its least-subgroup elimination principle.
• TauCeti.E6Minuscule.weightTorusSubgroup_le_elementarySubgroup: the represented weight torus lies in the generic Kostant elementary subgroup over every commutative ℤ-algebra.
• TauCeti.E6Minuscule.weightTorusPoints_range_le_elementarySubgroup: the range of the named weight-torus map lies in the elementary subgroup over every commutative ring.
• TauCeti.E6Minuscule.definingIdeal_eq_kostantGeneratedDefiningIdeal: the integral toral-closure carrier is already the root-generated carrier.
• TauCeti.E6Minuscule.groupScheme_eq_kostantGeneratedGroupScheme and TauCeti.E6Minuscule.isIso_kostantGeneratedToToral: the corresponding group schemes agree and their canonical comparison is an isomorphism.
• TauCeti.E6Minuscule.groupScheme_hom_ext_of_rootSubgroup: homomorphisms out of the carrier are determined by the twelve numbered root subgroups alone.
• TauCeti.E6Minuscule.baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal: the corresponding equality in every transported presentation.

References

• R. Steinberg, Lectures on Chevalley Groups, §3.
• R. W. Carter, Simple Groups of Lie Type, §§6.4 and 7.1.
• The scheme-theoretic comparison follows the parallel type-E₇ argument in TauCeti.Algebra.Lie.E7.Minuscule.Generation.

noncomputable def TauCeti.E6Minuscule.elementarySubgroup (A : Type v) [CommRing A] : Subgroup ↥(points A)

The elementary subgroup of the type-E₆ minuscule carrier points, generated by the ranges of its twelve named positive and negative simple-root subgroup maps.

Equations

• TauCeti.E6Minuscule.elementarySubgroup A = ⨆ (k : Fin 6 ⊕ Fin 6), (TauCeti.E6Minuscule.rootSubgroupPoints k A).range

theorem TauCeti.E6Minuscule.rootSubgroupPoints_mem_elementarySubgroup (A : Type v) [CommRing A] (k : Fin 6 ⊕ Fin 6) (u : Multiplicative A) : (rootSubgroupPoints k A) u ∈ elementarySubgroup A

Every point of a named root subgroup belongs to the elementary subgroup.

theorem TauCeti.E6Minuscule.elementarySubgroup_le_iff (A : Type v) [CommRing A] {H : Subgroup ↥(points A)} : elementarySubgroup A ≤ H ↔ ∀ (k : Fin 6 ⊕ Fin 6) (u : Multiplicative A), (rootSubgroupPoints k A) u ∈ H

A subgroup contains the elementary subgroup exactly when it contains every named root-subgroup point.

theorem TauCeti.E6Minuscule.weightTorusSubgroup_le_elementarySubgroup (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubgroup (coordinateLattice (Fin 27)).toAddSubgroup (coordinateLatticeBasis (Fin 27)) weightTable.weight ↑A ≤ UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ A

Over every commutative ring, the type-E₆ minuscule weight torus on the coordinate lattice is contained in the elementary group generated by the twelve positive and negative numbered simple root subgroups.

theorem TauCeti.E6Minuscule.weightTorusPoints_range_le_elementarySubgroup (A : Type v) [CommRing A] : (weightTorusPoints A).range ≤ elementarySubgroup A

Over every commutative ring, the range of the named type-E₆ minuscule weight-torus map is contained in the elementary subgroup generated by the named root-subgroup maps.

Scheme-theoretic generation

theorem TauCeti.E6Minuscule.definingIdeal_eq_kostantGeneratedDefiningIdeal : definingIdeal = UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27))

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

theorem TauCeti.E6Minuscule.groupScheme_eq_kostantGeneratedGroupScheme : groupScheme = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27))

The type-E₆ minuscule toral-closure group scheme is the group scheme generated by the twelve numbered root subgroups.

instance TauCeti.E6Minuscule.isIso_kostantGeneratedToToral : CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight)

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

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

Two homomorphisms out of the type-E₆ minuscule carrier agree when they agree on its twelve numbered root subgroups. The weight-torus hypothesis of groupScheme_hom_ext is redundant because the carrier is root-generated.

theorem TauCeti.E6Minuscule.groupScheme_hom_ext_of_rootSubgroup_iff {Y : CommHopfAlgCat ℤ} {f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)} : f = g ↔ ∀ (k : Fin 6 ⊕ Fin 6), CategoryTheory.CategoryStruct.comp (rootSubgroup k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup k) g

theorem TauCeti.E6Minuscule.baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal (A : Type v) [CommRing A] : baseChangeDefiningIdeal A = UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27)) A

After base change to any commutative ring, the transported type-E₆ minuscule 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.