Curry and uncurry, as functors.

We define curry : ((C × D) ⥤ E) ⥤ (C ⥤ (D ⥤ E)) and uncurry : (C ⥤ (D ⥤ E)) ⥤ ((C × D) ⥤ E), and verify that they provide an equivalence of categories currying : (C ⥤ (D ⥤ E)) ≌ ((C × D) ⥤ E).

@[simp]

theorem CategoryTheory.uncurry_obj_obj {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C × D) : (CategoryTheory.uncurry.obj F).obj X = (F.obj X.fst).obj X.snd

@[simp]

theorem CategoryTheory.uncurry_map_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] : ∀ {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : X ⟶ Y) (X_1 : C × D), (CategoryTheory.uncurry.map T).app X_1 = (T.app X_1.fst).app X_1.snd

@[simp]

theorem CategoryTheory.uncurry_obj_map {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X : C × D} {Y : C × D} (f : X ⟶ Y) : (CategoryTheory.uncurry.obj F).map f = CategoryTheory.CategoryStruct.comp ((F.map f.fst).app X.snd) ((F.obj Y.fst).map f.snd)

def CategoryTheory.uncurry {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] : CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.Functor D E)) (CategoryTheory.Functor (C × D) E)

The uncurrying functor, taking a functor C ⥤ (D ⥤ E) and producing a functor (C × D) ⥤ E.

Equations

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

def CategoryTheory.curryObj {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) : CategoryTheory.Functor C (CategoryTheory.Functor D E)

The object level part of the currying functor. (See curry for the functorial version.)

Equations

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

@[simp]

theorem CategoryTheory.curry_obj_obj_map {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) : ∀ {X Y : D} (g : X ⟶ Y), ((CategoryTheory.curry.obj F).obj X).map g = F.map (CategoryTheory.CategoryStruct.id X, g)

@[simp]

theorem CategoryTheory.curry_map_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] : ∀ {X Y : CategoryTheory.Functor (C × D) E} (T : X ⟶ Y) (X_1 : C) (Y_1 : D), ((CategoryTheory.curry.map T).app X_1).app Y_1 = T.app (X_1, Y_1)

@[simp]

theorem CategoryTheory.curry_obj_obj_obj {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) (Y : D) : ((CategoryTheory.curry.obj F).obj X).obj Y = F.obj (X, Y)

@[simp]

theorem CategoryTheory.curry_obj_map_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) : ∀ {X Y : C} (f : X ⟶ Y) (Y_1 : D), ((CategoryTheory.curry.obj F).map f).app Y_1 = F.map (f, CategoryTheory.CategoryStruct.id Y_1)

def CategoryTheory.curry {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] : CategoryTheory.Functor (CategoryTheory.Functor (C × D) E) (CategoryTheory.Functor C (CategoryTheory.Functor D E))

The currying functor, taking a functor (C × D) ⥤ E and producing a functor C ⥤ (D ⥤ E).

Equations

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

@[simp]

theorem CategoryTheory.currying_unitIso_inv_app_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C) (X : D) : ((CategoryTheory.currying.unitIso.inv.app X).app X).app X = CategoryTheory.CategoryStruct.id ((X.obj X).obj X)

@[simp]

theorem CategoryTheory.currying_counitIso_hom_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor (C × D) E) (X : C × D) : (CategoryTheory.currying.counitIso.hom.app X).app X = CategoryTheory.CategoryStruct.id (X.obj (X.fst, X.snd))

@[simp]

theorem CategoryTheory.currying_inverse_obj_obj_map {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) : ∀ {X Y : D} (g : X ⟶ Y), ((CategoryTheory.currying.inverse.obj F).obj X).map g = F.map (CategoryTheory.CategoryStruct.id X, g)

@[simp]

theorem CategoryTheory.currying_unitIso_hom_app_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C) (X : D) : ((CategoryTheory.currying.unitIso.hom.app X).app X).app X = CategoryTheory.CategoryStruct.id ((X.obj X).obj X)

@[simp]

theorem CategoryTheory.currying_inverse_map_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] : ∀ {X Y : CategoryTheory.Functor (C × D) E} (T : X ⟶ Y) (X_1 : C) (Y_1 : D), ((CategoryTheory.currying.inverse.map T).app X_1).app Y_1 = T.app (X_1, Y_1)

@[simp]

theorem CategoryTheory.currying_functor_obj_map {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X : C × D} {Y : C × D} (f : X ⟶ Y) : (CategoryTheory.currying.functor.obj F).map f = CategoryTheory.CategoryStruct.comp ((F.map f.fst).app X.snd) ((F.obj Y.fst).map f.snd)

@[simp]

theorem CategoryTheory.currying_functor_obj_obj {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C × D) : (CategoryTheory.currying.functor.obj F).obj X = (F.obj X.fst).obj X.snd

@[simp]

theorem CategoryTheory.currying_functor_map_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] : ∀ {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : X ⟶ Y) (X_1 : C × D), (CategoryTheory.currying.functor.map T).app X_1 = (T.app X_1.fst).app X_1.snd

@[simp]

theorem CategoryTheory.currying_inverse_obj_map_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) : ∀ {X Y : C} (f : X ⟶ Y) (Y_1 : D), ((CategoryTheory.currying.inverse.obj F).map f).app Y_1 = F.map (f, CategoryTheory.CategoryStruct.id Y_1)

@[simp]

theorem CategoryTheory.currying_inverse_obj_obj_obj {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) (Y : D) : ((CategoryTheory.currying.inverse.obj F).obj X).obj Y = F.obj (X, Y)

@[simp]

theorem CategoryTheory.currying_counitIso_inv_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor (C × D) E) (X : C × D) : (CategoryTheory.currying.counitIso.inv.app X).app X = CategoryTheory.CategoryStruct.id (X.obj (X.fst, X.snd))

def CategoryTheory.currying {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] : CategoryTheory.Functor C (CategoryTheory.Functor D E) ≌ CategoryTheory.Functor (C × D) E

The equivalence of functor categories given by currying/uncurrying.

Equations

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

@[simp]

theorem CategoryTheory.flipIsoCurrySwapUncurry_inv_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D) (X : C) : ((CategoryTheory.flipIsoCurrySwapUncurry F).inv.app X).app X = CategoryTheory.CategoryStruct.id ((F.obj X).obj X)

@[simp]

theorem CategoryTheory.flipIsoCurrySwapUncurry_hom_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D) (X : C) : ((CategoryTheory.flipIsoCurrySwapUncurry F).hom.app X).app X = CategoryTheory.CategoryStruct.id ((F.obj X).obj X)

def CategoryTheory.flipIsoCurrySwapUncurry {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) : CategoryTheory.Functor.flip F ≅ CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap D C) (CategoryTheory.uncurry.obj F))

F.flip is isomorphic to uncurrying F, swapping the variables, and currying.

Equations

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

@[simp]

theorem CategoryTheory.uncurryObjFlip_hom_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D × C) : (CategoryTheory.uncurryObjFlip F).hom.app X = CategoryTheory.CategoryStruct.id ((F.obj X.snd).obj X.fst)

@[simp]

theorem CategoryTheory.uncurryObjFlip_inv_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D × C) : (CategoryTheory.uncurryObjFlip F).inv.app X = CategoryTheory.CategoryStruct.id ((F.obj X.snd).obj X.fst)

def CategoryTheory.uncurryObjFlip {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) : CategoryTheory.uncurry.obj (CategoryTheory.Functor.flip F) ≅ CategoryTheory.Functor.comp (CategoryTheory.Prod.swap D C) (CategoryTheory.uncurry.obj F)

The uncurrying of F.flip is isomorphic to swapping the factors followed by the uncurrying of F.

Equations

• CategoryTheory.uncurryObjFlip F = CategoryTheory.NatIso.ofComponents fun p => CategoryTheory.Iso.refl ((CategoryTheory.uncurry.obj (CategoryTheory.Functor.flip F)).obj p)

@[simp]

theorem CategoryTheory.whiskeringRight₂_obj_map_app_app (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) : ∀ {X Y : CategoryTheory.Functor B C} (f : X ⟶ Y) (Y_1 : CategoryTheory.Functor B D) (X_1 : B), ((((CategoryTheory.whiskeringRight₂ B C D E).obj X).map f).app Y_1).app X_1 = (X.map (f.app X_1)).app (Y_1.obj X_1)

@[simp]

theorem CategoryTheory.whiskeringRight₂_obj_obj_obj_obj (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : CategoryTheory.Functor B C) (Y : CategoryTheory.Functor B D) (X : B) : ((((CategoryTheory.whiskeringRight₂ B C D E).obj X).obj X).obj Y).obj X = (X.obj (X.obj X)).obj (Y.obj X)

@[simp]

theorem CategoryTheory.whiskeringRight₂_obj_obj_obj_map (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : CategoryTheory.Functor B C) (Y : CategoryTheory.Functor B D) : ∀ {X Y : B} (f : X ⟶ Y), ((((CategoryTheory.whiskeringRight₂ B C D E).obj X).obj X).obj Y).map f = CategoryTheory.CategoryStruct.comp ((X.map (X.map f)).app (Y.obj X)) ((X.obj (X.obj Y)).map (Y.map f))

@[simp]

theorem CategoryTheory.whiskeringRight₂_obj_obj_map_app (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : CategoryTheory.Functor B C) : ∀ {X Y : CategoryTheory.Functor B D} (g : X ⟶ Y) (X_1 : B), ((((CategoryTheory.whiskeringRight₂ B C D E).obj X).obj X).map g).app X_1 = (X.obj (X.obj X_1)).map (g.app X_1)

@[simp]

theorem CategoryTheory.whiskeringRight₂_map_app_app_app (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] : ∀ {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (f : X ⟶ Y) (X_1 : CategoryTheory.Functor B C) (Y_1 : CategoryTheory.Functor B D) (c : B), ((((CategoryTheory.whiskeringRight₂ B C D E).map f).app X_1).app Y_1).app c = (f.app (X_1.obj c)).app (Y_1.obj c)

def CategoryTheory.whiskeringRight₂ (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] : CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.Functor D E)) (CategoryTheory.Functor (CategoryTheory.Functor B C) (CategoryTheory.Functor (CategoryTheory.Functor B D) (CategoryTheory.Functor B E)))

A version of CategoryTheory.whiskeringRight for bifunctors, obtained by uncurrying, applying whiskeringRight and currying back

Equations

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