The centralizer of the short-root G₂ weight torus

The diagonal points of the prime-field short-root carrier are exactly its weight-torus points, over every commutative 𝔽₃-algebra. Over an infinite field, this torus is its own centralizer in the carrier's point group. Consequently no larger commutative subgroup of points contains it.

The seven distinct weights force a commuting matrix to be diagonal; preservation of the cross product then restricts its diagonal to the rank-two weight torus. The pointwise centralizer calculation is the input for maximality of the torus as a closed subgroup scheme. No identification with a pinned simply connected group is asserted here.

References

• J. E. Humphreys, Linear Algebraic Groups, §16.1 and §26.3.
• The point-group argument follows TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Symplectic.Diagonal.Centralizer.
• Tensor invariance comes from TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.PreservesTensors.
• Character separation uses TauCeti.weightChar_injective from TauCeti.LinearAlgebra.Basis.DiagonalTorus.Basic.

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.exists_weightTorusPoints_eq_iff_isDiag {A : Type v} [CommRing A] [Algebra (ZMod 3) A] (g : ↥(points A)) : (∃ (s : Fin 2 → Aˣ), (weightTorusPoints A) s = g) ↔ (↑↑g).IsDiag

A point of the short-root carrier lies in the weight torus exactly when its matrix is diagonal. This characterization also holds over nonreduced value algebras.

theorem TauCeti.G2ShortRoot.PrimeField.centralizer_range_weightTorusPoints {k : Type v} [Field k] [Algebra (ZMod 3) k] [Infinite k] : Subgroup.centralizer ↑(weightTorusPoints k).range = (weightTorusPoints k).range

Over an infinite field of characteristic three, the weight torus is its own centralizer in the short-root carrier's point group.

theorem TauCeti.G2ShortRoot.PrimeField.eq_range_weightTorusPoints_of_le_of_isMulCommutative {k : Type v} [Field k] [Algebra (ZMod 3) k] [Infinite k] (H : Subgroup ↥(points k)) [IsMulCommutative ↥H] (hH : (weightTorusPoints k).range ≤ H) : H = (weightTorusPoints k).range

No commutative subgroup of short-root carrier points over an infinite field properly contains the weight torus.