yonedaEquiv_naturality — Mathlib

English

Naturality of yonedaEquiv: F.map g.op (yonedaEquiv f) = yonedaEquiv (yoneda.map g ≫ f).

Русский

Естественность yonedaEquiv: F.map g.op (yonedaEquiv f) = yonedaEquiv (yoneda.map g ≫ f).

LaTeX

$$$ F.map g^{op} (yonedaEquiv f) = yonedaEquiv (yoneda.map g ≫ f) $$$

Lean4

/-- See also `yonedaEquiv_naturality'` for a more general version. -/
theorem yonedaEquiv_naturality {X Y : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj X ⟶ F) (g : Y ⟶ X) :
    F.map g.op (yonedaEquiv f) = yonedaEquiv (yoneda.map g ≫ f) :=
  by
  change (f.app (op X) ≫ F.map g.op) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)
  rw [← f.naturality]
  simp

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