mathlib documentation

category_theory.functor.currying

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

def category_theory.uncurry {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] :
(C D E) C × D E

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

Equations
def category_theory.curry_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C × D E) :
C D E

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

Equations
def category_theory.curry {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] :
(C × D E) C D E

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

Equations
@[simp]
theorem category_theory.uncurry.obj_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C D E} {X : C × D} :
@[simp]
theorem category_theory.uncurry.obj_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C D E} {X Y : C × D} {f : X Y} :
@[simp]
theorem category_theory.uncurry.map_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C D E} {α : F G} {X : C × D} :
@[simp]
theorem category_theory.curry.obj_obj_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C × D E} {X : C} {Y : D} :
((category_theory.curry.obj F).obj X).obj Y = F.obj (X, Y)
@[simp]
theorem category_theory.curry.obj_obj_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C × D E} {X : C} {Y Y' : D} {g : Y Y'} :
@[simp]
theorem category_theory.curry.obj_map_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C × D E} {X X' : C} {f : X X'} {Y : D} :
@[simp]
theorem category_theory.curry.map_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C × D E} {α : F G} {X : C} {Y : D} :
((category_theory.curry.map α).app X).app Y = α.app (X, Y)
@[simp]
theorem category_theory.currying_inverse_map_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F G : C × D E) (T : F G) (X : C) (Y : D) :
@[simp]
theorem category_theory.currying_inverse_obj_map_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C × D E) (X X' : C) (f : X X') (Y : D) :
@[simp]
theorem category_theory.currying_unit_iso_hom_app_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (X : C D E) (X_1 : C) (X_2 : D) :
@[simp]
theorem category_theory.currying_functor_obj_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C D E) (X : C × D) :
def category_theory.currying {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] :
C D E C × D E

The equivalence of functor categories given by currying/uncurrying.

Equations
@[simp]
theorem category_theory.currying_inverse_obj_obj_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C × D E) (X : C) (Y : D) :
@[simp]
theorem category_theory.currying_functor_map_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F G : C D E) (T : F G) (X : C × D) :
@[simp]
theorem category_theory.currying_inverse_obj_obj_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C × D E) (X : C) (Y Y' : D) (g : Y Y') :
@[simp]
theorem category_theory.currying_unit_iso_inv_app_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (X : C D E) (X_1 : C) (X_2 : D) :
((category_theory.currying.unit_iso.inv.app X).app X_1).app X_2 = 𝟙 ((X.obj X_1).obj X_2)
@[simp]
theorem category_theory.currying_functor_obj_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C D E) (X Y : C × D) (f : X Y) :
@[simp]
theorem category_theory.flip_iso_curry_swap_uncurry_inv_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C D E) (X : D) (X_1 : C) :
@[simp]
theorem category_theory.flip_iso_curry_swap_uncurry_hom_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C D E) (X : D) (X_1 : C) :

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

Equations

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

Equations
@[simp]
theorem category_theory.uncurry_obj_flip_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C D E) (X : D × C) :
@[simp]
theorem category_theory.uncurry_obj_flip_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C D E) (X : D × C) :