English
From a monoid isomorphism e: X ≃* Y between commutative monoids X and Y, construct an isomorphism in CommMonCat between CommMonCat.of X and CommMonCat.of Y, with forward map given by e.toMonoidHom.
Русский
Изоморфизм между коммутативными моноидами даёт изоморфизм в CommMonCat между соответствующими объектами, где отображение вперед − e.toMonoidHom.
LaTeX
$$$\exists i: CommMonCat.of X \cong CommMonCat.of Y \text{ с } i.hom = e.toMonoidHom.$$$
Lean4
/-- Build an isomorphism in the category `CommMonCat` from a `MulEquiv` between `CommMonoid`s. -/
@[to_additive (attr := simps) AddEquiv.toAddCommMonCatIso]
def toCommMonCatIso (e : X ≃* Y) : CommMonCat.of X ≅ CommMonCat.of Y
where
hom := CommMonCat.ofHom e.toMonoidHom
inv := CommMonCat.ofHom e.symm.toMonoidHom
