mkIso' — Mathlib

English

Construct an isomorphism of commutative monoid objects from a monoid isomorphism between the underlying objects.

Русский

Построение изоморфизма коммутативных моноидов из изоморфизма моноидов между базовыми объектами.

LaTeX

$$$\\text{mkIso'}: (e : M ≅ N) \\Rightarrow (\\mk M ≅ \\mk N)$$$

Lean4

/-- Construct an isomorphism of commutative monoid objects by giving a monoid isomorphism between
the underlying objects. -/
@[simps!]
def mkIso' {M N : C} (e : M ≅ N) [MonObj M] [IsCommMonObj M] [MonObj N] [IsCommMonObj N] [IsMonHom e.hom] :
    mk M ≅ mk N :=
  (fullyFaithfulForget₂Mon C).preimageIso (Mon.mkIso' e)

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