commBialgCatEquivComonCommAlgCat — Mathlib

Lean4
/-- Commutative bialgebras over a commutative ring `R` are the same thing as comonoid
`R`-algebras. -/
@[simps! functor_obj_unop_X inverse_obj unitIso_hom_app unitIso_inv_app counitIso_hom_app counitIso_inv_app]
def commBialgCatEquivComonCommAlgCat : CommBialgCat R ≌ (Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ
    where
  functor.obj A := .op <| .mk <| .op <| .of R A
  functor.map {A B} f := .op <| .mk' <| .op <| CommAlgCat.ofHom f.hom
  inverse.obj A := .of R A.unop.X.unop
  inverse.map {A B}
    f :=
    CommBialgCat.ofHom <|
      .ofAlgHom f.unop.hom.unop.hom congr(($(IsMonHom.one_hom (f := f.unop.hom))).unop.hom)
        congr(($((IsMonHom.mul_hom (f := f.unop.hom)).symm)).unop.hom)
  unitIso.hom := 𝟙 _
  unitIso.inv := 𝟙 _
  counitIso.hom := 𝟙 _
  counitIso.inv := 𝟙 _
Похожие утверждения