English
An isomorphism of monoids M ≃* N induces an equivalence of the corresponding single-object categories.
Русский
Изоморфизм моноидов M ≃* N порождает эквивалентность категорий с одним объектом.
LaTeX
$$$e: M\\simeq_* N \\quad\\Rightarrow\\quad \\mathrm{SingleObj} M \\simeq \\mathrm{SingleObj} N$$$
Lean4
/-- Reinterpret a monoid isomorphism `f : M ≃* N` as an equivalence `SingleObj M ≌ SingleObj N`. -/
@[simps!]
def toSingleObjEquiv (e : M ≃* N) : SingleObj M ≌ SingleObj N
where
functor := e.toMonoidHom.toFunctor
inverse := e.symm.toMonoidHom.toFunctor
unitIso :=
eqToIso
(by
rw [← MonoidHom.comp_toFunctor, ← MonoidHom.id_toFunctor]
congr 1
simp)
counitIso :=
eqToIso
(by
rw [← MonoidHom.comp_toFunctor, ← MonoidHom.id_toFunctor]
congr 1
simp)
