English
The natural isomorphism between (-).Elementsᵒᵖ and (yoneda, -) is natural in its argument; i.e., it commutes with maps of functors in a natural way.
Русский
Естественная изоморфность между (-).Elementsᵒᵖ и (yoneda, -) является натуральной по отношению к аргументу; она коммутирует с отображениями функторов в естественный образом.
LaTeX
$$$\\text{Yoneda equivalence naturality: } (map α) .\\mathrm{op} \\circ toCostructuredArrow F_2 = toCostructuredArrow F_1 \\circ CostructuredArrow.map α$$$
Lean4
/-- The equivalence `(-.Elements)ᵒᵖ ≅ (yoneda, -)` of is actually a natural isomorphism of functors.
-/
theorem costructuredArrow_yoneda_equivalence_naturality {F₁ F₂ : Cᵒᵖ ⥤ Type v} (α : F₁ ⟶ F₂) :
(map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α :=
by
fapply Functor.ext
· intro X
simp only [CostructuredArrow.map_mk, toCostructuredArrow_obj, Functor.op_obj, Functor.comp_obj]
congr
ext _ f
simpa using congr_fun (α.naturality f.op).symm (unop X).snd
· simp
