English
Let R be a commutative ring and A a commutative R-algebra equipped with a bialgebra structure over R. Then the opposite of the algebra object CommAlgCat.of R A carries a natural monoid object structure, with the unit map given by the op of counitAlgHom R A and the multiplication map given by the op of comulAlgHom R A; the usual unit and associativity laws hold.
Русский
Пусть R — коммутативное кольцо, A — коммутативное R-алгебраическое пространство с биалгебраической структурой над R. Тогда противоположный объект моноида монодного типа Op CommAlgCat.of R A естественным образом образует моноидный объект, где единичный морфизм равен (counitAlgHom R A)^op, а умножение — (comulAlgHom R A)^op; выполняются стандартные аксиомы единицы и ассоциативности.
LaTeX
$$$1 = (\\mathrm{counitAlgHom}\\,R\\,A)^{\\mathrm{op}}, \\quad \\mu = (\\mathrm{comulAlgHom}\\,R\\,A)^{\\mathrm{op}}$$$
Lean4
instance monObjOpOf {A : Type u} [CommRing A] [Bialgebra R A] : MonObj (op <| CommAlgCat.of R A)
where
one := (CommAlgCat.ofHom <| counitAlgHom R A).op
mul := (CommAlgCat.ofHom <| comulAlgHom R A).op
one_mul := by ext; exact Coalgebra.rTensor_counit_comul _
mul_one := by ext; exact Coalgebra.lTensor_counit_comul _
mul_assoc := by ext; exact (Coalgebra.coassoc_symm_apply _).symm
