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

source

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.

Instances For

source

@[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 Y : C × D} (f : X ⟶ Y) :

(CategoryTheory.uncurry.obj F).map f = CategoryTheory.CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)

source

@[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.1).obj X.2

source

@[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 : C × D) :

(CategoryTheory.uncurry.map T).app X = (T.app X.1).app X.2

source

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.

Instances For

source

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.

Instances For

source

@[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 : D) :

((CategoryTheory.curry.obj F).map f).app Y = F.map (f, CategoryTheory.CategoryStruct.id Y)

source

@[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)

source

@[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)

source

@[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 : C) (Y : D) :

((CategoryTheory.curry.map T).app X).app Y = T.app (X, Y)

source

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.

Instances For

source

@[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✝)

source

@[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)

source

@[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 : C × D) :

(CategoryTheory.currying.functor.map T).app X = (T.app X.1).app X.2

source

@[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 : D) :

((CategoryTheory.currying.inverse.obj F).map f).app Y = F.map (f, CategoryTheory.CategoryStruct.id Y)

source

@[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.1).obj X.2

source

@[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✝)

source

@[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)

source

@[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 Y : C × D} (f : X ⟶ Y) :

(CategoryTheory.currying.functor.obj F).map f = CategoryTheory.CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)

source

@[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✝.1, X✝.2))

source

@[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 : C) (Y : D) :

((CategoryTheory.currying.inverse.map T).app X).app Y = T.app (X, Y)

source

@[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✝.1, X✝.2))

source

def CategoryTheory.fullyFaithfulUncurry {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.uncurry.FullyFaithful

The functor uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E is fully faithful.

Equations

CategoryTheory.fullyFaithfulUncurry = CategoryTheory.currying.fullyFaithfulFunctor

Instances For

source

instance CategoryTheory.instFullFunctorProdUncurry {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.uncurry.Full

source

instance CategoryTheory.instFaithfulFunctorProdUncurry {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.uncurry.Faithful

source

def CategoryTheory.curryObjProdComp {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] {C' : Type u_1} {D' : Type u_2} [CategoryTheory.Category.{u_3, u_1} C'] [CategoryTheory.Category.{u_4, u_2} D'] (F₁ : CategoryTheory.Functor C D) (F₂ : CategoryTheory.Functor C' D') (G : CategoryTheory.Functor (D × D') E) :

CategoryTheory.curry.obj ((F₁.prod F₂).comp G) ≅ F₁.comp ((CategoryTheory.curry.obj G).comp ((CategoryTheory.whiskeringLeft C' D' E).obj F₂))

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

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.curryObjProdComp_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] {C' : Type u_1} {D' : Type u_2} [CategoryTheory.Category.{u_3, u_1} C'] [CategoryTheory.Category.{u_4, u_2} D'] (F₁ : CategoryTheory.Functor C D) (F₂ : CategoryTheory.Functor C' D') (G : CategoryTheory.Functor (D × D') E) (X : C) (X✝ : C') :

((CategoryTheory.curryObjProdComp F₁ F₂ G).inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X✝))

source

@[simp]

theorem CategoryTheory.curryObjProdComp_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] {C' : Type u_1} {D' : Type u_2} [CategoryTheory.Category.{u_3, u_1} C'] [CategoryTheory.Category.{u_4, u_2} D'] (F₁ : CategoryTheory.Functor C D) (F₂ : CategoryTheory.Functor C' D') (G : CategoryTheory.Functor (D × D') E) (X : C) (X✝ : C') :

((CategoryTheory.curryObjProdComp F₁ F₂ G).hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X✝))

source

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

F.flip ≅ CategoryTheory.curry.obj ((CategoryTheory.Prod.swap D C).comp (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.

Instances For

source

@[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)

source

@[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)

source

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 F.flip ≅ (CategoryTheory.Prod.swap D C).comp (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 (x : D × C) => CategoryTheory.Iso.refl ((CategoryTheory.uncurry.obj F.flip).obj x)) ⋯

Instances For

source

@[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.2).obj X.1)

source

@[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.2).obj X.1)

source

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.

Instances For

source

@[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 : CategoryTheory.Functor B D) (X✝¹ : B) :

((((CategoryTheory.whiskeringRight₂ B C D E).obj X).map f).app Y).app X✝¹ = (X.map (f.app X✝¹)).app (Y.obj X✝¹)

source

@[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✝ : B) :

((((CategoryTheory.whiskeringRight₂ B C D E).obj X).obj X✝).map g).app X✝ = (X.obj (X✝.obj X✝)).map (g.app X✝)

source

@[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))

source

@[simp]