Generation of the short-root type-G2 carrier over 𝔽₃ by root subgroups

The short-root type-G₂ carrier over 𝔽₃ is the closed subgroup scheme of GL₇ over 𝔽₃ generated by the reductions of the four numbered positive and negative simple root subgroups and of the rank-two weight torus of the integral toral closure. This file proves that the torus is redundant: the carrier is already the subgroup scheme generated over 𝔽₃ by the four root subgroups alone.

On points the statement is inherited from ℤ. A reduced generator is, as a matrix, the corresponding point of the integral carrier, and over every commutative ring the integral weight torus lies in the elementary subgroup generated by the integral root subgroups (TauCeti.G2ShortRoot.weightTorusSubgroup_le_elementarySubgroup). So over every 𝔽₃-algebra a weight-torus point of the carrier is a product of its root-subgroup points. Testing this on the universal point of the torus shows that the reduced torus kills the Hopf ideal cut out by the reduced root subgroups, which is the scheme-theoretic statement.

This is an equality of subgroup schemes generated over 𝔽₃, each with its maximal defining ideal there; it does not compare the carrier with the base change of the integral one beyond the containment already recorded. Its use is rigidity: a homomorphism out of the carrier is determined by the four root subgroups, with no condition on the torus, so an endomorphism such as the special isogeny in characteristic three is pinned by its equations on the numbered simple root subgroups alone.

Main results

• TauCeti.G2ShortRoot.PrimeField.weightTorusPoints_range_le_closure_rootSubgroupPoints: over every 𝔽₃-algebra the weight torus lies in the subgroup generated by the four root subgroups.
• TauCeti.G2ShortRoot.PrimeField.definingIdeal_eq_commonKernelHopfIdeal_generator_inl and TauCeti.G2ShortRoot.PrimeField.groupScheme_eq_generatedGroupScheme_generator_inl: the carrier is cut out by the root subgroups alone.
• TauCeti.G2ShortRoot.PrimeField.points_eq_generatedPointsSubgroup_generator_inl: the same statement on matrix-valued points.
• TauCeti.G2ShortRoot.PrimeField.groupScheme_hom_ext_of_rootSubgroup: homomorphisms out of the carrier agreeing on the four root subgroups are equal.

References

• R. Steinberg, Lectures on Chevalley Groups, §3.
• R. W. Carter, Simple Groups of Lie Type, §§6.4 and 7.1.

The argument follows the integral statement in TauCeti.Algebra.Lie.G2.ShortRoot.IntegralToralClosure.Generation.

theorem TauCeti.G2ShortRoot.PrimeField.weightTorusPoints_range_le_closure_rootSubgroupPoints (A : Type v) [CommRing A] [Algebra (ZMod 3) A] : (weightTorusPoints A).range ≤ Subgroup.closure (⋃ (k : Fin 2 ⊕ Fin 2), Set.range ⇑(rootSubgroupPoints k A))

The weight torus of the carrier over 𝔽₃ is generated by its root subgroups: over every 𝔽₃-algebra, each weight-torus point is a product of points of the four numbered positive and negative simple root subgroups.

theorem TauCeti.G2ShortRoot.PrimeField.definingIdeal_eq_commonKernelHopfIdeal_generator_inl : definingIdeal = CommHopfAlgCat.commonKernelHopfIdeal fun (k : Fin 2 ⊕ Fin 2) => generator (Sum.inl k)

The carrier over 𝔽₃ is cut out by its root subgroups alone: adjoining the weight torus to the four reduced root-subgroup generators does not change the defining Hopf ideal.

theorem TauCeti.G2ShortRoot.PrimeField.groupScheme_eq_generatedGroupScheme_generator_inl : groupScheme = GeneralLinear.generatedGroupScheme 7 fun (k : Fin 2 ⊕ Fin 2) => generator (Sum.inl k)

The short-root type-G₂ carrier over 𝔽₃ is generated by its four numbered root subgroups.

theorem TauCeti.G2ShortRoot.PrimeField.points_eq_generatedPointsSubgroup_generator_inl (A : Type v) [CommRing A] [Algebra (ZMod 3) A] : points A = GeneralLinear.generatedPointsSubgroup 7 (fun (k : Fin 2 ⊕ Fin 2) => generator (Sum.inl k)) A

The points of the carrier over 𝔽₃ are the points of the subgroup scheme generated by the four reduced root subgroups.

theorem TauCeti.G2ShortRoot.PrimeField.groupScheme_hom_ext_of_rootSubgroup {Y : CommHopfAlgCat (ZMod 3)} (f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧(ZMod 3)).obj (Opposite.op Y)) (hroot : ∀ (k : Fin 2 ⊕ Fin 2), CategoryTheory.CategoryStruct.comp (rootSubgroup k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup k) g) : f = g

Rigidity on the root subgroups alone. Two morphisms from the carrier over 𝔽₃ to an affine group scheme presented as hopfSpec Y agree when they agree on all four numbered simple root subgroups. Compare TauCeti.G2ShortRoot.PrimeField.groupScheme_hom_ext, which also asks for agreement on the weight torus.

theorem TauCeti.G2ShortRoot.PrimeField.groupScheme_hom_ext_of_rootSubgroup_iff {Y : CommHopfAlgCat (ZMod 3)} {f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧(ZMod 3)).obj (Opposite.op Y)} : f = g ↔ ∀ (k : Fin 2 ⊕ Fin 2), CategoryTheory.CategoryStruct.comp (rootSubgroup k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup k) g