English
The forgetful functor forget₂ from CommMonCat to MonCat is full, i.e., every MonCat-morphism between forgetful images lifts to a CommMonCat-morphism.
Русский
Забывающий функтор forget₂ от CommMonCat к MonCat полон: любой моноидовый морфизм поднимается до CommMonCat-морфизма.
LaTeX
$$$\forall X,Y:\; \forall f:\; \mathrm{Hom}_{MonCat}(\mathrm{forget}_2 X, \mathrm{forget}_2 Y),\; \exists g:\; \mathrm{Hom}_{CommMonCat}(X,Y)\; \text{ с } \mathrm{forget}_2(g)=f.$$$
Lean4
/-- Ensure that `forget₂ CommMonCat MonCat` automatically reflects isomorphisms.
We could have used `CategoryTheory.HasForget.ReflectsIso` alternatively.
-/
@[to_additive]
instance forget₂_full : (forget₂ CommMonCat MonCat).Full where map_surjective f := ⟨ofHom f.hom, rfl⟩
