English
For X, Y in C and F : C ⥤ Type, given f : X ⟶ Y and t ∈ F.obj X, the symmetric coyoneda equivalence satisfies coyonedaEquiv.symm (F.map f t) = coyoneda.map f.op ≫ coyonedaEquiv.symm t. In words: transporting along f commutes with the coyoneda equivalence on the left and the coyoneda map on the right.
Русский
Пусть X, Y — объекты категории C, F — функтор C ⥤ Type, f : X ⟶ Y, t ∈ F.obj X. Тогда coyonedaEquiv.symm (F.map f t) = coyoneda.map f.op ≫ coyonedaEquiv.symm t. Это означает корректную совместимость обратной эквивалентности Coyoneda с отображением coyoneda.map.
LaTeX
$$$$ \mathrm{coyonedaEquiv}.symm (F.map f t) = \mathrm{coyoneda.map} f^{op} \;\circ\; \mathrm{coyonedaEquiv}.symm t $$$$
Lean4
theorem coyonedaEquiv_symm_map {X Y : C} (f : X ⟶ Y) {F : C ⥤ Type v₁} (t : F.obj X) :
coyonedaEquiv.symm (F.map f t) = coyoneda.map f.op ≫ coyonedaEquiv.symm t :=
by
obtain ⟨u, rfl⟩ := coyonedaEquiv.surjective t
simp [coyonedaEquiv_naturality u f]
