naturality — Mathlib

English

If α is a morphism between Yoneda objects yoneda X and yoneda Y, then for any Z,Z' with f: Z ⟶ Z' and h: Z' ⟶ X, the naturality condition holds: f followed by α.app(op Z') h equals α.app(op Z) (f followed by h).

Русский

Если α — морфизм между объектами Yoneda – yoneda X и yoneda Y, то для любых Z,Z' с f: Z ⟶ Z' и h: Z' ⟶ X выполнено условие натуральности: f ; α.app(op Z') h = α.app(op Z) (f ; h).

LaTeX

$$$ f \; \gg \alpha_{\mathrm{op} Z'}(h) = \alpha_{\mathrm{op} Z}(f \; \gg \! h) $$$

Lean4

@[simp]
theorem naturality {X Y : C} (α : yoneda.obj X ⟶ yoneda.obj Y) {Z Z' : C} (f : Z ⟶ Z') (h : Z' ⟶ X) :
    f ≫ α.app (op Z') h = α.app (op Z) (f ≫ h) :=
  (FunctorToTypes.naturality _ _ α f.op h).symm

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