map_comp_assoc — Mathlib

English

Let F : C ⥤ D be a functor and f : X ⟶ Y, g : Y ⟶ Z, h : F.obj Z ⟶ W a morphism in D. Then the map preserves composition: (F.map (f ≫ g)) ≫ h = F.map f ≫ F.map g ≫ h.

Русский

Пусть F : C ⥤ D — функтор, f : X ⟶ Y, g : Y ⟶ Z, h : F.obj Z ⟶ W; тогда отображение сохраняет композицию: (F.map (f ≫ g)) ≫ h = F.map f ≫ F.map g ≫ h.

LaTeX

$$$ (F.map (f \circ g)) \circ h = (F.map f) \circ (F.map g) \circ h. $$$

Lean4

theorem map_comp_assoc {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : C ⥤ D) {X Y Z : C} (f : X ⟶ Y)
    (g : Y ⟶ Z) {W : D} (h : F.obj Z ⟶ W) : (F.map (f ≫ g)) ≫ h = F.map f ≫ F.map g ≫ h := by grind

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