Smoothness of commutative Hopf algebras

This file records smoothness of a commutative Hopf algebra over a commutative ring R as an object property. The Hopf algebra structure carries the group law, while Algebra.Smooth R H records smoothness of the coordinate ring separately.

Main declarations

• TauCeti.smoothCommHopfAlgProperty: the object property on CommHopfAlgCat R selecting objects whose underlying R-algebra is smooth.

References

This is the explicit smoothness predicate requested by ReductiveGroups/README.md in TauCetiRoadmap. Smoothness remains separate from the commutative Hopf algebra category, as required by the roadmap.

def TauCeti.smoothCommHopfAlgProperty (R : Type u) [CommRing R] : CategoryTheory.ObjectProperty (CommHopfAlgCat R)

The object property on commutative Hopf algebras selecting coordinate algebras smooth over the base ring.

Equations

• TauCeti.smoothCommHopfAlgProperty R H = Algebra.Smooth R ↑H

@[simp]

theorem TauCeti.smoothCommHopfAlgProperty_iff {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : smoothCommHopfAlgProperty R H ↔ Algebra.Smooth R ↑H

Membership in the smooth commutative-Hopf-algebra object property.

instance TauCeti.instIsClosedUnderIsomorphismsCommHopfAlgCatSmoothCommHopfAlgProperty (R : Type u) [CommRing R] : (smoothCommHopfAlgProperty R).IsClosedUnderIsomorphisms

Smoothness is invariant under isomorphism of commutative Hopf algebras.