Trifunctors obtained by composition of bifunctors #
Given two bifunctors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂ and G : C₁₂ ⥤ C₃ ⥤ C₄, we define
the trifunctor bifunctorComp₁₂ F₁₂ G : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ which sends three
objects X₁ : C₁, X₂ : C₂ and X₃ : C₃ to G.obj ((F₁₂.obj X₁).obj X₂)).obj X₃.
Similarly, given two bifunctors F : C₁ ⥤ C₂₃ ⥤ C₄ and G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃, we define
the trifunctor bifunctorComp₂₃ F G₂₃ : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ which sends three
objects X₁ : C₁, X₂ : C₂ and X₃ : C₃ to (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃).
def
CategoryTheory.bifunctorComp₁₂Obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
(X₁ : C₁)
:
CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)
Auxiliary definition for bifunctorComp₁₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.bifunctorComp₁₂Obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
(X₁ : C₁)
{X₂ Y₂ : C₂}
(φ : X₂ ⟶ Y₂)
(X₃ : C₃)
:
((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).map φ).app X₃ = (G.map ((F₁₂.obj X₁).map φ)).app X₃
@[simp]
theorem
CategoryTheory.bifunctorComp₁₂Obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
(X₁ : C₁)
(X₂ : C₂)
(X₃ : C₃)
:
((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂).obj X₃ = (G.obj ((F₁₂.obj X₁).obj X₂)).obj X₃
@[simp]
theorem
CategoryTheory.bifunctorComp₁₂Obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
(X₁ : C₁)
(X₂ : C₂)
{x✝ x✝¹ : C₃}
(φ : x✝ ⟶ x✝¹)
:
((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂).map φ = (G.obj ((F₁₂.obj X₁).obj X₂)).map φ
def
CategoryTheory.bifunctorComp₁₂
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
:
CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))
Given two bifunctors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂ and G : C₁₂ ⥤ C₃ ⥤ C₄, this is
the trifunctor C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ obtained by composition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.bifunctorComp₁₂_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{X₁ Y₁ : C₁}
(φ : X₁ ⟶ Y₁)
(X₂ : C₂)
(X₃ : C₃)
:
(((CategoryTheory.bifunctorComp₁₂ F₁₂ G).map φ).app X₂).app X₃ = (G.map ((F₁₂.map φ).app X₂)).app X₃
@[simp]
theorem
CategoryTheory.bifunctorComp₁₂_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
(X₁ : C₁)
:
(CategoryTheory.bifunctorComp₁₂ F₁₂ G).obj X₁ = CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁
def
CategoryTheory.bifunctorComp₁₂FunctorObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
:
CategoryTheory.Functor (CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
(CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
Auxiliary definition for bifunctorComp₁₂Functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.bifunctorComp₁₂FunctorObj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
:
(CategoryTheory.bifunctorComp₁₂FunctorObj F₁₂).obj G = CategoryTheory.bifunctorComp₁₂ F₁₂ G
@[simp]
theorem
CategoryTheory.bifunctorComp₁₂FunctorObj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
{G G' : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
(φ : G ⟶ G')
(X₁ : C₁)
(X₂ : C₂)
(X₃ : C₃)
:
((((CategoryTheory.bifunctorComp₁₂FunctorObj F₁₂).map φ).app X₁).app X₂).app X₃ = (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃
def
CategoryTheory.bifunctorComp₁₂FunctorMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
{F₁₂ F₁₂' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
(φ : F₁₂ ⟶ F₁₂')
:
Auxiliary definition for bifunctorComp₁₂Functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.bifunctorComp₁₂FunctorMap_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
{F₁₂ F₁₂' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
(φ : F₁₂ ⟶ F₁₂')
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
(X₁ : C₁)
(X₂ : C₂)
(X₃ : C₃)
:
((((CategoryTheory.bifunctorComp₁₂FunctorMap φ).app G).app X₁).app X₂).app X₃ = (G.map ((φ.app X₁).app X₂)).app X₃
def
CategoryTheory.bifunctorComp₁₂Functor
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
:
CategoryTheory.Functor (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(CategoryTheory.Functor (CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
(CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))))
The functor (C₁ ⥤ C₂ ⥤ C₁₂) ⥤ (C₁₂ ⥤ C₃ ⥤ C₄) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ which
sends F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂ and G : C₁₂ ⥤ C₃ ⥤ C₄ to the functor
bifunctorComp₁₂ F₁₂ G : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.bifunctorComp₁₂Functor_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
{X✝ Y✝ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
(φ : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.bifunctorComp₁₂Functor_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
:
def
CategoryTheory.bifunctorComp₂₃Obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
(X₁ : C₁)
:
CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)
Auxiliary definition for bifunctorComp₂₃.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.bifunctorComp₂₃Obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
(X₁ : C₁)
(X₂ : C₂)
{X✝ Y✝ : C₃}
(φ : X✝ ⟶ Y✝)
:
((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).obj X₂).map φ = (F.obj X₁).map ((G₂₃.obj X₂).map φ)
@[simp]
theorem
CategoryTheory.bifunctorComp₂₃Obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
(X₁ : C₁)
(X₂ : C₂)
(X₃ : C₃)
:
((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).obj X₂).obj X₃ = (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃)
@[simp]
theorem
CategoryTheory.bifunctorComp₂₃Obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
(X₁ : C₁)
{X₂ Y₂ : C₂}
(φ : X₂ ⟶ Y₂)
(X₃ : C₃)
:
((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).map φ).app X₃ = (F.obj X₁).map ((G₂₃.map φ).app X₃)
def
CategoryTheory.bifunctorComp₂₃
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
:
CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))
Given two bifunctors F : C₁ ⥤ C₂₃ ⥤ C₄ and G₂₃ : C₂ ⥤ C₃ ⥤ C₄, this is
the trifunctor C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ obtained by composition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.bifunctorComp₂₃_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{X₁ Y₁ : C₁}
(φ : X₁ ⟶ Y₁)
(X₂ : C₂)
(X₃ : C₃)
:
(((CategoryTheory.bifunctorComp₂₃ F G₂₃).map φ).app X₂).app X₃ = (F.map φ).app ((G₂₃.obj X₂).obj X₃)
@[simp]
theorem
CategoryTheory.bifunctorComp₂₃_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
(X₁ : C₁)
:
(CategoryTheory.bifunctorComp₂₃ F G₂₃).obj X₁ = CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁
def
CategoryTheory.bifunctorComp₂₃FunctorObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
:
CategoryTheory.Functor (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
(CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
Auxiliary definition for bifunctorComp₂₃Functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.bifunctorComp₂₃FunctorObj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
:
(CategoryTheory.bifunctorComp₂₃FunctorObj F).obj G₂₃ = CategoryTheory.bifunctorComp₂₃ F G₂₃
@[simp]
theorem
CategoryTheory.bifunctorComp₂₃FunctorObj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
{G₂₃ G₂₃' : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)}
(φ : G₂₃ ⟶ G₂₃')
(X₁ : C₁)
(X₂ : C₂)
(X₃ : C₃)
:
((((CategoryTheory.bifunctorComp₂₃FunctorObj F).map φ).app X₁).app X₂).app X₃ = (F.obj X₁).map ((φ.app X₂).app X₃)
def
CategoryTheory.bifunctorComp₂₃FunctorMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
{F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
(φ : F ⟶ F')
:
Auxiliary definition for bifunctorComp₂₃Functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.bifunctorComp₂₃FunctorMap_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
{F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
(φ : F ⟶ F')
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
(X₁ : C₁)
(X₂ : C₂)
(X₃ : C₃)
:
((((CategoryTheory.bifunctorComp₂₃FunctorMap φ).app G₂₃).app X₁).app X₂).app X₃ = (φ.app X₁).app ((G₂₃.obj X₂).obj X₃)
def
CategoryTheory.bifunctorComp₂₃Functor
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
:
CategoryTheory.Functor (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(CategoryTheory.Functor (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
(CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))))
The functor (C₁ ⥤ C₂₃ ⥤ C₄) ⥤ (C₂ ⥤ C₃ ⥤ C₂₃) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ which
sends F : C₁ ⥤ C₂₃ ⥤ C₄ and G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃ to the
functor bifunctorComp₂₃ F G₂₃ : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.bifunctorComp₂₃Functor_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
:
@[simp]
theorem
CategoryTheory.bifunctorComp₂₃Functor_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_11, u_6} C₂₃]
{X✝ Y✝ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
(φ : X✝ ⟶ Y✝)
: