Smoothness of the generated type-E₇ subgroup

Over every field, the fourteen numbered root subgroups and weight torus of the type-E₇ minuscule carrier generate a smooth closed subgroup of GL₅₆. Smoothness is one geometric property needed to recognize the generated subgroup as a pinned split group.

The generated subgroup is smooth and has reduced coordinate algebra over every field, with geometrically reduced additive root subgroups and a split torus as generators. This concerns the subgroup generated over the field; its identification with the specialization of the integral minuscule carrier is separate.

References

• J. E. Humphreys, Linear Algebraic Groups, §§26–27.
• J. S. Milne, Algebraic Groups (2017), §2.h.

theorem TauCeti.E7Minuscule.smoothCommHopfAlgProperty_generatedCoordinateHopfAlgebra (k : Type u) [Field k] : smoothCommHopfAlgProperty k (generatedCoordinateHopfAlgebra k)

The subgroup generated by the type-E₇ root subgroups and torus is smooth over every field, including imperfect fields and fields of characteristics two and three.

theorem TauCeti.E7Minuscule.isReduced_generatedCoordinateHopfAlgebra (k : Type u) [Field k] : IsReduced ↑(generatedCoordinateHopfAlgebra k)

The subgroup generated by the type-E₇ root subgroups and torus has reduced coordinate algebra over every field.