yonedaEquiv_symm_naturality_left — Mathlib

English

Naturality of the symmetry of Yoneda Equiv on the left side: for f: X' → X, F a Sheaf, x ∈ F.val.obj ⟨X⟩, the equality involving symm holds due to injectivity of yonedaEquiv.

Русский

Натуральность симметрии Yoneda слева: для f: X' → X, F оболочка, x ∈ F(X), равенство следует из инъективности yonedaEquiv.

LaTeX

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

Lean4

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

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