Geometric connectedness and reducedness of diagonalizable groups

The coordinate ring of a diagonalizable group is a group algebra. When its character group has the unique-product property, this group algebra is a domain over every field, so it is reduced and has connected prime spectrum. In particular, this applies to the finite-rank free character group of every split torus.

Main declarations

• TauCeti.DiagonalizableGroup.connectedSpace_primeSpectrum_coordinateRing: a diagonalizable coordinate ring that is a domain has connected prime spectrum.
• TauCeti.DiagonalizableGroup.connectedSpace_primeSpectrum_baseChange_coordinateRing: the base-changed coordinate ring has connected prime spectrum when K[G] is a domain.
• TauCeti.DiagonalizableGroup.geometricallyConnected_coordinateRing: the coordinate ring of a unique-product diagonalizable group is geometrically connected.
• TauCeti.DiagonalizableGroup.geometricallyReduced_coordinateRing: the coordinate ring of a unique-product diagonalizable group is geometrically reduced.

References

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

This establishes the geometric connectedness and reducedness of the split-torus case in Layer 4, "Tori: split and non-split", of the ReductiveGroups roadmap.

theorem TauCeti.DiagonalizableGroup.connectedSpace_primeSpectrum_coordinateRing (K : Type v) [CommRing K] (G : FGCommGrpCat) [IsDomain (MonoidAlgebra K ↑G)] : ConnectedSpace (PrimeSpectrum ↑(coordinateRing K G).obj)

The coordinate ring of a diagonalizable group has connected prime spectrum when it is a domain.

theorem TauCeti.DiagonalizableGroup.connectedSpace_primeSpectrum_baseChange_coordinateRing (k : Type u) (K : Type v) [CommRing k] [CommRing K] [Algebra k K] (G : FGCommGrpCat) [IsDomain (MonoidAlgebra K ↑G)] : ConnectedSpace (PrimeSpectrum ↑(CommHopfAlgCat.baseChange (coordinateRing k G).obj))

The base change of a diagonalizable-group coordinate ring has connected prime spectrum when the resulting group algebra is a domain.

theorem TauCeti.DiagonalizableGroup.geometricallyConnected_coordinateRing (k : Type u) [Field k] (G : FGCommGrpCat) [UniqueProds ↑G] : geometricallyConnectedCommHopfAlgProperty k (coordinateRing k G).obj

The coordinate Hopf algebra of a unique-product diagonalizable group is geometrically connected.

theorem TauCeti.DiagonalizableGroup.geometricallyReduced_coordinateRing (k : Type u) [Field k] (G : FGCommGrpCat) [UniqueProds ↑G] : geometricallyReducedCommHopfAlgProperty k (coordinateRing k G).obj

The coordinate Hopf algebra of a unique-product diagonalizable group is geometrically reduced.