English
There is a naturality condition for functorEnrichedHomCoyonedaObjEquiv with respect to precomposition by a morphism f: X→Y in C; the naturality equality holds between the two evaluations of the equivalence after precomposition.
Русский
Существует условие естественной натуральности для equiv между functorEnrichedHomCoyonedaObjEquiv и предкомпозицией по morphism f: X→Y; равенство натурализовано.
LaTeX
$$$\text{functorEnrichedHomCoyonedaObjEquiv}_N (f) = \text{presheafHom map } f \circ \text{equiv}$$$
Lean4
theorem functorEnrichedHomCoyonedaObjEquiv_naturality {M : A} {F G : Cᵒᵖ ⥤ A} {X Y : C} (f : X ⟶ Y)
[HasFunctorEnrichedHom A F G] (y : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op Y)) :
functorEnrichedHomCoyonedaObjEquiv M F G X (y ≫ precompEnrichedHom' _ (Under.map f.op) (Iso.refl _) (Iso.refl _)) =
(presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).map f.op (functorEnrichedHomCoyonedaObjEquiv M F G Y y) :=
by
dsimp
ext ⟨j⟩
simp [functorEnrichedHomCoyonedaObjEquiv, presheafHom]
rfl
