Geometric reducedness of commutative Hopf algebras

For a commutative Hopf algebra H over a field k, geometric reducedness means that every field extension K / k in their common universe gives a reduced coordinate ring H ⊗[k] K. The base field and Hopf algebra may live in independent universes.

Mathlib's Algebra.IsGeometricallyReduced tests the base change to algebraic closures of residue fields. Its source currently lists equivalence with reducedness after arbitrary field extension as a TODO. The all-extension condition used here implies Mathlib's existing algebra predicate.

Main declarations

• TauCeti.geometricallyReducedCommHopfAlgProperty: geometric reducedness after every field extension.
• TauCeti.geometricallyReducedCommHopfAlgProperty.isGeometricallyReduced: comparison with Mathlib's algebra predicate.
• TauCeti.geometricallyReducedCommHopfAlgProperty.isReduced: reducedness over the base field.
• The ObjectProperty.IsClosedUnderIsomorphisms instance records invariance under Hopf-algebra isomorphisms.

References

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

The object-property organization follows TauCeti.Algebra.AlgebraicGroup.Connected.CommHopfAlgCat with reducedness replacing connectedness.

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

def TauCeti.geometricallyReducedCommHopfAlgProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (CommHopfAlgCat k)

A commutative Hopf algebra over a field is geometrically reduced when its coordinate ring remains reduced after every extension of the base field.

Equations

• TauCeti.geometricallyReducedCommHopfAlgProperty k H = ∀ (K : Type (max ?u.2 ?u.1)) [inst : Field K] [inst_1 : Algebra k K], IsReduced (TensorProduct k (↑H) K)

@[simp]

theorem TauCeti.geometricallyReducedCommHopfAlgProperty_iff (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallyReducedCommHopfAlgProperty k H ↔ ∀ (K : Type (max u v)) [inst : Field K] [inst_1 : Algebra k K], IsReduced (TensorProduct k (↑H) K)

Membership in the geometrically reduced commutative-Hopf-algebra object property.

theorem TauCeti.geometricallyReducedCommHopfAlgProperty.isGeometricallyReduced {k : Type u} [Field k] {H : CommHopfAlgCat k} (hH : geometricallyReducedCommHopfAlgProperty k H) : Algebra.IsGeometricallyReduced k ↑H

The all-extension coordinate condition implies Mathlib's algebraic geometric-reducedness predicate, which over a field tests the base change to an algebraic closure.

theorem TauCeti.geometricallyReducedCommHopfAlgProperty.isReduced {k : Type u} [Field k] {H : CommHopfAlgCat k} (hH : geometricallyReducedCommHopfAlgProperty k H) : IsReduced ↑H

A geometrically reduced commutative Hopf algebra has reduced coordinate ring over its base field.

instance TauCeti.instIsClosedUnderIsomorphismsCommHopfAlgCatGeometricallyReducedCommHopfAlgProperty (k : Type u) [Field k] : (geometricallyReducedCommHopfAlgProperty k).IsClosedUnderIsomorphisms

Geometric reducedness is invariant under isomorphisms of commutative Hopf algebras.