map_id_comp — Mathlib

English

Let F : C × D ⥤ E be a bifunctor. For objects W ∈ C and X ⟶ Y, f : X ⟶ Y and g : ? ⟶ ?, we have F.map (id_W × f ≫ g) = F.map (id_W × f) ≫ F.map (id_W × g).

Русский

Для бисюфунктора F : C × D ⥤ E, выполняется равенство сохранения композиции по второму аргументу: F.map (id_W × (f ≫ g)) = F.map (id_W × f) ≫ F.map (id_W × g).

LaTeX

$$$F.map (\\mathrm{id}_W \\times (f \\circ g)) = F.map (\\mathrm{id}_W \\times f) \\circ F.map (\\mathrm{id}_W \\times g)$$$

Lean4

@[simp]
theorem map_id_comp (F : C × D ⥤ E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map (𝟙 W ×ₘ (f ≫ g)) = F.map (𝟙 W ×ₘ f) ≫ F.map (𝟙 W ×ₘ g) := by
  rw [← Functor.map_comp, prod_comp, Category.comp_id]

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