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

source
def CategoryTheory.Functor.uncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
Functor (Functor C (Functor D E)) (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.Functor.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
    source
    @[simp]
    theorem CategoryTheory.Functor.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
    source
    @[simp]
    theorem CategoryTheory.Functor.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)
    source
    def CategoryTheory.Functor.curryObj {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) :
    Functor C (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.Functor.curry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
      Functor (Functor (C × D) E) (Functor C (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.Functor.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)
        source
        @[simp]
        theorem CategoryTheory.Functor.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) :
        ((curry.obj F).map f).app Y = F.map (f, CategoryStruct.id Y)
        source
        @[simp]
        theorem CategoryTheory.Functor.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)
        source
        @[simp]
        theorem CategoryTheory.Functor.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✝) :
        ((curry.obj F).obj X).map g = F.map (CategoryStruct.id X, g)
        source
        def CategoryTheory.Functor.currying {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
        Functor C (Functor D E) ≌ 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.Functor.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) :
          ((currying.inverse.obj F).map f).app Y = F.map (f, CategoryStruct.id Y)
          source
          @[simp]
          theorem CategoryTheory.Functor.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) :
          ((currying.inverse.obj F).obj X).obj Y = F.obj (X, Y)
          source
          @[simp]
          theorem CategoryTheory.Functor.currying_counitIso_hom_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 × D) E) (X✝ : C × D) :
          (currying.counitIso.hom.app X).app X✝ = CategoryStruct.id (X.obj (X✝.1, X✝.2))
          source
          @[simp]
          theorem CategoryTheory.Functor.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✝)
          source
          @[simp]
          theorem CategoryTheory.Functor.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)
          source
          @[simp]
          theorem CategoryTheory.Functor.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✝)
          source
          @[simp]
          theorem CategoryTheory.Functor.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✝) :
          ((currying.inverse.obj F).obj X).map g = F.map (CategoryStruct.id X, g)
          source
          @[simp]
          theorem CategoryTheory.Functor.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
          source
          @[simp]
          theorem CategoryTheory.Functor.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
          source
          @[simp]
          theorem CategoryTheory.Functor.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) :
          ((currying.inverse.map T).app X).app Y = T.app (X, Y)
          source
          @[simp]
          theorem CategoryTheory.Functor.currying_counitIso_inv_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 × D) E) (X✝ : C × D) :
          (currying.counitIso.inv.app X).app X✝ = CategoryStruct.id (X.obj (X✝.1, X✝.2))
          source
          def CategoryTheory.Functor.fullyFaithfulUncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
          uncurry.FullyFaithful

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

          Equations
          Instances For
            source
            instance CategoryTheory.Functor.instFullProdUncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
            uncurry.Full
            source
            instance CategoryTheory.Functor.instFaithfulProdUncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
            uncurry.Faithful
            source
            def CategoryTheory.Functor.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
              source
              @[simp]
              theorem CategoryTheory.Functor.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') :
              ((F₁.curryObjProdComp F₂ G).inv.app X).app X✝ = CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X✝))
              source
              @[simp]
              theorem CategoryTheory.Functor.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') :
              ((F₁.curryObjProdComp F₂ G).hom.app X).app X✝ = CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X✝))
              source
              def CategoryTheory.Functor.flipIsoCurrySwapUncurry {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)) :
              F.flip ≅ curry.obj ((Prod.swap D C).comp (uncurry.obj F))

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

              Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.Functor.flipIsoCurrySwapUncurry_inv_app_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 (Functor D E)) (X : D) (X✝ : C) :
                (F.flipIsoCurrySwapUncurry.inv.app X).app X✝ = CategoryStruct.id ((F.obj X✝).obj X)
                source
                @[simp]
                theorem CategoryTheory.Functor.flipIsoCurrySwapUncurry_hom_app_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 (Functor D E)) (X : D) (X✝ : C) :
                (F.flipIsoCurrySwapUncurry.hom.app X).app X✝ = CategoryStruct.id ((F.obj X✝).obj X)
                source
                def CategoryTheory.Functor.uncurryObjFlip {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)) :
                uncurry.obj F.flip ≅ (Prod.swap D C).comp (uncurry.obj F)

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

                Equations
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.uncurryObjFlip_hom_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 (Functor D E)) (X : D × C) :
                  F.uncurryObjFlip.hom.app X = CategoryStruct.id ((F.obj X.2).obj X.1)
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.uncurryObjFlip_inv_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 (Functor D E)) (X : D × C) :
                  F.uncurryObjFlip.inv.app X = CategoryStruct.id ((F.obj X.2).obj X.1)
                  source
                  def CategoryTheory.Functor.whiskeringRight₂ (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] :
                  Functor (Functor C (Functor D E)) (Functor (Functor B C) (Functor (Functor B D) (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.Functor.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✝)
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.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))
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.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)
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.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✝)
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.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✝¹)
                    source
                    theorem CategoryTheory.Functor.uncurry_obj_curry_obj {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (F : Functor (B × C) D) :
                    uncurry.obj (curry.obj F) = F
                    source
                    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₂
                    source
                    theorem CategoryTheory.Functor.curry_obj_uncurry_obj {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (F : Functor B (Functor C D)) :
                    curry.obj (uncurry.obj F) = F
                    source
                    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₂
                    source
                    theorem CategoryTheory.Functor.flip_flip {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (F : Functor B (Functor C D)) :
                    F.flip.flip = F
                    source
                    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₂
                    source
                    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
                    source
                    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