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