Geometry of the upper-triangular subgroup scheme

The standard upper-triangular subgroup of GL_n is the weight parabolic for the strictly decreasing weights i ↦ n - 1 - i. This file specializes the general geometry of weight parabolics to establish smoothness and geometric connectedness of the upper-triangular group over an arbitrary commutative ring for smoothness and over a field for geometric connectedness.

Main declarations

• TauCeti.GeneralLinear.UpperTriangular.smoothCommHopfAlgProperty_coordinateHopfAlgebra: the upper-triangular coordinate Hopf algebra is smooth.
• TauCeti.GeneralLinear.UpperTriangular. geometricallyConnectedCommHopfAlgProperty_coordinateHopfAlgebra: the upper-triangular coordinate Hopf algebra is geometrically connected.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 12--13 and 17.
• T. A. Springer, Linear Algebraic Groups, Sections 6.2--6.3.

theorem TauCeti.GeneralLinear.UpperTriangular.smoothCommHopfAlgProperty_coordinateHopfAlgebra (n : ℕ) (R : Type u) [CommRing R] : smoothCommHopfAlgProperty R (coordinateHopfAlgebra R n)

The standard upper-triangular subgroup of GL_n is smooth over every commutative ring.

theorem TauCeti.GeneralLinear.UpperTriangular.geometricallyConnectedCommHopfAlgProperty_coordinateHopfAlgebra (n : ℕ) (k : Type u) [Field k] : geometricallyConnectedCommHopfAlgProperty k (coordinateHopfAlgebra k n)

The standard upper-triangular subgroup of GL_n is geometrically connected over every field.