Geometric reducedness of affine group schemes

This file compares geometric reducedness of a same-universe commutative Hopf algebra with Mathlib's scheme-theoretic GeometricallyReduced predicate on its Hopf spectrum.

Main declarations

• TauCeti.geometricallyReducedCommHopfAlg_iff_geometricallyReduced_hopfSpec: agreement of the coordinate-ring and scheme-theoretic predicates.

References

• J. S. Milne, Algebraic Groups (2017), for the geometric-reducedness terminology.

The comparison follows TauCeti.AlgebraicGeometry.AffineGroupScheme.Connected, especially its Hopf-spectrum comparison between the coordinate and scheme models.

This advances Layer 2, "Smoothness and dimension tools via Lie(G)", of the ReductiveGroups roadmap.

theorem TauCeti.geometricallyReducedCommHopfAlg_iff_geometricallyReduced_hopfSpec (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallyReducedCommHopfAlgProperty k H ↔ AlgebraicGeometry.GeometricallyReduced ((AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op H)).X.hom

Geometric reducedness agrees across the affine-group-scheme and coordinate-ring models. The structural morphism of a Hopf spectrum is geometrically reduced if and only if its coordinate algebra stays reduced after every extension K / k of the base field, meaning that H ⊗[k] K is reduced for every such K.