Smoothness and connectedness of the general linear group

The determinant localization defining the coordinate Hopf algebra of GL_n is smooth. It is also an integral domain whenever the base ring is an integral domain. After base change to any field it therefore has connected prime spectrum, proving geometric connectedness over a field.

Main declarations

• TauCeti.GeneralLinear.instSmoothCoordinateHopfAlgebra: O(GL_n) is smooth.
• TauCeti.GeneralLinear.instIsDomainCoordinateHopfAlgebra: O(GL_n) is an integral domain over an integral domain.
• TauCeti.GeneralLinear.geometricallyConnectedCommHopfAlgProperty_coordinateHopfAlgebra: GL_n is geometrically connected.

instance TauCeti.GeneralLinear.instSmoothCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : Algebra.Smooth R ↑(coordinateHopfAlgebra R n)

The coordinate Hopf algebra of GL_n is smooth over its base ring.

instance TauCeti.GeneralLinear.instIsDomainCoordinateHopfAlgebra (R : Type u) [CommRing R] [IsDomain R] (n : ℕ) : IsDomain ↑(coordinateHopfAlgebra R n)

Over an integral domain, the coordinate Hopf algebra of GL_n is an integral domain.

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

The coordinate Hopf algebra of GL_n is geometrically connected over every field.