English
There is a universal adjunction between free and forgetful functors for monoids, realized via an explicit equivalence of hom-sets.
Русский
Существуют универсальные сопряжения между свободным и забывающим функтором для моноидов, реализованные через эквиваленцию множество-гомоморфизмов.
LaTeX
$$adj : free ⊣ forget MonCat$$
Lean4
/-- The free-forgetful adjunction for monoids. -/
@[to_additive /-- The free-forgetful adjunction for additive monoids. -/
]
def adj : free ⊣ forget MonCat.{u} :=
Adjunction.mkOfHomEquiv
{ homEquiv X Y := (ConcreteCategory.homEquiv (C := MonCat)).trans FreeMonoid.lift.symm
homEquiv_naturality_left_symm _ _ := MonCat.hom_ext (FreeMonoid.hom_eq fun _ => rfl) }
