English
Let F be the free functor from sets to Additive Commutative Groups and U the forgetful functor from AddCommGrp to sets. Then F is left adjoint to U; equivalently, for every set X and additive commutative group A, there is a natural bijection Hom_AddCommGrp(F(X), A) ≅ Hom_Set(X, U(A)).
Русский
Пусть F — свободный функтор от множеств в свободные аддитивные коммутативные группы, а U — забывательный функтор из AddCommGrp в множества. Тогда F является левым сопряжением к U; эквивалентно, для любых множества X и аддитивной коммутативной группы A существует естественная биекция между множествами гомоморфизмов Hom_AddCommGrp(F(X), A) и Hom_Set(X, U(A)).
LaTeX
$$$\operatorname{Hom}_{\text{AddCommGrp}}(F(X), A) \cong \operatorname{Hom}_{\text{Set}}(X, U(A)).$$$
Lean4
instance : free.{u}.IsLeftAdjoint :=
⟨_, ⟨adj⟩⟩
