English
The forgetful-units adjunction between CommGrpCat and CommMonCat: forget₂ CommGrpCat CommMonCat ⊣ CommMonCat.units. In particular, MonCat units is the right adjoint to forget₂ CommGrpCat CommMonCat.
Русский
Сопряжение forget₂ CommGrpCat CommMonCat и CommMonCat.units: забывательное преобразование и единицы образуют правое соприкожение; MonCat.units является правым сопряжением к forget₂ CommGrpCat CommMonCat.
LaTeX
$$$\operatorname{forget}_{\text{CommGrpCat} \to \text{CommMonCat}} \dashv \text{CommMonCat.units}.$$$
Lean4
/-- The forgetful-units adjunction between `CommGrpCat` and `CommMonCat`. -/
def forget₂CommMonAdj : forget₂ CommGrpCat CommMonCat ⊣ CommMonCat.units.{u} :=
Adjunction.mk'
{ homEquiv := fun _ Y ↦
{ toFun f := ofHom (MonoidHom.toHomUnits f.hom)
invFun f := CommMonCat.ofHom ((Units.coeHom Y).comp f.hom) }
unit.app X := ofHom toUnits.toMonoidHom
unit.naturality _ _ _ := CommGrpCat.ext fun _ => Units.ext rfl
counit.app
X :=
CommMonCat.ofHom
(Units.coeHom X)
-- `aesop` can find the following proof but it takes `0.5`s.
counit.naturality _ _ _ := CommMonCat.ext fun _ => rfl
homEquiv_unit := by intros;
rfl
-- `aesop` can find the following proof but it takes `0.2`s.
homEquiv_counit := by intros; rfl }
