English
For X,Y in C^op and a morphism f: X → Y, and any F : C^op ⥤ Type with t ∈ F.obj X, the Yoneda symmetry gives yonedaEquiv.symm (F.map f t) = yoneda.map f.unop ≫ yonedaEquiv.symm t.
Русский
Для X, Y в C^op и морфизма f: X → Y, и для F: C^op ⥤ Type с элементом t ∈ F.obj X, симметрия Ёнеды даёт: yonedaEquiv.symm (F.map f t) = yoneda.map f.unop ≫ yonedaEquiv.symm t.
LaTeX
$$$yonedaEquiv.symm (F.map f t) = \ yoneda.map f.unop \gg YonedaEquiv.symm t$$$
Lean4
theorem yonedaEquiv_symm_map {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : Cᵒᵖ ⥤ Type v₁} (t : F.obj X) :
yonedaEquiv.symm (F.map f t) = yoneda.map f.unop ≫ yonedaEquiv.symm t :=
by
obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t
rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]
