English
There is a canonical bijection between morphisms from the free Yoneda object to F and morphisms from M to F.obj(op X), natural in X, M, F.
Русский
Существует естественная Биекция между морфизмами из freeYoneda X M в F и морфизмами из M в F.obj(op X).
LaTeX
$$$\mathrm{freeYonedaHomEquiv} : (\mathrm{freeYoneda}\ X\ M \to F) \simeq (M \to F^{op}(X))$$$
Lean4
/-- The bijection `(Presheaf.freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (op X))`. -/
noncomputable def freeYonedaHomEquiv {X : C} {M : A} {F : Cᵒᵖ ⥤ A} : (freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (op X))
where
toFun f := Sigma.ι (fun (i : (yoneda.obj X).obj _) ↦ M) (𝟙 _) ≫ f.app (op X)
invFun
g :=
{ app Y := Sigma.desc (fun φ ↦ g ≫ F.map φ.op)
naturality _ _ _ := Sigma.hom_ext _ _ (by simp) }
left_inv
f := by
ext Y
refine Sigma.hom_ext _ _ (fun φ ↦ ?_)
simpa using (Sigma.ι _ (𝟙 _) ≫= f.naturality φ.op).symm
right_inv g := by simp
