English
Explicit description of the hom-equivalences giving the MonCat.adjoinOneAdj adjunction between free and forgetful functors for monoids.
Русский
Явное описание гомохарактеристик, задающих сопряжение между свободной конструкцией и забывающим функтором для моноидов.
LaTeX
$$MonCat.adjoinOneAdj : adjoinOne ⊣ forget MonCat$$
Lean4
/-- The `adjoinOne`-forgetful adjunction from `Semigrp` to `MonCat`. -/
@[to_additive /-- The `adjoinZero`-forgetful adjunction from `AddSemigrp` to `AddMonCat` -/
]
def adjoinOneAdj : adjoinOne ⊣ forget₂ MonCat.{u} Semigrp.{u} :=
Adjunction.mkOfHomEquiv
{ homEquiv X
Y :=
ConcreteCategory.homEquiv.trans
(WithOne.lift.symm.trans (ConcreteCategory.homEquiv (X := X) (Y := (forget₂ _ _).obj Y)).symm)
homEquiv_naturality_left_symm := by
intros
ext ⟨_ | _⟩ <;> simp <;> rfl }
