Lemmas about functors out of product categories. #
@[simp]
theorem
CategoryTheory.Bifunctor.map_id
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor (C × D) E)
(X : C)
(Y : D)
:
F.map (CategoryTheory.CategoryStruct.id X, CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (F.obj (X, Y))
@[simp]
theorem
CategoryTheory.Bifunctor.map_id_comp
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor (C × D) E)
(W : C)
{X : D}
{Y : D}
{Z : D}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
F.map (CategoryTheory.CategoryStruct.id W, CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.id W, f))
(F.map (CategoryTheory.CategoryStruct.id W, g))
@[simp]
theorem
CategoryTheory.Bifunctor.map_comp_id
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor (C × D) E)
(X : C)
(Y : C)
(Z : C)
(W : D)
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
F.map (CategoryTheory.CategoryStruct.comp f g, CategoryTheory.CategoryStruct.id W) = CategoryTheory.CategoryStruct.comp (F.map (f, CategoryTheory.CategoryStruct.id W))
(F.map (g, CategoryTheory.CategoryStruct.id W))
@[simp]
theorem
CategoryTheory.Bifunctor.diagonal
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor (C × D) E)
(X : C)
(X' : C)
(f : X ⟶ X')
(Y : D)
(Y' : D)
(g : Y ⟶ Y')
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.id X, g))
(F.map (f, CategoryTheory.CategoryStruct.id Y')) = F.map (f, g)
@[simp]
theorem
CategoryTheory.Bifunctor.diagonal'
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor (C × D) E)
(X : C)
(X' : C)
(f : X ⟶ X')
(Y : D)
(Y' : D)
(g : Y ⟶ Y')
:
CategoryTheory.CategoryStruct.comp (F.map (f, CategoryTheory.CategoryStruct.id Y))
(F.map (CategoryTheory.CategoryStruct.id X', g)) = F.map (f, g)