Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLattice.FullWeight

The pinned Geck carrier is full-weight in the unimodular types #

The explicit Chevalley carrier TauCeti.DynkinType.geckGroupScheme of a valid Dynkin type is the smallest closed subgroup scheme of GLₙ over ℤ containing the divided-power exponential root subgroups of the numbered Chevalley generators together with the weight torus of Geck's admissible lattice. Whether it is a candidate for the simply connected form turns on one thing: the torus acts through the lattice generated by the weights of the representation, and that lattice has to be the whole weight lattice.

For the Geck lattice the generated lattice is the root lattice (TauCeti.DynkinType.span_range_geckWeight_eq_span_range_root), which is the whole weight lattice precisely in the three unimodular types E₈, F₄ and G₂. This file draws the consequence for the carrier's torus in those types, in both of the forms a consumer uses: the weight torus is a closed subgroup scheme of the carrier, and it is injective on points over every value algebra. Neither form is transported from the other, since the identification of the point group Fin rank → Aˣ with the scheme-theoretic points of the split torus is not available. The two general criteria live beside the carrier in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLattice.GroupScheme, and both are stated against the finite-ordinal weights TauCeti.DynkinType.geckWeightFin that the construction consumes, so the bridge to the merged spanning results is the reindexing lemma TauCeti.DynkinType.range_geckWeightFin.

Nothing here asserts that the Geck carrier is reductive, that its weight torus is a maximal torus, or that the carrier realizes the pinned root datum; those remain Layer 9 work. Neither does anything here bear on the other six valid diagrams, where the Geck weights generate only the proper root sublattice, so that a larger admissible lattice is needed before the same two statements can hold.

Main results #

References #

The identification of the character lattice of the torus with the lattice generated by the weights of an admissible lattice, and its role in separating the simply connected and adjoint forms, follow J. E. Humphreys, Linear Algebraic Groups, §27, and J. C. Jantzen, Representations of Algebraic Groups, II.1. The unimodularity of the E₈, F₄ and G₂ Cartan matrices is Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plates VII--IX.

This advances "Pinnings" and "Points over an algebraically closed field" in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, whose consumer is milestone L0 of TauCetiRoadmap/CFSGStatement/README.md, the pinned simply connected ambient group of a valid Lie-type index.

source
@[simp]
theorem TauCeti.DynkinType.range_geckWeightFin (t : DynkinType) (ht : t.Valid) :
Set.range (t.geckWeightFin ht) = Set.range (t.geckWeight ht)

Reindexing the Geck weights by a finite ordinal does not change the set of weights.

source
theorem TauCeti.DynkinType.span_range_geckWeightFin_eq_top_iff (t : DynkinType) (ht : t.Valid) :
Submodule.span ℤ (Set.range (t.geckWeightFin ht)) = ⊤ ↔ Submodule.span ℤ (Set.range (t.geckWeight ht)) = ⊤

The finite-ordinal Geck weights generate the character lattice exactly when the Geck weights do. This is the bridge between the weights the carrier is built from and the weights the spanning results are stated for.

The three unimodular types #

source
theorem TauCeti.DynkinType.geckTorusPoints_E8_injective (ht : E8.Valid) (A : CommAlgCat ℤ) :
Function.Injective ⇑(E8.geckTorusPoints ht A)

The weight torus of the pinned Geck carrier of type E₈ is injective on points.

source
theorem TauCeti.DynkinType.geckTorusPoints_F4_injective (ht : F4.Valid) (A : CommAlgCat ℤ) :
Function.Injective ⇑(F4.geckTorusPoints ht A)

The weight torus of the pinned Geck carrier of type F₄ is injective on points.

source
theorem TauCeti.DynkinType.geckTorusPoints_G2_injective (ht : G2.Valid) (A : CommAlgCat ℤ) :
Function.Injective ⇑(G2.geckTorusPoints ht A)

The weight torus of the pinned Geck carrier of type G₂ is injective on points.