Reductivity of the short-root G₂ carrier over 𝔽₃

The short-root type-G₂ carrier over 𝔽₃ is the closed subgroup scheme of GL₇ generated by four numbered root subgroups and a rank-two weight torus. It is reductive: smooth, geometrically connected, and with no nontrivial connected normal smooth unipotent subgroup after extension to an algebraic closure.

The geometric fibre is identified with the subgroup generated after scalar extension by TauCeti.G2ShortRoot.PrimeField.coordinateHopfAlgebraGeneratedIso. The latter's faithful simple seven-dimensional standard representation eliminates normal smooth unipotent subgroups, as proved in TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.Generated.UnipotentRadical.

This proves reductivity of the constructed carrier. Identification with the pinned simply connected group of type G₂ also requires maximal-torus and root-datum recognition.

References

• J. S. Milne, Algebraic Groups (2017), §2.h and Chapter 19.
• J. E. Humphreys, Linear Algebraic Groups, §§19 and 26.
• J. C. Jantzen, Representations of Algebraic Groups, I.2 and II.2.

@[reducible, inline]

noncomputable abbrev TauCeti.G2ShortRoot.PrimeField.finiteTypeCarrierAlgebra : FiniteTypeCommHopfAlgCat (ZMod 3)

The prime-field short-root type-G₂ carrier as a finite-type commutative Hopf algebra.

Equations

• TauCeti.G2ShortRoot.PrimeField.finiteTypeCarrierAlgebra = { obj := TauCeti.G2ShortRoot.PrimeField.carrierAlgebra, property := TauCeti.G2ShortRoot.PrimeField.finiteTypeCarrierAlgebra._proof_1 }

theorem TauCeti.G2ShortRoot.PrimeField.reductiveCommHopfAlgProperty_finiteTypeCarrierAlgebra : reductiveCommHopfAlgProperty (ZMod 3) finiteTypeCarrierAlgebra

The short-root type-G₂ carrier over 𝔽₃ is reductive: smooth and geometrically connected, with trivial geometric unipotent radical.