Generation of the short-root type-G2 carrier by root subgroups

The integral toral closure of the seven-dimensional module V(ϖ₁) of type G₂ is defined from its four numbered positive and negative simple root subgroups together with its rank-two split weight torus. This file proves that the torus is redundant: over every commutative ring it already lies in the elementary subgroup generated by those root subgroups, and the integral carrier is therefore the root-generated Kostant group scheme.

The represented generators at each node form an sl₂ triple by TauCeti.G2ShortRoot.isSl2Triple_rep_serreRootGenerator, and the two rows of the Bourbaki type-G₂ Cartan matrix are primitive integer vectors by TauCeti.sum_transpose_cartanMatrixG2_mul_typeG2CartanBezout, the long row (-3, 2) through the Bezout coefficients (-1, -1) rather than through an entry -1. So each simple root is a primitive character of the weight torus, and the generic Kostant coroot-generation theorem writes every coordinate cocharacter, hence the whole torus, as a product of root-subgroup elements.

Testing that pointwise containment on the universal point of the torus, over the coordinate ring of the split torus itself, makes the torus redundant scheme-theoretically as well: the toral-closure defining Hopf ideal over ℤ equals the ideal cut out by the numbered root subgroups alone. This is an equality of integral carriers; it does not say that the subgroup generated anew over a base that is not flat over ℤ is the base change of the integral carrier, and in particular it does not identify the companion carrier generated over 𝔽₃.

Main results

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

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, with the type-G₂ Cartan rows and short-root weights in place of the type-E₇ data.

theorem TauCeti.G2ShortRoot.weightTorusSubgroup_le_elementarySubgroup (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubgroup lattice.toAddSubgroup latticeBasis weight ↑A ≤ UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator A

Over every commutative ring, the rank-two weight torus of the short-root type-G₂ module on the base-changed admissible lattice is contained in the elementary group generated by the four positive and negative numbered simple root subgroups.

theorem TauCeti.G2ShortRoot.weightTorusSubsystemSubgroup_univ_eq_elementarySubgroup (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis weight Set.univ A = UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator A

Over every commutative ring, adjoining the rank-two weight torus of the short-root type-G₂ module to all four numbered simple root subgroups does not enlarge their elementary subgroup.

Scheme-theoretic generation

theorem TauCeti.G2ShortRoot.IntegralToralClosure.definingIdeal_eq_kostantGeneratedDefiningIdeal : definingIdeal = UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis

The short-root type-G₂ integral toral closure is already generated scheme-theoretically by its four numbered root subgroups. Equivalently, adjoining the represented weight torus does not change the integral defining Hopf ideal.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.groupScheme_eq_kostantGeneratedGroupScheme : groupScheme = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis

The short-root type-G₂ integral toral closure is the group scheme generated by its four numbered simple root subgroups.

instance TauCeti.G2ShortRoot.IntegralToralClosure.isIso_kostantGeneratedToToral : CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis weight)

The canonical inclusion of the root-generated short-root type-G₂ carrier into its toral closure is an isomorphism.