English
There is a forgetful-units adjunction between GrpCat and MonCat: forget₂ GrpCat MonCat ⊣ MonCat.units. In particular, Hom_MonCat(Forget(X), Y) ≅ Hom_GrpCat(X, Units(Y)) naturally.
Русский
Сопряжение forget₂ GrpCat MonCat ⊣ MonCat.units между GrpCat и MonCat: забывательное преобразование является левой частью, а Units — правой; естественно, MonCat-морфизмы из Forget(X) в Y соответствуют групповым морфизмам от X в Units(Y).
LaTeX
$$$\operatorname{Hom}_{\text{MonCat}}(\operatorname{Forget}(X), Y) \cong \operatorname{Hom}_{\text{GrpCat}}(X, \operatorname{Units}(Y)).$$$
Lean4
/-- The forgetful-units adjunction between `GrpCat` and `MonCat`. -/
def forget₂MonAdj : forget₂ GrpCat MonCat ⊣ MonCat.units.{u} :=
Adjunction.mk'
{ homEquiv _
Y :=
{ toFun f := ofHom (MonoidHom.toHomUnits f.hom)
invFun f := MonCat.ofHom ((Units.coeHom Y).comp f.hom) }
unit :=
{ app X := ofHom (@toUnits X _)
naturality _ _ _ := GrpCat.ext fun _ => Units.ext rfl }
counit :=
{ app X := MonCat.ofHom (Units.coeHom X)
naturality _ _ _ := MonCat.ext fun _ => rfl } }
