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.

@[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))
@[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)
@[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)
@[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)
@[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)