Geometric connectedness of the special linear group

The coordinate Hopf algebra of SLₙ is geometrically connected over every field. The proof uses idempotents and algebraically closed points, so it does not depend on an irreducibility theorem for the generic determinant polynomial.

Over an algebraically closed extension, a finite-type coordinate algebra has no nontrivial idempotent once every idempotent has the same value at all rational points. Right translation reduces that constancy to generators of the ordinary special linear group. Mathlib's Matrix.SpecialLinearGroup.diagonal_transvection_induction' gives elementary transvections and two-coordinate diagonal matrices as generators. Their one-parameter families are defined over K[X] and K[T,T⁻¹]; these rings are domains, so an idempotent function on either family is constant. The argument includes ranks zero and one, where the special linear group is trivial.

Main declaration

• TauCeti.SpecialLinear.geometricallyConnectedCommHopfAlgProperty_coordinateHopfAlgebra: SLₙ is geometrically connected.

References

• J. S. Milne, Algebraic Groups (2017), §§2.a and 21.a.

theorem TauCeti.SpecialLinear.instIsScalarTowerPolynomial_tauCeti {k K : Type u} [Field k] [Field K] [Algebra k K] : IsScalarTower k K (Polynomial K)

theorem TauCeti.SpecialLinear.instIsScalarTowerLaurentPolynomial_tauCeti {k K : Type u} [Field k] [Field K] [Algebra k K] : IsScalarTower k K (LaurentPolynomial K)

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

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