Documentation

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

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

Instances For

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

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

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

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

        The equivalence of functor categories given by currying/uncurrying.

        Instances For

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

          Instances For

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

            Instances For
              @[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_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)