Group-like evaluation in commutative Hopf algebras

For a commutative Hopf algebra over a domain whose group-like elements span, evaluation identifies the group algebra on those elements with the original Hopf algebra. This categorical isomorphism is natural in morphisms between such algebras.

noncomputable def TauCeti.CommHopfAlgCat.evaluationIso {k : Type u} [CommRing k] [IsDomain k] {H : CommHopfAlgCat k} [Module.IsTorsionFree k ↑H] (hH : Submodule.span k (Set.range GroupLike.val) = ⊤) : ↧(MonoidAlgebra k (GroupLike k ↑H)) ≅ H

The categorical isomorphism given by evaluation on the group-like elements of a torsion-free commutative Hopf algebra when they span its carrier.

Equations

• TauCeti.CommHopfAlgCat.evaluationIso hH = CommHopfAlgCat.isoMk (TauCeti.GroupLike.evaluationBialgEquiv k (↑H) hH)

theorem TauCeti.CommHopfAlgCat.evaluationIso_naturality {k : Type u} [CommRing k] [IsDomain k] {H K : CommHopfAlgCat k} [Module.IsTorsionFree k ↑H] [Module.IsTorsionFree k ↑K] (hH : Submodule.span k (Set.range GroupLike.val) = ⊤) (hK : Submodule.span k (Set.range GroupLike.val) = ⊤) (f : H ⟶ K) : CategoryTheory.CategoryStruct.comp (evaluationIso hH).hom f = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom k (GroupLike.map (CommHopfAlgCat.Hom.hom f)))) (evaluationIso hK).hom

Evaluation commutes with a morphism of torsion-free commutative Hopf algebras whose group-like elements span their carriers.