yonedaEquiv_symm_naturality_left — Mathlib

English

Left naturality of yonedaEquiv.symm: yoneda.map f ≫ yonedaEquiv.symm x = yonedaEquiv.symm ((F.map f.op) x).

Русский

Левая естественность yonedaEquiv.symm: yoneda.map f ≫ yonedaEquiv.symm x = yonedaEquiv.symm ((F.map f.op) x).

LaTeX

$$$ yoneda.map f \\; \\gg \\; yonedaEquiv.symm x = yonedaEquiv.symm ((F.map f^{op}) x) $$$

Lean4

theorem yonedaEquiv_symm_naturality_left {X X' : C} (f : X' ⟶ X) (F : Cᵒᵖ ⥤ Type v₁) (x : F.obj ⟨X⟩) :
    yoneda.map f ≫ yonedaEquiv.symm x = yonedaEquiv.symm ((F.map f.op) x) :=
  by
  apply yonedaEquiv.injective
  simp only [yonedaEquiv_comp, yoneda_obj_obj, yonedaEquiv_symm_app_apply, Equiv.apply_symm_apply]
  erw [yonedaEquiv_yoneda_map]

Похожие утверждения