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

The integral toral closure of the twenty-six-dimensional module V(ϖ₄) of type F₄ is defined from its eight numbered positive and negative simple root subgroups together with its rank-four 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.F4ShortRoot.isSl2Triple_rep_serreRootGenerator, and every row of the type-F₄ Cartan matrix is a primitive integer vector by TauCeti.sum_cartanMatrixF4_mul_typeF4CartanBezout, each row having an entry -1 at a neighbouring node. 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.F4ShortRoot.weightTorusSubgroup_le_elementarySubgroup: the weight torus lies in the elementary subgroup over every commutative ring.
• TauCeti.F4ShortRoot.weightTorusSubsystemSubgroup_univ_eq_elementarySubgroup: adjoining the weight torus to all eight numbered root subgroups gives exactly the elementary subgroup.
• TauCeti.F4ShortRoot.definingIdeal_eq_kostantGeneratedDefiningIdeal: the integral toral closure is already cut out by the root subgroups alone.
• TauCeti.F4ShortRoot.groupScheme_eq_kostantGeneratedGroupScheme and TauCeti.F4ShortRoot.isIso_kostantGeneratedToToral: the carrier is the root-generated Kostant group scheme, and the canonical comparison between them is an isomorphism.
• TauCeti.F4ShortRoot.groupScheme_hom_ext_of_rootSubgroup: a morphism out of the carrier is determined by its restrictions to the eight 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.E7.Minuscule.Generation, the same coroot-generation argument run on the minuscule type-E₇ carrier, whose formal template this file follows with the type-F₄ Cartan rows and short-root weights in place of the type-E₇ data.

theorem TauCeti.F4ShortRoot.weightTorusSubgroup_le_elementarySubgroup (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubgroup lattice.toAddSubgroup latticeBasis DynkinType.f4ShortRootWeight ↑A ≤ UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator CartanMatrix.F₄.transpose) (serreH ℚ CartanMatrix.F₄.transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator A

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

theorem TauCeti.F4ShortRoot.weightTorusSubsystemSubgroup_univ_eq_elementarySubgroup (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup (serreRootGenerator CartanMatrix.F₄.transpose) (serreH ℚ CartanMatrix.F₄.transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.f4ShortRootWeight Set.univ A = UniversalEnvelopingAlgebra.kostantElementarySubgroup (serreRootGenerator CartanMatrix.F₄.transpose) (serreH ℚ CartanMatrix.F₄.transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator A

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

Scheme-theoretic generation

theorem TauCeti.F4ShortRoot.definingIdeal_eq_kostantGeneratedDefiningIdeal : definingIdeal = UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal (serreRootGenerator CartanMatrix.F₄.transpose) (serreH ℚ CartanMatrix.F₄.transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis

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

theorem TauCeti.F4ShortRoot.groupScheme_eq_kostantGeneratedGroupScheme : groupScheme = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme (serreRootGenerator CartanMatrix.F₄.transpose) (serreH ℚ CartanMatrix.F₄.transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis

The short-root type-F₄ integral toral closure is the group scheme generated by its eight numbered simple root subgroups.

instance TauCeti.F4ShortRoot.isIso_kostantGeneratedToToral : CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral (serreRootGenerator CartanMatrix.F₄.transpose) (serreH ℚ CartanMatrix.F₄.transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.f4ShortRootWeight)

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

theorem TauCeti.F4ShortRoot.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 short-root type-F₄ carrier agree as soon as they agree on its eight numbered root subgroups. This drops the weight-torus hypothesis of TauCeti.F4ShortRoot.groupScheme_hom_ext, which root generation of the carrier makes redundant.