Currying of functors in four variables

We study the equivalence of categories currying₄ : (C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E) ≌ C₁ × C₂ × C₃ × C₄ ⥤ E.

@[implicit_reducible]

def CategoryTheory.Functor.currying₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E))) ≌ Functor (C₁ × C₂ × C₃ × C₄) E

The equivalence of categories (C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E) ≌ C₁ × C₂ × C₃ × C₄ ⥤ E given by the curryfication of functors in four variables.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Functor.uncurry₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] : Functor (Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))) (Functor (C₁ × C₂ × C₃ × C₄) E)

Uncurrying a functor in four variables.

Equations

• CategoryTheory.Functor.uncurry₄ = CategoryTheory.Functor.currying₄.functor

@[reducible, inline]

abbrev CategoryTheory.Functor.curry₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] : Functor (Functor (C₁ × C₂ × C₃ × C₄) E) (Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E))))

Currying a functor in four variables.

Equations

• CategoryTheory.Functor.curry₄ = CategoryTheory.Functor.currying₄.inverse

@[simp]

theorem CategoryTheory.Functor.curry₄_map_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] {X✝ Y✝ : Functor (C₁ × C₂ × C₃ × C₄) E} (f : X✝ ⟶ Y✝) (X : C₁) (Y : C₂) (Y✝¹ : C₃) (Y✝² : C₄) : ((((curry₄.map f).app X).app Y).app Y✝¹).app Y✝² = f.app (X, Y, Y✝¹, Y✝²)

@[simp]

theorem CategoryTheory.Functor.curry₄_obj_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] (X : Functor (C₁ × C₂ × C₃ × C₄) E) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (Y : C₂) (Y✝¹ : C₃) (Y✝² : C₄) : ((((curry₄.obj X).map f).app Y).app Y✝¹).app Y✝² = X.map (Prod.mkHom f (Prod.mkHom (CategoryStruct.id Y) (Prod.mkHom (CategoryStruct.id Y✝¹) (CategoryStruct.id Y✝²))))

@[simp]

theorem CategoryTheory.Functor.curry₄_obj_obj_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] (X : Functor (C₁ × C₂ × C₃ × C₄) E) (X✝ : C₁) (Y : C₂) (Y✝ : C₃) {X✝¹ Y✝¹ : C₄} (g : X✝¹ ⟶ Y✝¹) : ((((curry₄.obj X).obj X✝).obj Y).obj Y✝).map g = X.map (Prod.mkHom (CategoryStruct.id X✝) (Prod.mkHom (CategoryStruct.id Y) (Prod.mkHom (CategoryStruct.id Y✝) g)))

@[simp]

theorem CategoryTheory.Functor.curry₄_obj_obj_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] (X : Functor (C₁ × C₂ × C₃ × C₄) E) (X✝ : C₁) (Y : C₂) {X✝¹ Y✝ : C₃} (g : X✝¹ ⟶ Y✝) (Y✝¹ : C₄) : ((((curry₄.obj X).obj X✝).obj Y).map g).app Y✝¹ = X.map (Prod.mkHom (CategoryStruct.id X✝) (Prod.mkHom (CategoryStruct.id Y) (Prod.mkHom g (CategoryStruct.id Y✝¹))))

@[simp]

theorem CategoryTheory.Functor.curry₄_obj_obj_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] (X : Functor (C₁ × C₂ × C₃ × C₄) E) (X✝ : C₁) {X✝¹ Y✝ : C₂} (g : X✝¹ ⟶ Y✝) (Y : C₃) (Y✝¹ : C₄) : ((((curry₄.obj X).obj X✝).map g).app Y).app Y✝¹ = X.map (Prod.mkHom (CategoryStruct.id X✝) (Prod.mkHom g (Prod.mkHom (CategoryStruct.id Y) (CategoryStruct.id Y✝¹))))

@[implicit_reducible]

def CategoryTheory.Functor.fullyFaithfulUncurry₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] : uncurry₄.FullyFaithful

Uncurrying functors in four variables gives a fully faithful functor.

Equations

• CategoryTheory.Functor.fullyFaithfulUncurry₄ = CategoryTheory.Functor.currying₄.fullyFaithfulFunctor

@[implicit_reducible]

def CategoryTheory.Functor.fullyFaithfulCurry₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] : curry₄.FullyFaithful

Currying functors in four variables gives a fully faithful functor.

Equations

• CategoryTheory.Functor.fullyFaithfulCurry₄ = CategoryTheory.Functor.currying₄.fullyFaithfulInverse

instance CategoryTheory.Functor.instFullProdUncurry₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] : uncurry₄.Full

instance CategoryTheory.Functor.instFaithfulProdUncurry₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] : uncurry₄.Faithful

instance CategoryTheory.Functor.instFullProdCurry₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] : curry₄.Full

instance CategoryTheory.Functor.instFaithfulProdCurry₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] : curry₄.Faithful

@[simp]

theorem CategoryTheory.Functor.currying₄_unitIso_hom_app_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) (X₄ : C₄) : ((((currying₄.unitIso.hom.app F).app X₁).app X₂).app X₃).app X₄ = CategoryStruct.id ((((((Functor.id (Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E))))).obj F).obj X₁).obj X₂).obj X₃).obj X₄)

@[simp]

theorem CategoryTheory.Functor.currying₄_unitIso_inv_app_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) (X₄ : C₄) : ((((currying₄.unitIso.inv.app F).app X₁).app X₂).app X₃).app X₄ = CategoryStruct.id ((((((currying₄.functor.comp currying₄.inverse).obj F).obj X₁).obj X₂).obj X₃).obj X₄)

@[implicit_reducible]

def CategoryTheory.Functor.curry₄ObjProdComp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (F₄ : Functor C₄ D₄) (G : Functor (D₁ × D₂ × D₃ × D₄) E) : curry₄.obj ((F₁.prod (F₂.prod (F₃.prod F₄))).comp G) ≅ F₁.comp ((curry₄.obj G).comp ((((whiskeringLeft₃ E).obj F₂).obj F₃).obj F₄))

Given functors F₁ : C₁ ⥤ D₁, F₂ : C₂ ⥤ D₂, F₃ : C₃ ⥤ D₃, F₄ : C₄ ⥤ D₄ and G : D₁ × D₂ × D₃ × D₄ ⥤ E, this is the isomorphism between curry₄.obj (F₁.prod (F₂.prod (F₃.prod F₄)) ⋙ G) : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E and F₁ ⋙ curry₄.obj G ⋙ ((((whiskeringLeft₃ E).obj F₂).obj F₃).obj F₄).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.curry₄ObjProdComp_hom_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (F₄ : Functor C₄ D₄) (G : Functor (D₁ × D₂ × D₃ × D₄) E) (X : C₁) (X✝ : C₂) (X✝¹ : C₃) (X✝² : C₄) : ((((F₁.curry₄ObjProdComp F₂ F₃ F₄ G).hom.app X).app X✝).app X✝¹).app X✝² = CategoryStruct.id (((((curry₄.obj ((F₁.prod (F₂.prod (F₃.prod F₄))).comp G)).obj X).obj X✝).obj X✝¹).obj X✝²)

@[simp]

theorem CategoryTheory.Functor.curry₄ObjProdComp_inv_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (F₄ : Functor C₄ D₄) (G : Functor (D₁ × D₂ × D₃ × D₄) E) (X : C₁) (X✝ : C₂) (X✝¹ : C₃) (X✝² : C₄) : ((((F₁.curry₄ObjProdComp F₂ F₃ F₄ G).inv.app X).app X✝).app X✝¹).app X✝² = CategoryStruct.id (((((curry₄.obj ((F₁.prod (F₂.prod (F₃.prod F₄))).comp G)).obj X).obj X✝).obj X✝¹).obj X✝²)