mopMonObj — Mathlib

English

If M is a monoid object in C, then mop M is a monoid object in C^op.

Русский

Если M — моноид-объект в C, то mop M — моноид-объект в C^op.

LaTeX

$$$$ \\mathrm{MonObj}(M) \\Rightarrow \\mathrm{MonObj}(\\mathrm{mop}(M)) $$$$

Lean4

/-- If `M : C` is a monoid object, then `mop M : Cᴹᵒᵖ` too. -/
@[simps!]
instance mopMonObj : MonObj (mop M) where
  mul := MonObj.mul.mop
  one := MonObj.one.mop
  mul_one := by
    apply mopEquiv C |>.fullyFaithfulInverse.map_injective
    simp
  one_mul := by
    apply mopEquiv C |>.fullyFaithfulInverse.map_injective
    simp
  mul_assoc := by
    apply mopEquiv C |>.fullyFaithfulInverse.map_injective
    simp

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