Connectedness of the generated type-E₇ subgroup #
The numbered root subgroups and weight torus of the type-E₇ minuscule carrier generate a
geometrically connected closed subgroup over an algebraically closed field. The coordinate
algebras of the generators have connected spectra, and the closed subgroup they generate
inherits this property. This is a geometric input to recognizing the explicit carrier as a
pinned split group of type E₇.
The integral carrier is known to contain the generated subgroup. Its identification with the generated subgroup after base change is a separate question.
References #
- J. S. Milne, Algebraic Groups (2017), Propositions 2.37 and 2.48.
TauCeti.Algebra.AlgebraicGroup.Connected.Generated, connectedness of common-kernel quotients.
theorem
TauCeti.E7Minuscule.geometricallyConnectedCommHopfAlgProperty_generatedCoordinateHopfAlgebra
(k : Type u)
[Field k]
[IsAlgClosed k]
:
The closed subgroup generated by the type-E₇ numbered root subgroups and weight torus is
geometrically connected over an algebraically closed field.