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

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
    @[simp]
    theorem CategoryTheory.uncurry_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) {X Y : C × D} (f : X Y) :
    (uncurry.obj F).map f = CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
    @[simp]
    theorem CategoryTheory.uncurry_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : C × D) :
    (uncurry.obj F).obj X = (F.obj X.1).obj X.2
    @[simp]
    theorem CategoryTheory.uncurry_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {X✝ Y✝ : Functor C (Functor D E)} (T : X✝ Y✝) (X : C × D) :
    (uncurry.map T).app X = (T.app X.1).app X.2

    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

      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
        @[simp]
        theorem CategoryTheory.curry_obj_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ Y✝) (Y : D) :
        @[simp]
        theorem CategoryTheory.curry_obj_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ Y✝) :
        @[simp]
        theorem CategoryTheory.curry_obj_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) (Y : D) :
        ((curry.obj F).obj X).obj Y = F.obj (X, Y)
        @[simp]
        theorem CategoryTheory.curry_map_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {X✝ Y✝ : Functor (C × D) E} (T : X✝ Y✝) (X : C) (Y : D) :
        ((curry.map T).app X).app Y = T.app (X, Y)

        The equivalence of functor categories given by currying/uncurrying.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.currying_unitIso_hom_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : C) (X✝ : D) :
          ((currying.unitIso.hom.app X).app X✝).app X✝ = CategoryStruct.id ((X.obj X✝).obj X✝)
          @[simp]
          theorem CategoryTheory.currying_inverse_obj_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) (Y : D) :
          @[simp]
          theorem CategoryTheory.currying_functor_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {X✝ Y✝ : Functor C (Functor D E)} (T : X✝ Y✝) (X : C × D) :
          (currying.functor.map T).app X = (T.app X.1).app X.2
          @[simp]
          theorem CategoryTheory.currying_inverse_obj_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ Y✝) (Y : D) :
          @[simp]
          theorem CategoryTheory.currying_functor_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : C × D) :
          (currying.functor.obj F).obj X = (F.obj X.1).obj X.2
          @[simp]
          theorem CategoryTheory.currying_unitIso_inv_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : C) (X✝ : D) :
          ((currying.unitIso.inv.app X).app X✝).app X✝ = CategoryStruct.id ((X.obj X✝).obj X✝)
          @[simp]
          theorem CategoryTheory.currying_inverse_obj_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ Y✝) :
          @[simp]
          theorem CategoryTheory.currying_functor_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) {X Y : C × D} (f : X Y) :
          (currying.functor.obj F).map f = CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
          @[simp]
          theorem CategoryTheory.currying_inverse_map_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {X✝ Y✝ : Functor (C × D) E} (T : X✝ Y✝) (X : C) (Y : D) :

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

          Equations
          Instances For
            def CategoryTheory.curryObjProdComp {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {C' : Type u_1} {D' : Type u_2} [Category.{u_3, u_1} C'] [Category.{u_4, u_2} D'] (F₁ : Functor C D) (F₂ : Functor C' D') (G : Functor (D × D') E) :
            curry.obj ((F₁.prod F₂).comp G) F₁.comp ((curry.obj G).comp ((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
              @[simp]
              theorem CategoryTheory.curryObjProdComp_inv_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {C' : Type u_1} {D' : Type u_2} [Category.{u_3, u_1} C'] [Category.{u_4, u_2} D'] (F₁ : Functor C D) (F₂ : Functor C' D') (G : Functor (D × D') E) (X : C) (X✝ : C') :
              ((curryObjProdComp F₁ F₂ G).inv.app X).app X✝ = CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X✝))
              @[simp]
              theorem CategoryTheory.curryObjProdComp_hom_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {C' : Type u_1} {D' : Type u_2} [Category.{u_3, u_1} C'] [Category.{u_4, u_2} D'] (F₁ : Functor C D) (F₂ : Functor C' D') (G : Functor (D × D') E) (X : C) (X✝ : C') :
              ((curryObjProdComp F₁ F₂ G).hom.app X).app X✝ = CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X✝))

              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

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

                Equations
                Instances For

                  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
                    @[simp]
                    theorem CategoryTheory.whiskeringRight₂_obj_map_app_app (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) {X✝ Y✝ : Functor B C} (f : X✝ Y✝) (Y : Functor B D) (X✝¹ : B) :
                    ((((whiskeringRight₂ B C D E).obj X).map f).app Y).app X✝¹ = (X.map (f.app X✝¹)).app (Y.obj X✝¹)
                    @[simp]
                    theorem CategoryTheory.whiskeringRight₂_obj_obj_map_app (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : Functor B C) {X✝¹ Y✝ : Functor B D} (g : X✝¹ Y✝) (X✝ : B) :
                    ((((whiskeringRight₂ B C D E).obj X).obj X✝).map g).app X✝ = (X.obj (X✝.obj X✝)).map (g.app X✝)
                    @[simp]
                    theorem CategoryTheory.whiskeringRight₂_obj_obj_obj_map (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : Functor B C) (Y : Functor B D) {X✝¹ Y✝ : B} (f : X✝¹ Y✝) :
                    ((((whiskeringRight₂ B C D E).obj X).obj X✝).obj Y).map f = CategoryStruct.comp ((X.map (X✝.map f)).app (Y.obj X✝¹)) ((X.obj (X✝.obj Y✝)).map (Y.map f))
                    @[simp]
                    theorem CategoryTheory.whiskeringRight₂_map_app_app_app (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] {X✝ Y✝ : Functor C (Functor D E)} (f : X✝ Y✝) (X : Functor B C) (Y : Functor B D) (c : B) :
                    ((((whiskeringRight₂ B C D E).map f).app X).app Y).app c = (f.app (X.obj c)).app (Y.obj c)
                    @[simp]
                    theorem CategoryTheory.whiskeringRight₂_obj_obj_obj_obj (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : Functor B C) (Y : Functor B D) (X✝ : B) :
                    ((((whiskeringRight₂ B C D E).obj X).obj X✝).obj Y).obj X✝ = (X.obj (X✝.obj X✝)).obj (Y.obj X✝)
                    theorem CategoryTheory.Functor.curry_obj_injective {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {F₁ F₂ : Functor (C × D) E} (h : curry.obj F₁ = curry.obj F₂) :
                    F₁ = F₂
                    theorem CategoryTheory.Functor.uncurry_obj_injective {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {F₁ F₂ : Functor B (Functor C D)} (h : uncurry.obj F₁ = uncurry.obj F₂) :
                    F₁ = F₂
                    theorem CategoryTheory.Functor.flip_injective {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {F₁ F₂ : Functor B (Functor C D)} (h : F₁.flip = F₂.flip) :
                    F₁ = F₂
                    theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {H : Type u₅} [Category.{v₅, u₅} H] (F₁ : Functor B C) (F₂ : Functor D E) (G : Functor (C × E) H) :
                    uncurry.obj (F₂.comp (F₁.comp (curry.obj G)).flip).flip = (F₁.prod F₂).comp G
                    theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip' {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {H : Type u₅} [Category.{v₅, u₅} H] (F₁ : Functor B C) (F₂ : Functor D E) (G : Functor (C × E) H) :
                    uncurry.obj (F₁.comp (F₂.comp (curry.obj G).flip).flip) = (F₁.prod F₂).comp G