naturality_app — Mathlib

English

Let T : F ⟶ G be a natural transformation between functors C ⥤ D ⥤ E, and X ∈ C with f : Y ⟶ Z in D. Then (F.obj X).map f ≫ (T.app X).app Z = (T.app X).app Y ≫ (G.obj X).map f.

Русский

Пусть T : F ⟶ G — естественное преобразование между функторaми C ⥤ D ⥤ E и X ∈ C с f : Y ⟶ Z в D. Тогда (F.obj X).map f ≫ (T.app X).app Z = (T.app X).app Y ≫ (G.obj X).map f.

LaTeX

$$$ (F.obj X).map f \; \gg \; (T.app X).app Z = (T.app X).app Y \; \gg \; (G.obj X).map f. $$$

Lean4

@[reassoc (attr := simp)]
theorem naturality_app {F G : C ⥤ D ⥤ E} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) :
    (F.map f).app Z ≫ (T.app Y).app Z = (T.app X).app Z ≫ (G.map f).app Z :=
  congr_fun (congr_arg app (T.naturality f)) Z

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