instIsRightAdjointForget — Mathlib

English

The forgetful functor forget_AddCommGrp : AddCommGrp -> Type is right adjoint to the free functor F: Type -> AddCommGrp; equivalently, for every set X and additive commutative group A, there is a natural bijection Hom_Set(X, U(A)) ≅ Hom_AddCommGrp(F(X), A).

Русский

Забывательный функтор forget_AddCommGrp: AddCommGrp → Type является правым сопряжением к свободному функтору F: Type → AddCommGrp; эквивалентно, для любых множества X и аддитивной коммутативной группы A существует естественная биекция Hom_Set(X, U(A)) ≅ Hom_AddCommGrp(F(X), A).

LaTeX

$$$\operatorname{Hom}_{\text{Set}}(X, U(A)) \cong \operatorname{Hom}_{\text{AddCommGrp}}(F(X), A).$$$

Lean4

instance : (forget AddCommGrpCat.{u}).IsRightAdjoint :=
  ⟨_, ⟨adj⟩⟩

Похожие утверждения