mathlib3 documentation

category_theory.products.bifunctor

Lemmas about functors out of product categories. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[simp]
theorem category_theory.bifunctor.map_id {C : Type u₁} {D : Type u₂} {E : Type u₃} [category_theory.category C] [category_theory.category D] [category_theory.category E] (F : C × D ⥤ E) (X : C) (Y : D) :
F.map (𝟙 X, 𝟙 Y) = 𝟙 (F.obj (X, Y))
source
@[simp]
theorem category_theory.bifunctor.map_id_comp {C : Type u₁} {D : Type u₂} {E : Type u₃} [category_theory.category C] [category_theory.category D] [category_theory.category E] (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)
source
@[simp]
theorem category_theory.bifunctor.map_comp_id {C : Type u₁} {D : Type u₂} {E : Type u₃} [category_theory.category C] [category_theory.category D] [category_theory.category E] (F : C × D ⥤ E) (X Y Z : C) (W : D) (f : X ⟶ Y) (g : Y ⟶ Z) :
F.map (f ≫ g, 𝟙 W) = F.map (f, 𝟙 W) ≫ F.map (g, 𝟙 W)
source
@[simp]
theorem category_theory.bifunctor.diagonal {C : Type u₁} {D : Type u₂} {E : Type u₃} [category_theory.category C] [category_theory.category D] [category_theory.category E] (F : C × D ⥤ E) (X X' : C) (f : X ⟶ X') (Y Y' : D) (g : Y ⟶ Y') :
F.map (𝟙 X, g) ≫ F.map (f, 𝟙 Y') = F.map (f, g)
source
@[simp]
theorem category_theory.bifunctor.diagonal' {C : Type u₁} {D : Type u₂} {E : Type u₃} [category_theory.category C] [category_theory.category D] [category_theory.category E] (F : C × D ⥤ E) (X X' : C) (f : X ⟶ X') (Y Y' : D) (g : Y ⟶ Y') :
F.map (f, 𝟙 Y) ≫ F.map (𝟙 X', g) = F.map (f, g)