unmop_isMonHom — Mathlib

English

If f is a morphism of monoid objects in C^op, then f.unmop is a morphism of monoid objects in C.

Русский

Если f — морфизм моноид-объектов в C^op, то f.unmop — морфизм моноид-объектов в C.

LaTeX

$$$$ \\text{IsMonHom}(f) \\Rightarrow \\text{IsMonHom}(f^{\\mathrm{unmop}}) $$$$

Lean4

/-- If `f` is a morphism of monoid objects internal to `Cᴹᵒᵖ`,
so is `f.unmop`. -/
instance unmop_isMonHom {N : Cᴹᵒᵖ} [MonObj N] (f : M ⟶ N) [IsMonHom f] : IsMonHom f.unmop
    where
  mul_hom := by
    apply mopEquiv C |>.fullyFaithfulFunctor.map_injective
    simpa [-IsMonHom.mul_hom] using IsMonHom.mul_hom f
  one_hom := by
    apply mopEquiv C |>.fullyFaithfulFunctor.map_injective
    simpa [-IsMonHom.one_hom] using IsMonHom.one_hom f

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