Closed generators of the short-root G₂ carrier over 𝔽₃

The four numbered simple-root maps and the weight-torus map into the prime-field short-root carrier are closed immersions. Thus their parametrizations identify closed copies of the additive group and of the rank-two split torus inside the carrier, including on nonreduced value algebras. This supplies the closed-subgroup condition needed to use these maps as root subgroups and as a candidate maximal torus in a pinned-group comparison.

Surjectivity of the generating coordinate maps follows from the integral root-matrix calculations and the fact that the seven weights span the full character lattice. Scalar extension preserves that surjectivity, without requiring flatness of ℤ → 𝔽₃. Factoring through the separately generated prime-field carrier preserves it as well.

The integral root-coordinate calculation is from TauCeti.Algebra.Lie.G2.ShortRoot.IntegralToralClosure.Basic, and the weight-span theorem is from TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.G2.ShortRootWeight. The organization follows TauCeti.Algebra.Lie.E7.Minuscule.ClosedGenerators, using the general generated-subgroup closed-immersion criterion rather than a new presentation of the carrier.

Main declarations

• TauCeti.G2ShortRoot.PrimeField.generator_surjective: each generating coordinate map is surjective.
• TauCeti.G2ShortRoot.PrimeField.isClosedImmersion_rootSubgroup: the numbered root-subgroup maps are closed immersions.
• TauCeti.G2ShortRoot.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.G2ShortRoot.PrimeField.generator_surjective (j : (Fin 2 ⊕ Fin 2) ⊕ Unit) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (generator j))

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

instance TauCeti.G2ShortRoot.PrimeField.isClosedImmersion_rootSubgroup (k : Fin 2 ⊕ Fin 2) : 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.G2ShortRoot.PrimeField.isClosedImmersion_weightTorus : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left weightTorus.hom.hom)

The rank-two 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.