Documentation

Mathlib.CategoryTheory.Functor.Trifunctor

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₃).

@[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} [] [] [] [] [] (F₁₂ : CategoryTheory.Functor C₁ ()) (G : CategoryTheory.Functor C₁₂ ()) (X₁ : C₁) (X₂ : C₂) {X₃ : C₃} {Y₃ : C₃} (φ : X₃ Y₃) :
(().obj X₂).map φ = (G.obj ((F₁₂.obj X₁).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_5} [] [] [] [] [] (F₁₂ : CategoryTheory.Functor C₁ ()) (G : CategoryTheory.Functor C₁₂ ()) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
(().obj X₂).obj X₃ = (G.obj ((F₁₂.obj X₁).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_5} [] [] [] [] [] (F₁₂ : CategoryTheory.Functor C₁ ()) (G : CategoryTheory.Functor C₁₂ ()) (X₁ : C₁) {X₂ : C₂} {Y₂ : C₂} (φ : X₂ Y₂) (X₃ : C₃) :
(().map φ).app X₃ = (G.map ((F₁₂.obj X₁).map φ)).app 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} [] [] [] [] [] (F₁₂ : CategoryTheory.Functor C₁ ()) (G : CategoryTheory.Functor C₁₂ ()) (X₁ : C₁) :

Auxiliary definition for bifunctorComp₁₂.

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} [] [] [] [] [] (F₁₂ : CategoryTheory.Functor C₁ ()) (G : CategoryTheory.Functor C₁₂ ()) {X₁ : C₁} {Y₁ : C₁} (φ : X₁ Y₁) (X₂ : C₂) (X₃ : C₃) :
((().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} [] [] [] [] [] (F₁₂ : CategoryTheory.Functor C₁ ()) (G : CategoryTheory.Functor C₁₂ ()) (X₁ : C₁) :
().obj X₁ =
def CategoryTheory.bifunctorComp₁₂ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [] [] [] [] [] (F₁₂ : CategoryTheory.Functor C₁ ()) (G : CategoryTheory.Functor 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₂₃Obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [] [] [] [] [] (F : CategoryTheory.Functor C₁ ()) (G₂₃ : CategoryTheory.Functor C₂ ()) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
(().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} [] [] [] [] [] (F : CategoryTheory.Functor C₁ ()) (G₂₃ : CategoryTheory.Functor C₂ ()) (X₁ : C₁) {X₂ : C₂} {Y₂ : C₂} (φ : X₂ Y₂) (X₃ : C₃) :
(().map φ).app X₃ = (F.obj X₁).map ((G₂₃.map φ).app 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_6} [] [] [] [] [] (F : CategoryTheory.Functor C₁ ()) (G₂₃ : CategoryTheory.Functor C₂ ()) (X₁ : C₁) (X₂ : C₂) {X₃ : C₃} {Y₃ : C₃} (φ : X₃ Y₃) :
(().obj X₂).map φ = (F.obj X₁).map ((G₂₃.obj X₂).map φ)
def CategoryTheory.bifunctorComp₂₃Obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [] [] [] [] [] (F : CategoryTheory.Functor C₁ ()) (G₂₃ : CategoryTheory.Functor C₂ ()) (X₁ : C₁) :

Auxiliary definition for bifunctorComp₂₃.

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} [] [] [] [] [] (F : CategoryTheory.Functor C₁ ()) (G₂₃ : CategoryTheory.Functor C₂ ()) {X₁ : C₁} {Y₁ : C₁} (φ : X₁ Y₁) (X₂ : C₂) (X₃ : C₃) :
((().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} [] [] [] [] [] (F : CategoryTheory.Functor C₁ ()) (G₂₃ : CategoryTheory.Functor C₂ ()) (X₁ : C₁) :
().obj X₁ =
def CategoryTheory.bifunctorComp₂₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [] [] [] [] [] (F : CategoryTheory.Functor C₁ ()) (G₂₃ : CategoryTheory.Functor 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