coyonedaEquiv_naturality — Mathlib

English

For f: coyoneda.obj (op X) ⟶ F and g: X ⟶ Y, F.map g (coyonedaEquiv f) = coyonedaEquiv (coyoneda.map g.op ≫ f).

Русский

Для f: coyoneda.obj (op X) ⟶ F и g: X ⟶ Y, выполняется F.map g (coyonedaEquiv f) = coyonedaEquiv (coyoneda.map g.op ≫ f).

LaTeX

$$$F.map g (coyonedaEquiv f) = coyonedaEquiv (coyoneda.map g.op \circ f)$$$

Lean4

theorem coyonedaEquiv_naturality {X Y : C} {F : C ⥤ Type v₁} (f : coyoneda.obj (op X) ⟶ F) (g : X ⟶ Y) :
    F.map g (coyonedaEquiv f) = coyonedaEquiv (coyoneda.map g.op ≫ f) :=
  by
  change (f.app X ≫ F.map g) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)
  rw [← f.naturality]
  simp

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