Closed generators of the short-root F₄ carrier over 𝔽₂

The eight numbered simple-root maps and the weight-torus map into the prime-field short-root carrier are closed immersions. Their parametrizations therefore identify closed copies of the additive group and of the rank-four split torus inside the carrier, over nonreduced value algebras as well as fields. These are the closed-subgroup inputs needed to recognize the carrier's torus and root datum in a pinned-group comparison.

The coordinate maps of the integral root subgroups are surjective by their explicit matrix coordinates, while the twenty-six short-root weights span the full character lattice. Base change to 𝔽₂ preserves both surjections without a flatness hypothesis, and factoring the resulting maps through the subgroup generated over 𝔽₂ preserves them again.

The integral root-coordinate calculation is in TauCeti.Algebra.Lie.F4.ShortRoot.Carrier; the weight-span theorem is in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.F4.ShortRootWeight.Basic. The organization follows the prime-field short-root type-G₂ carrier.

Main declarations

• TauCeti.F4ShortRoot.PrimeField.generator_surjective: every generating coordinate map is surjective.
• TauCeti.F4ShortRoot.PrimeField.isClosedImmersion_rootSubgroup: the numbered root-subgroup maps are closed immersions.
• TauCeti.F4ShortRoot.PrimeField.isClosedImmersion_weightTorus: the weight-torus map is a closed immersion.

References

• J. E. Humphreys, Linear Algebraic Groups, §26.
• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.

theorem TauCeti.F4ShortRoot.PrimeField.generator_surjective (j : (Fin 4 ⊕ Fin 4) ⊕ Unit) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (generator j))

Each reduced generating coordinate map is surjective: the eight simple-root generators parametrize closed copies of 𝔾ₐ, and the torus generator parametrizes a closed split torus.

instance TauCeti.F4ShortRoot.PrimeField.isClosedImmersion_rootSubgroup (k : Fin 4 ⊕ Fin 4) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (rootSubgroup k).hom.hom)

Every numbered positive or negative simple-root map is a closed immersion into the short-root carrier over 𝔽₂.

instance TauCeti.F4ShortRoot.PrimeField.isClosedImmersion_weightTorus : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left weightTorus.hom.hom)

The rank-four weight-torus map is a closed immersion into the short-root carrier over 𝔽₂. This asserts that it is a split torus subgroup, without asserting maximality.