English
If R is a commutative ring and A a CommBialgCat object cocommutative, then the underlying carrier object after applying the equivalence has a commutative monoid in the opposite sense.
Русский
Пусть R — коммутативное кольцо, A — объект CommBialgCat cocommutative; тогда носитель после применения эквивалентности становится коммутативным моноидом в противоположном виде.
LaTeX
$$$\\IsCommMonObj((commBialgCatEquivComonCommAlgCat R).functor.obj A).unop.X$$$
Lean4
instance {A : CommBialgCat.{u} R} [IsCocomm R A] :
IsCommMonObj ((commBialgCatEquivComonCommAlgCat R).functor.obj A).unop.X :=
inferInstanceAs <| IsCommMonObj <| op <| CommAlgCat.of R A
