English
Let F, G be functors and φ as above. For any presheaf P and any morphism f: uliftYoneda.obj X ⟶ P, the Yoneda equivalence sends f ≫ presheafHom φ P to the G-map applied to f evaluated at the image of X under F, using the φ-component at X.
Русский
Пусть F, G — функторы, φ — как выше. Для любой прешпефии P и морфизма f: uliftYoneda.obj X ⟶ P эквивалент Ёнеда переводит f ≫ presheafHom φ P в отображение G, применённое к f и оценивающееся в образе X через F, с использованием компонента φ при X.
LaTeX
$$$$ uliftYonedaEquiv (f ≡≡ presheafHom φ P) = (G.map f).app (Opposite.op (F.obj X)) ((φ.app X).app _ (ULift.up (\mathcal{1}))) $$$$
Lean4
theorem uliftYonedaEquiv_ι_presheafHom (P : Cᵒᵖ ⥤ Type max w v₁ v₂) {X : C} (f : uliftYoneda.{max w v₂}.obj X ⟶ P) :
uliftYonedaEquiv (f ≫ presheafHom.{w} φ P) =
(G.map f).app (Opposite.op (F.obj X)) ((φ.app X).app _ (ULift.up (𝟙 _))) :=
by
obtain ⟨x, rfl⟩ := uliftYonedaEquiv.symm.surjective f
erw [(colimitOfRepresentable P).fac _ (Opposite.op (P.elementsMk _ x))]
dsimp only [coconeApp]
apply Equiv.apply_symm_apply
