The character lattice generated by the pinned Geck weights

For a valid Dynkin type t, the standard coordinates of Geck's representation have weight zero on the Cartan coordinates and have the roots of t as their remaining weights. This file records that fact integrally and identifies the lattice generated by those weights with the root lattice inside the character lattice of TauCeti.DynkinType.simplyConnectedRootDatum.

That distinction matters for the Chevalley--Demazure construction. The torus in the explicit Geck carrier acts through the lattice generated by the representation's weights. In general this is only the root lattice, so the carrier is a candidate for the adjoint form rather than the simply connected form needed by milestone L0 of the CFSG statement roadmap. The root lattice is the whole character lattice exactly at a unimodular Cartan matrix, which by TauCeti.DynkinType.span_range_root_eq_top_iff happens exactly in the types E₈, F₄ and G₂. The weights of the existing Geck admissible lattice therefore generate the full character lattice in precisely those three exceptional cases, and a proper sublattice of it in every other valid type.

This file proves only the lattice statement. Identifying the resulting group scheme as split reductive with the pinned root datum, and constructing suitable admissible lattices for the other types, remain Layer 9 work in the reductive-groups roadmap.

Main results

• TauCeti.DynkinType.geckWeight_inl_eq_zero: a Cartan coordinate of the Geck module has weight zero.
• TauCeti.DynkinType.geckWeight_inr_eq_root: a root coordinate of the Geck module has exactly the corresponding integral root as its weight.
• TauCeti.DynkinType.span_range_geckWeight_eq_span_range_root: the Geck weights generate the root lattice.
• TauCeti.DynkinType.span_range_geckWeight_eq_top_iff: they generate the full character lattice exactly in the types E₈, F₄ and G₂.
• TauCeti.DynkinType.span_range_geckWeight_E8_eq_top, and the analogous F4 and G2 results: the three cases of that classification in which the span is full.

References

The use of an admissible lattice and its weights follows J. E. Humphreys, Linear Algebraic Groups, §27. The determinants of the Cartan matrices and the identification of the root and weight lattices follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plates VII--IX.

theorem TauCeti.DynkinType.geckWeight_inl_eq_zero (t : DynkinType) (ht : t.Valid) (x : ↥(t.rationalBase ht).support) : t.geckWeight ht (Sum.inl x) = 0

A Cartan coordinate of the pinned Geck module has weight zero.

theorem TauCeti.DynkinType.geckWeight_inr_eq_root (t : DynkinType) (ht : t.Valid) (k : Fin t.numRoots) : t.geckWeight ht (Sum.inr k) = (t.simplyConnectedRootDatum ht).root k

A root coordinate of the pinned Geck module has the corresponding integral root as its weight.

theorem TauCeti.DynkinType.span_range_geckWeight_eq_span_range_root (t : DynkinType) (ht : t.Valid) : Submodule.span ℤ (Set.range (t.geckWeight ht)) = Submodule.span ℤ (Set.range ⇑(t.simplyConnectedRootDatum ht).root)

The weights of the pinned Geck representation generate exactly the root lattice. Its Cartan coordinates have weight zero, while its remaining coordinates carry every root once.

@[simp]

theorem TauCeti.DynkinType.span_range_geckWeight_eq_top_iff (t : DynkinType) (ht : t.Valid) : Submodule.span ℤ (Set.range (t.geckWeight ht)) = ⊤ ↔ t = E8 ∨ t = F4 ∨ t = G2

The pinned Geck weights generate the full character lattice exactly in the types E₈, F₄ and G₂. They generate the root lattice, which is the whole character lattice precisely at a unimodular Cartan matrix. In every other valid type they generate a proper sublattice, so the carrier built from the Geck admissible lattice is not the simply connected form there.

theorem TauCeti.DynkinType.span_range_geckWeight_E8_eq_top (ht : E8.Valid) : Submodule.span ℤ (Set.range (E8.geckWeight ht)) = ⊤

The pinned Geck weights of type E₈ generate the full character lattice. This is the unimodularity of the type E₈ Cartan matrix read in the representation used by the explicit Chevalley carrier.

theorem TauCeti.DynkinType.span_range_geckWeight_F4_eq_top (ht : F4.Valid) : Submodule.span ℤ (Set.range (F4.geckWeight ht)) = ⊤

The pinned Geck weights of type F₄ generate the full character lattice.

theorem TauCeti.DynkinType.span_range_geckWeight_G2_eq_top (ht : G2.Valid) : Submodule.span ℤ (Set.range (G2.geckWeight ht)) = ⊤

The pinned Geck weights of type G₂ generate the full character lattice.