English
If f: M → N is a morphism of monoid objects in C, then f.mop: mop M → mop N is a morphism of monoid objects in C^op.
Русский
Если f: M → N — морфизм моноид-объектов в C, то f.mop: mop M → mop N — морфизм моноид-объектов в C^op.
LaTeX
$$$$ \\text{IsMonHom}(f) \\Rightarrow \\text{IsMonHom}(f^{\\mathrm{mop}}) $$$$
Lean4
/-- If `f` is a morphism of monoid objects internal to `C`,
then `f.mop` is a morphism of monoid objects internal to `Cᴹᵒᵖ`. -/
instance mop_isMonHom {N : C} [MonObj N] (f : M ⟶ N) [IsMonHom f] : IsMonHom f.mop
where
mul_hom := by
apply mopEquiv C |>.fullyFaithfulInverse.map_injective
simpa [-IsMonHom.mul_hom] using IsMonHom.mul_hom f
one_hom := by
apply mopEquiv C |>.fullyFaithfulInverse.map_injective
simpa [-IsMonHom.one_hom] using IsMonHom.one_hom f
