The upper-unitriangular group is geometrically connected

The coordinate ring of the upper-unitriangular group U_m is the polynomial algebra on the strictly upper-triangular matrix entries. After every field extension it remains a polynomial algebra over a field, hence a domain. Its prime spectrum is therefore connected.

This file records geometric connectedness in both synchronized models used by the reductive-groups roadmap: as an object property of the coordinate Hopf algebra and as geometric connectedness of the structural morphism of the affine group scheme.

Main declarations

• TauCeti.UpperUnitriangular.geometricallyConnectedCommHopfAlgProperty_coordinateHopfAlgebra: the coordinate Hopf algebra of U_m is geometrically connected.
• TauCeti.UpperUnitriangular.geometricallyConnected_groupScheme: the structural morphism of the upper-unitriangular group scheme is geometrically connected.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, Section 2.4.

This supplies the connectedness of the standard ambient group in Layer 5, "Unipotent groups", of the ReductiveGroups roadmap. Together with its existing smoothness and unipotence, it completes the model required by the characterization of smooth connected unipotent groups as closed subgroups of some U_n.

theorem TauCeti.UpperUnitriangular.geometricallyConnectedCommHopfAlgProperty_coordinateHopfAlgebra (k : Type u) [Field k] (m : Type) [Fintype m] [LinearOrder m] : geometricallyConnectedCommHopfAlgProperty k (coordinateHopfAlgebra k m)

The upper-unitriangular coordinate Hopf algebra is geometrically connected. After every field extension its coordinate ring is a polynomial algebra over a field, hence a domain with connected prime spectrum.

theorem TauCeti.UpperUnitriangular.geometricallyConnected_groupScheme (k : Type u) [Field k] (m : Type) [Fintype m] [LinearOrder m] : AlgebraicGeometry.GeometricallyConnected (groupScheme k m).X.hom

The upper-unitriangular group scheme is geometrically connected over a field. This is the scheme-side form of geometric connectedness of its coordinate Hopf algebra.