Smoothness and connectedness of tori

A torus becomes split over an algebraic closure. The base-change descent theorems transport both geometric properties back to the ground field. Finally, geometric reducedness of a finite-type affine group over a field implies smoothness, so every torus is smooth.

Main declarations

• TauCeti.torusCommHopfAlgProperty.geometricallyConnected: every torus is geometrically connected.
• TauCeti.torusCommHopfAlgProperty.geometricallyReduced: every torus is geometrically reduced.
• TauCeti.torusCommHopfAlgProperty.smooth: every torus is smooth.

References

• J. S. Milne, Algebraic Groups (2017), Definitions 12.14 and 12.17.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.

This completes the smoothness and geometric-connectedness part of Layer 4, "Tori: split and non-split", of the ReductiveGroups roadmap. The character lattice of a non-split torus with its Galois action remains to be constructed.

theorem TauCeti.torusCommHopfAlgProperty.geometricallyConnected (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : torusCommHopfAlgProperty k H) : geometricallyConnectedCommHopfAlgProperty k H.obj

Every torus over a field is geometrically connected.

theorem TauCeti.torusCommHopfAlgProperty.geometricallyReduced (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : torusCommHopfAlgProperty k H) : geometricallyReducedCommHopfAlgProperty k H.obj

Every torus over a field is geometrically reduced.

theorem TauCeti.torusCommHopfAlgProperty.smooth (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : torusCommHopfAlgProperty k H) : smoothCommHopfAlgProperty k H.obj

Every torus over a field is smooth.