Connectedness of the generated short-root type-F₄ carrier

After scalar extension to an algebraically closed field of characteristic two, the eight numbered root subgroups and the rank-four weight torus generate a geometrically connected closed subgroup of GL₂₆. Their coordinate algebras are scalar extensions of a polynomial algebra and a Laurent polynomial algebra, respectively, so each has connected spectrum. The common-kernel construction then preserves connectedness of the generated subgroup.

Since this generated subgroup is the scalar extension of the prime-field carrier, the carrier itself is geometrically connected (TauCeti.F4ShortRoot.PrimeField.geometricallyConnectedCommHopfAlgProperty_quotient_definingIdeal).

References

• J. S. Milne, Algebraic Groups (2017), Propositions 2.37 and 2.48.

The formal argument follows TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.Generated.Connected.

theorem TauCeti.F4ShortRoot.PrimeField.geometricallyConnectedCommHopfAlgProperty_generatedCoordinateHopfAlgebra (k : Type u) [Field k] [Algebra (ZMod 2) k] [IsAlgClosed k] : geometricallyConnectedCommHopfAlgProperty k (generatedCoordinateHopfAlgebra k)

The closed subgroup generated by the scalar-extended short-root type-F₄ root subgroups and weight torus is geometrically connected over an algebraically closed field.

theorem TauCeti.F4ShortRoot.PrimeField.geometricallyConnectedCommHopfAlgProperty_quotient_definingIdeal : geometricallyConnectedCommHopfAlgProperty (ZMod 2) (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) definingIdeal)

The short-root type-F₄ carrier over 𝔽₂ is geometrically connected.