Root generation of the Geck weight torus

The Geck carrier of a valid Dynkin type is built from its numbered positive and negative root subgroups and its split weight torus. The represented generators form sl₂ triples, and the root of the i-th raising generator is the i-th row of the Bourbaki Cartan matrix. So the generic coroot-generation theorem puts the entire weight torus in the subgroup generated by the root subgroups, over every commutative ring, as soon as every row of the Cartan matrix is a primitive integer vector: some integer combination of its entries is 1.

That hypothesis is checked here for the three types whose Geck carrier is full-weight, E₈, F₄ and G₂. Every row of the E₈ Cartan matrix contains an entry -1, at a neighbouring node of the diagram, and so does every row of the F₄ one, by the shared certificate TauCeti.sum_cartanMatrixF4_mul_typeF4CartanBezout. For G₂ the shared certificate TauCeti.sum_transpose_cartanMatrixG2_mul_typeG2CartanBezout supplies the coefficients: the long row (-3, 2) has no entry -1, and pairs to 1 with (-1, -1) instead.

This is a statement about the generated subgroups in the defining representation. Identifying that subgroup with all points of the Geck toral-closure scheme is a separate comparison.

Main results

• TauCeti.DynkinType.range_geckTorusPoints_le_geckElementarySubgroup: when every Cartan row is primitive, the Geck weight torus is contained in the elementary subgroup.
• TauCeti.DynkinType.geckTorusSubsystemSubgroup_univ_eq_geckElementarySubgroup: under the same hypothesis, adjoining the torus to all numbered root subgroups adds no elements.
• TauCeti.DynkinType.range_geckTorusPoints_le_geckElementarySubgroup_E8, range_geckTorusPoints_le_geckElementarySubgroup_F4 and range_geckTorusPoints_le_geckElementarySubgroup_G2, with the corresponding geckTorusSubsystemSubgroup_univ_eq_geckElementarySubgroup_E8, _F4 and _G2: the three full-weight Geck carriers.

References

• R. Steinberg, Lectures on Chevalley Groups, §3.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plates VII, VIII and IX, for the Cartan matrices.
• TauCeti.Algebra.Lie.E7.Minuscule.Generation, an earlier formal coroot-generation application.

Types whose Cartan rows are primitive

theorem TauCeti.DynkinType.range_geckTorusPoints_le_geckElementarySubgroup (t : DynkinType) (ht : t.Valid) (hrow : ∀ (i : Fin t.rank), ∃ (c : Fin t.rank → ℤ), ∑ j : Fin t.rank, t.cartanMatrix i j * c j = 1) (A : CommAlgCat ℤ) : (t.geckTorusPoints ht A).range ≤ t.geckElementarySubgroup ht A

The Geck weight torus lies in the elementary subgroup when every row of the Cartan matrix is primitive. Over every commutative ring, the torus is then contained in the subgroup generated by the numbered positive and negative simple-root subgroups.

theorem TauCeti.DynkinType.geckTorusSubsystemSubgroup_univ_eq_geckElementarySubgroup (t : DynkinType) (ht : t.Valid) (hrow : ∀ (i : Fin t.rank), ∃ (c : Fin t.rank → ℤ), ∑ j : Fin t.rank, t.cartanMatrix i j * c j = 1) (A : CommAlgCat ℤ) : t.geckTorusSubsystemSubgroup ht Set.univ A = t.geckElementarySubgroup ht A

Adjoining the Geck weight torus to every numbered simple-root subgroup adds nothing when every row of the Cartan matrix is primitive, over every commutative ring.

The full-weight types

theorem TauCeti.DynkinType.range_geckTorusPoints_le_geckElementarySubgroup_E8 (A : CommAlgCat ℤ) : (E8.geckTorusPoints valid_E8 A).range ≤ E8.geckElementarySubgroup valid_E8 A

Over every commutative ring, the type-E₈ Geck weight torus is contained in the elementary subgroup generated by the sixteen numbered positive and negative simple-root subgroups.

@[simp]

theorem TauCeti.DynkinType.geckTorusSubsystemSubgroup_univ_eq_geckElementarySubgroup_E8 (A : CommAlgCat ℤ) : E8.geckTorusSubsystemSubgroup valid_E8 Set.univ A = E8.geckElementarySubgroup valid_E8 A

Adding the type-E₈ Geck weight torus to every numbered simple-root subgroup does not enlarge the elementary subgroup over any commutative ring.

theorem TauCeti.DynkinType.range_geckTorusPoints_le_geckElementarySubgroup_F4 (A : CommAlgCat ℤ) : (F4.geckTorusPoints valid_F4 A).range ≤ F4.geckElementarySubgroup valid_F4 A

Over every commutative ring, the type-F₄ Geck weight torus is contained in the elementary subgroup generated by the eight numbered positive and negative simple-root subgroups.

@[simp]

theorem TauCeti.DynkinType.geckTorusSubsystemSubgroup_univ_eq_geckElementarySubgroup_F4 (A : CommAlgCat ℤ) : F4.geckTorusSubsystemSubgroup valid_F4 Set.univ A = F4.geckElementarySubgroup valid_F4 A

Adding the type-F₄ Geck weight torus to every numbered simple-root subgroup does not enlarge the elementary subgroup over any commutative ring.

theorem TauCeti.DynkinType.range_geckTorusPoints_le_geckElementarySubgroup_G2 (A : CommAlgCat ℤ) : (G2.geckTorusPoints valid_G2 A).range ≤ G2.geckElementarySubgroup valid_G2 A

Over every commutative ring, the type-G₂ Geck weight torus is contained in the elementary subgroup generated by the four numbered positive and negative simple-root subgroups.

@[simp]

theorem TauCeti.DynkinType.geckTorusSubsystemSubgroup_univ_eq_geckElementarySubgroup_G2 (A : CommAlgCat ℤ) : G2.geckTorusSubsystemSubgroup valid_G2 Set.univ A = G2.geckElementarySubgroup valid_G2 A

Adding the type-G₂ Geck weight torus to every numbered simple-root subgroup does not enlarge the elementary subgroup over any commutative ring.