instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm

English

If A is a commutative ring and a bialgebra over R with the cocommutativity condition IsCocomm R A, then the opposite object of CommAlgCat.of R A is a commutative monoid object.

Русский

Пусть A — кольцо с биалгеброй над R и выполняется cocommutativity IsCocomm R A. Тогда противоположный объект CommAlgCat.of R A является коммутативным моноидом (объектом моноида).

LaTeX

$$$\\text{IsCommMonObj}\\big(\\mathrm{op}\\big(\\mathrm{CommAlgCat.of}\\,R\\,A\\big)\\big) , \\quad \\text{mul\_comm}:= \\text{mul}_{\\mathrm{op}}(a\\otimes b)=\\text{mul}_{\\mathrm{op}}(b\\otimes a)$$$

Lean4

instance {A : Type u} [CommRing A] [Bialgebra R A] [IsCocomm R A] : IsCommMonObj (Opposite.op <| CommAlgCat.of R A)
    where mul_comm := by ext; exact comm_comul R _

Похожие утверждения