app_naturality — Mathlib

English

Let F,G : C ⥤ D ⥤ E and T : F ⟶ G. For X ∈ C and Y,Z ∈ D with f : Y ⟶ Z, we have (F.obj X).map f ≫ (T.app X).app Z = (T.app X).app Y ≫ (G.obj X).map f.

Русский

Пусть F,G : C ⥤ D ⥤ E и T : F ⟶ G. Для X ∈ C и Y,Z ∈ D с f : Y ⟶ Z выполняется (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]
theorem app_naturality {F G : C ⥤ D ⥤ E} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) :
    (F.obj X).map f ≫ (T.app X).app Z = (T.app X).app Y ≫ (G.obj X).map f :=
  (T.app X).naturality f

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