The unipotent radical of the generated short-root type-G2 subgroup

Let k be an algebraically closed field of characteristic three, and let G be the closed subgroup of GL₇ over k generated by the scalar extensions of the four numbered simple root subgroups and of the weight torus of the short-root type-G₂ carrier over 𝔽₃. Then every normal smooth unipotent closed subgroup of G is trivial; consequently the unipotent radical of G is trivial.

The mathematical input is the standard seven-dimensional representation of G. It is faithful, and simple by TauCeti.G2ShortRoot.PrimeField.instIsSimpleOrderGeneratedSubcomodule, hence completely reducible. The generic normal-unipotent elimination theorem TauCeti.HopfIdeal.eq_augmentation_of_isNormal_of_smoothUnipotent_of_isFaithful then applies: normality makes the fixed vectors of a smooth unipotent closed subgroup an ambient subcomodule, Kolchin's fixed-vector theorem and simplicity force the subgroup to act trivially, and faithfulness identifies its defining ideal with the augmentation ideal. The reducedness that theorem requires is TauCeti.G2ShortRoot.PrimeField.isReduced_generatedCoordinateHopfAlgebra.

The generated subgroup is also smooth and geometrically connected, by smoothCommHopfAlgProperty_generatedCoordinateHopfAlgebra and geometricallyConnectedCommHopfAlgProperty_generatedCoordinateHopfAlgebra in the namespace TauCeti.G2ShortRoot.PrimeField.

Main declarations

In the namespace TauCeti.G2ShortRoot.PrimeField:

• eq_augmentation_of_isNormal_of_smoothUnipotent: every normal smooth unipotent closed subgroup of G is trivial.
• unipotentRadicalDefiningIdeal_eq_augmentation: the unipotent radical of G is trivial.

References

• J. E. Humphreys, Linear Algebraic Groups, §§19 and 26.
• J. C. Jantzen, Representations of Algebraic Groups, I.2 and II.2.

The statements follow TauCeti.Algebra.Lie.E6.Minuscule.UnipotentRadical.

theorem TauCeti.G2ShortRoot.PrimeField.eq_augmentation_of_isNormal_of_smoothUnipotent (k : Type u) [Field k] [Algebra (ZMod 3) k] [IsAlgClosed k] (I : HopfIdeal k ↑(generatedCoordinateHopfAlgebra k)) (hI : I.IsNormal) (hU : smoothUnipotentCommHopfAlgProperty k ((finiteTypeGeneratedCoordinateHopfAlgebra k).quotient I)) : I = HopfIdeal.augmentation k ↑(generatedCoordinateHopfAlgebra k)

Every normal smooth unipotent closed subgroup of the generated short-root type-G₂ subgroup is trivial, over an algebraically closed field of characteristic three.

The conclusion is stated contravariantly: the subgroup's defining Hopf ideal is the augmentation ideal of the generated subgroup's coordinate algebra.

theorem TauCeti.G2ShortRoot.PrimeField.unipotentRadicalDefiningIdeal_eq_augmentation (k : Type u) [Field k] [Algebra (ZMod 3) k] [IsAlgClosed k] : (finiteTypeGeneratedCoordinateHopfAlgebra k).unipotentRadicalDefiningIdeal = HopfIdeal.augmentation k ↑(generatedCoordinateHopfAlgebra k)

The unipotent radical of the generated short-root type-G₂ subgroup is trivial, over an algebraically closed field of characteristic three.