The split torus in the Geck carrier

The represented Geck lattice of a valid Dynkin type t gives a morphism from the split torus of rank t.rank into the explicit Kostant toral-closure carrier TauCeti.DynkinType.geckGroupScheme. This file proves that the morphism is a closed immersion whenever the Geck weights span the full character lattice.

The proof is deliberately conditional in the general case. The Geck weights generate exactly the root lattice, which is usually a proper sublattice of the weight lattice used by the simply connected root datum. Consequently the represented torus need not embed in the Geck carrier for an arbitrary Dynkin type. The spanning condition is known for the three unimodular exceptional types E₈, F₄, and G₂, where the root and weight lattices coincide, and this file records the resulting closed immersions explicitly.

This supplies the intended closed split-torus component of a future pinning for those three types. Proving that it is maximal, constructing a compatible Borel, identifying the carrier as split reductive with the stated root datum, and constructing full-weight admissible lattices for the remaining types are separate Layer 9 steps in the ReductiveGroups roadmap. The resulting completed carriers are consumed by milestone L0 of the CFSGStatement roadmap.

Main declarations

• TauCeti.DynkinType.isClosedImmersion_geckWeightTorus_of_span_eq_top: the Geck weight torus is a closed immersion under the exact character-spanning hypothesis.
• TauCeti.DynkinType.geckWeightTorusClosedSubgroup: the corresponding closed subgroup scheme of the Geck carrier.
• TauCeti.DynkinType.isClosedImmersion_geckWeightTorus_E8, and the analogous F4 and G2 instances: the spanning hypothesis holds for the three unimodular exceptional types.

References

• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• R. W. Carter, Simple Groups of Lie Type, §§7.1 and 8.2.

theorem TauCeti.DynkinType.isClosedImmersion_geckWeightTorus_of_span_eq_top (t : DynkinType) (ht : t.Valid) (hwt : Submodule.span ℤ (Set.range (t.geckWeight ht)) = ⊤) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (t.geckWeightTorus ht).hom.hom)

Full character span makes the represented Geck torus a closed subgroup of the Geck carrier. The hypothesis is exact: it says that the characters occurring in the Geck lattice generate the character lattice of the source split torus.

noncomputable def TauCeti.DynkinType.geckWeightTorusClosedSubgroup (t : DynkinType) (ht : t.Valid) (hwt : Submodule.span ℤ (Set.range (t.geckWeight ht)) = ⊤) : ClosedSubgroupScheme (t.geckGroupScheme ht)

The closed split torus in the Geck carrier supplied by a full character-spanning family of Geck weights. No maximality or reductivity statement is part of this definition.

Equations

• t.geckWeightTorusClosedSubgroup ht hwt = TauCeti.ClosedSubgroupScheme.mk (t.geckWeightTorus ht)

@[simp]

theorem TauCeti.DynkinType.coe_geckWeightTorusClosedSubgroup (t : DynkinType) (ht : t.Valid) (hwt : Submodule.span ℤ (Set.range (t.geckWeight ht)) = ⊤) : have x := ⋯; ↑(t.geckWeightTorusClosedSubgroup ht hwt) = CategoryTheory.Subobject.mk (t.geckWeightTorus ht)

The underlying subobject of the closed Geck weight torus is represented by the defining weight-torus morphism.

The unimodular exceptional types

instance TauCeti.DynkinType.isClosedImmersion_geckWeightTorus_E8 (ht : E8.Valid) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (E8.geckWeightTorus ht).hom.hom)

The represented Geck weight torus of type E₈ is a closed immersion. The type E₈ roots span the full weight lattice because its Cartan matrix is unimodular.

instance TauCeti.DynkinType.isClosedImmersion_geckWeightTorus_F4 (ht : F4.Valid) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (F4.geckWeightTorus ht).hom.hom)

The represented Geck weight torus of type F₄ is a closed immersion.

instance TauCeti.DynkinType.isClosedImmersion_geckWeightTorus_G2 (ht : G2.Valid) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (G2.geckWeightTorus ht).hom.hom)

The represented Geck weight torus of type G₂ is a closed immersion.