Generation of the short-root type-F4 carrier over 𝔽₂ by root subgroups

The short-root type-F₄ carrier over 𝔽₂ is the closed subgroup scheme of GL₂₆ over 𝔽₂ generated by the reductions of the eight numbered positive and negative simple root subgroups and of the rank-four weight torus of the integral short-root carrier. This file proves that the torus is redundant: the carrier is already the subgroup scheme generated over 𝔽₂ by the eight 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.F4ShortRoot.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 eight root subgroups, with no condition on the torus, so an endomorphism such as the special isogeny in characteristic two is pinned by its equations on the numbered simple root subgroups alone.

Main results

• TauCeti.F4ShortRoot.PrimeField.weightTorusPoints_range_le_closure_rootSubgroupPoints: over every 𝔽₂-algebra the weight torus lies in the subgroup generated by the eight root subgroups.
• TauCeti.F4ShortRoot.PrimeField.definingIdeal_eq_commonKernelHopfIdeal_generator_inl and TauCeti.F4ShortRoot.PrimeField.groupScheme_eq_generatedGroupScheme_generator_inl: the carrier is cut out by the root subgroups alone.
• TauCeti.F4ShortRoot.PrimeField.points_eq_generatedPointsSubgroup_generator_inl: the same statement on matrix-valued points.
• TauCeti.F4ShortRoot.PrimeField.groupScheme_hom_ext_of_rootSubgroup: homomorphisms out of the carrier agreeing on the eight 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.F4.ShortRoot.Generation, and the organization follows the type-G₂ sibling TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.Generation.

theorem TauCeti.F4ShortRoot.PrimeField.weightTorusPoints_range_le_closure_rootSubgroupPoints (A : Type v) [CommRing A] [Algebra (ZMod 2) A] : (weightTorusPoints A).range ≤ Subgroup.closure (⋃ (k : Fin 4 ⊕ Fin 4), 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 eight numbered positive and negative simple root subgroups.

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

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

theorem TauCeti.F4ShortRoot.PrimeField.groupScheme_eq_generatedGroupScheme_generator_inl : groupScheme = GeneralLinear.generatedGroupScheme 26 fun (k : Fin 4 ⊕ Fin 4) => generator (Sum.inl k)

The short-root type-F₄ carrier over 𝔽₂ is generated by its eight numbered root subgroups.

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

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

theorem TauCeti.F4ShortRoot.PrimeField.groupScheme_hom_ext_of_rootSubgroup {Y : CommHopfAlgCat (ZMod 2)} (f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧(ZMod 2)).obj (Opposite.op Y)) (hroot : ∀ (k : Fin 4 ⊕ Fin 4), 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 eight numbered simple root subgroups. Compare TauCeti.F4ShortRoot.PrimeField.groupScheme_hom_ext, which also asks for agreement on the weight torus.

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