Triviality of the generated type-E₇ subgroup's unipotent radical

Over an algebraically closed field, the subgroup of GL₅₆ generated by the fourteen numbered minuscule root subgroups and the weight torus has no nontrivial normal smooth unipotent closed subgroup, so its unipotent radical is trivial. Its faithful simple standard comodule supplies the representation-theoretic input, and its coordinate algebra is reduced because its generators are reduced. Thus, unlike the corresponding statements for the specialized integral carrier in TauCeti.Algebra.Lie.E7.Minuscule.UnipotentRadical, no reducedness hypothesis remains.

The result concerns the subgroup generated over the field, not the base change of the integral minuscule carrier. An identification between those two subgroup schemes is needed to transfer this conclusion to that carrier.

Main results

• TauCeti.E7Minuscule.eq_augmentation_generated_of_isNormal_of_smoothUnipotent: every normal smooth unipotent closed subgroup of the generated subgroup is trivial.
• TauCeti.E7Minuscule.unipotentRadicalDefiningIdeal_generated_eq_augmentation: the unipotent radical of the generated subgroup 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 normal-subgroup elimination follows the generated type-E₆ subgroup in TauCeti.Algebra.Lie.E6.Minuscule.Generated.UnipotentRadical, using the generic faithful-comodule theorem.

theorem TauCeti.E7Minuscule.eq_augmentation_generated_of_isNormal_of_smoothUnipotent (k : Type u) [Field k] [IsAlgClosed k] (I : HopfIdeal k ↑(generatedCoordinateHopfAlgebra k)) (hI : I.IsNormal) (hU : smoothUnipotentCommHopfAlgProperty k ((FiniteTypeCommHopfAlgCat.of k ↑(generatedCoordinateHopfAlgebra k)).quotient I)) : I = HopfIdeal.augmentation k ↑(generatedCoordinateHopfAlgebra k)

Every normal smooth unipotent closed subgroup of the subgroup generated over an algebraically closed field by the type-E₇ minuscule root subgroups and weight torus is trivial.

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

theorem TauCeti.E7Minuscule.unipotentRadicalDefiningIdeal_generated_eq_augmentation (k : Type u) [Field k] [IsAlgClosed k] : (FiniteTypeCommHopfAlgCat.of k ↑(generatedCoordinateHopfAlgebra k)).unipotentRadicalDefiningIdeal = HopfIdeal.augmentation k ↑(generatedCoordinateHopfAlgebra k)

The unipotent radical of the subgroup generated over an algebraically closed field by the type-E₇ minuscule root subgroups and weight torus is trivial.