Generation of the doubled E₆ weight torus by root subgroups

The doubled type-E₆ carrier, the Kostant toral closure of V(ϖ₁) ⊕ V(ϖ₆) inside GL₅₄, is defined from its twelve numbered positive and negative simple-root subgroups together with its rank-six split 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, so the torus is redundant among the generators of the pointwise group.

The two inputs are the same as for the 27-dimensional carrier. The positive and negative generators at every node act on the rational doubled module as an sl₂ triple, by TauCeti.E6DoubledMinuscule.isSl2Triple_rep_serreRootGenerator. The root characters are those of the type-E₆ Serre algebra and do not depend on the representation, so the Bézout certificate TauCeti.E6.rootGeneratorWeight_sum_mul_cartanBezout shows that each of them is a primitive character of the weight torus. The generic coroot-generation theorem then puts every coordinate cocharacter, and hence every point of the weight torus, in the elementary group.

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 identify the elementary subgroup of points with all points of the carrier over a non-flat base.

Main results

• TauCeti.E6DoubledMinuscule.elementarySubgroup: the subgroup of carrier points generated by the ranges of the twelve named root-subgroup maps.
• TauCeti.E6DoubledMinuscule.elementarySubgroup_le_iff: its least-subgroup elimination principle.
• TauCeti.E6DoubledMinuscule.weightTorusSubgroup_le_elementarySubgroup and TauCeti.E6DoubledMinuscule.weightTorusPoints_range_le_elementarySubgroup: the weight torus lies in the elementary subgroup over every commutative ring, in the represented and the named form.
• TauCeti.E6DoubledMinuscule.definingIdeal_eq_kostantGeneratedDefiningIdeal: the integral toral-closure carrier is already the root-generated carrier.
• TauCeti.E6DoubledMinuscule.groupScheme_eq_kostantGeneratedGroupScheme and TauCeti.E6DoubledMinuscule.isIso_kostantGeneratedToToral: the corresponding group schemes agree and their canonical comparison is an isomorphism.
• baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal: the corresponding equality in the transported presentation over every commutative ring.
• TauCeti.E6DoubledMinuscule.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, §3.
• R. W. Carter, Simple Groups of Lie Type, §§6.4 and 7.1.

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

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

Equations

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

theorem TauCeti.E6DoubledMinuscule.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.E6DoubledMinuscule.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.E6DoubledMinuscule.weightTorusSubgroup_le_elementarySubgroup (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubgroup lattice.toAddSubgroup matrixBasis matrixWeight ↑A ≤ UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator A

The doubled type-E₆ weight torus lies in the elementary group. Over every commutative ring, the represented weight torus on the base-changed admissible lattice is contained in the elementary group generated by the twelve positive and negative numbered simple root subgroups.

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

The range of the named doubled type-E₆ weight-torus map lies in the elementary group. This is TauCeti.E6DoubledMinuscule.weightTorusSubgroup_le_elementarySubgroup read through the named carrier points.

Scheme-theoretic generation

theorem TauCeti.E6DoubledMinuscule.definingIdeal_eq_kostantGeneratedDefiningIdeal : definingIdeal = UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis

The full-weight doubled type-E₆ minuscule carrier is generated scheme-theoretically by its twelve numbered root subgroups. Adjoining the represented weight torus does not change the integral defining Hopf ideal.

theorem TauCeti.E6DoubledMinuscule.groupScheme_eq_kostantGeneratedGroupScheme : groupScheme = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis

The full-weight doubled type-E₆ minuscule carrier is the group scheme generated by its twelve numbered positive and negative simple root subgroups.

instance TauCeti.E6DoubledMinuscule.isIso_kostantGeneratedToToral : CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis matrixWeight)

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

theorem TauCeti.E6DoubledMinuscule.baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal (A : Type v) [CommRing A] : baseChangeDefiningIdeal A = UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIdeal (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis A

After base change to any commutative ring, the transported doubled 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.

theorem TauCeti.E6DoubledMinuscule.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 morphisms out of the doubled type-E₆ minuscule carrier agree as soon as they agree on its twelve numbered root subgroups. This drops the weight-torus hypothesis of TauCeti.E6DoubledMinuscule.groupScheme_hom_ext, which root generation of the carrier makes redundant.