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

@[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) :
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
@[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) (T : F G) (X : C × D) :
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
@[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_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) :
((category_theory.curry.map T).app X).app Y = T.app (X, Y)
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.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_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_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) :
((category_theory.currying.unit_iso.hom.app X).app X_1).app X_2 = 𝟙 ((X.obj X_1).obj X_2)
@[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) :
def category_theory.whiskering_right₂ (B : Type u₁) [category_theory.category B] (C : Type u₂) [category_theory.category C] (D : Type u₃) [category_theory.category D] (E : Type u₄) [category_theory.category E] :
(C D E) (B C) (B D) B E

A version of category_theory.whiskering_right for bifunctors, obtained by uncurrying, applying whiskering_right and currying back

Equations
@[simp]
theorem category_theory.whiskering_right₂_map_app_app_app (B : Type u₁) [category_theory.category B] (C : Type u₂) [category_theory.category C] (D : Type u₃) [category_theory.category D] (E : Type u₄) [category_theory.category E] (_x _x_1 : C D E) (f : _x _x_1) (X : B C) (Y : B D) (c : B) :
((((category_theory.whiskering_right₂ B C D E).map f).app X).app Y).app c = (f.app (X.obj c)).app (Y.obj c)
@[simp]
theorem category_theory.whiskering_right₂_obj_map_app_app (B : Type u₁) [category_theory.category B] (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 X' : B C) (f : X_1 X') (Y : B D) (X_2 : B) :
((((category_theory.whiskering_right₂ B C D E).obj X).map f).app Y).app X_2 = (X.map (f.app X_2)).app (Y.obj X_2)
@[simp]
theorem category_theory.whiskering_right₂_obj_obj_obj_obj (B : Type u₁) [category_theory.category B] (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 : B C) (Y : B D) (X_2 : B) :
((((category_theory.whiskering_right₂ B C D E).obj X).obj X_1).obj Y).obj X_2 = (X.obj (X_1.obj X_2)).obj (Y.obj X_2)
@[simp]
theorem category_theory.whiskering_right₂_obj_obj_map_app (B : Type u₁) [category_theory.category B] (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 : B C) (Y Y' : B D) (g : Y Y') (X_2 : B) :
((((category_theory.whiskering_right₂ B C D E).obj X).obj X_1).map g).app X_2 = (X.obj (X_1.obj X_2)).map (g.app X_2)
@[simp]
theorem category_theory.whiskering_right₂_obj_obj_obj_map (B : Type u₁) [category_theory.category B] (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 : B C) (Y : B D) (_x _x_1 : B) (f : _x _x_1) :
((((category_theory.whiskering_right₂ B C D E).obj X).obj X_1).obj Y).map f = (X.map (X_1.map f)).app (Y.obj _x) (X.obj (X_1.obj _x_1)).map (Y.map f)