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

This is used in CategoryTheory.Category.Cat.CartesianClosed to equip the category of small categories Cat.{u, u} with a Cartesian-closed structure.

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_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
        @[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_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
        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_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_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_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
          @[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_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_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_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_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_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
          def CategoryTheory.Functor.flipping {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 D (Functor C E)

          The equivalence of functor categories given by flipping.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_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) :
            ((flipping.unitIso.inv.app X).app X✝).app X✝¹ = CategoryStruct.id ((X.obj X✝).obj X✝¹)
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_functor_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 (Functor D E)) (k : D) (j : C) :
            ((flipping.functor.obj F).obj k).obj j = (F.obj j).obj k
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_functor_map_app_app {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 (Functor D E)} (φ : F₁ ⟶ F₂) (Y : D) (X : C) :
            ((flipping.functor.map φ).app Y).app X = (φ.app X).app Y
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_functor_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 (Functor D E)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) :
            ((flipping.functor.obj F).map f).app j = (F.obj j).map f
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_functor_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 (Functor D E)) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
            ((flipping.functor.obj F).obj k).map f = (F.map f).app k
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_counitIso_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 D (Functor C E)) (X✝ : D) (X✝¹ : C) :
            ((flipping.counitIso.hom.app X).app X✝).app X✝¹ = CategoryStruct.id ((X.obj X✝).obj X✝¹)
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_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 D (Functor C E)) (k : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
            ((flipping.inverse.obj F).obj k).map f = (F.map f).app k
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_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] {F₁ F₂ : Functor D (Functor C E)} (φ : F₁ ⟶ F₂) (Y : C) (X : D) :
            ((flipping.inverse.map φ).app Y).app X = (φ.app X).app Y
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_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) :
            ((flipping.unitIso.hom.app X).app X✝).app X✝¹ = CategoryStruct.id ((X.obj X✝).obj X✝¹)
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_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 D (Functor C E)) (k : C) (j : D) :
            ((flipping.inverse.obj F).obj k).obj j = (F.obj j).obj k
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_counitIso_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 D (Functor C E)) (X✝ : D) (X✝¹ : C) :
            ((flipping.counitIso.inv.app X).app X✝).app X✝¹ = CategoryStruct.id ((X.obj X✝).obj X✝¹)
            source
            @[simp]
            theorem CategoryTheory.Functor.flipping_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 D (Functor C E)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : D) :
            ((flipping.inverse.obj F).map f).app j = (F.obj j).map f
            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_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
                    @[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
                    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_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
                      @[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₂_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_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₂_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
                      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
                      source
                      def CategoryTheory.Functor.compFlipUncurryIso {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] (F : Functor B D) (G : Functor D (Functor C E)) :
                      uncurry.obj (F.comp G).flip ≅ ((Functor.id C).prod F).comp (uncurry.obj G.flip)

                      Natural isomorphism witnessing comp_flip_uncurry_eq.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.Functor.compFlipUncurryIso_inv_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] (F : Functor B D) (G : Functor D (Functor C E)) (X : C × B) :
                        (F.compFlipUncurryIso G).inv.app X = CategoryStruct.id ((G.obj (F.obj X.2)).obj X.1)
                        source
                        @[simp]
                        theorem CategoryTheory.Functor.compFlipUncurryIso_hom_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] (F : Functor B D) (G : Functor D (Functor C E)) (X : C × B) :
                        (F.compFlipUncurryIso G).hom.app X = CategoryStruct.id ((G.obj (F.obj X.2)).obj X.1)
                        source
                        theorem CategoryTheory.Functor.comp_flip_uncurry_eq {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] (F : Functor B D) (G : Functor D (Functor C E)) :
                        uncurry.obj (F.comp G).flip = ((Functor.id C).prod F).comp (uncurry.obj G.flip)
                        source
                        def CategoryTheory.Functor.curryObjCompIso {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] (F : Functor (C × B) D) (G : Functor D E) :
                        (curry.obj (F.comp G)).flip ≅ (curry.obj F).flip.comp ((whiskeringRight C D E).obj G)

                        Natural isomorphism witnessing comp_flip_curry_eq.

                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.Functor.curryObjCompIso_hom_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] (F : Functor (C × B) D) (G : Functor D E) (X : B) (X✝ : C) :
                          ((F.curryObjCompIso G).hom.app X).app X✝ = CategoryStruct.id (G.obj (F.obj (X✝, X)))
                          source
                          @[simp]
                          theorem CategoryTheory.Functor.curryObjCompIso_inv_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] (F : Functor (C × B) D) (G : Functor D E) (X : B) (X✝ : C) :
                          ((F.curryObjCompIso G).inv.app X).app X✝ = CategoryStruct.id (G.obj (F.obj (X✝, X)))
                          source
                          theorem CategoryTheory.Functor.curry_obj_comp_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] (F : Functor (C × B) D) (G : Functor D E) :
                          (curry.obj (F.comp G)).flip = (curry.obj F).flip.comp ((whiskeringRight C D E).obj G)
                          source
                          def CategoryTheory.Functor.flippingEquiv {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 D (Functor C E)

                          The equivalence of types of bifunctors giving by flipping the arguments.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.flippingEquiv_symm_apply_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 D (Functor C E)) (k : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
                            ((flippingEquiv.symm F).obj k).map f = (F.map f).app k
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.flippingEquiv_apply_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)) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                            ((flippingEquiv F).obj k).map f = (F.map f).app k
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.flippingEquiv_apply_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 (Functor D E)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) :
                            ((flippingEquiv F).map f).app j = (F.obj j).map f
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.flippingEquiv_symm_apply_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 D (Functor C E)) (k : C) (j : D) :
                            ((flippingEquiv.symm F).obj k).obj j = (F.obj j).obj k
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.flippingEquiv_symm_apply_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 D (Functor C E)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : D) :
                            ((flippingEquiv.symm F).map f).app j = (F.obj j).map f
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.flippingEquiv_apply_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)) (k : D) (j : C) :
                            ((flippingEquiv F).obj k).obj j = (F.obj j).obj k
                            source
                            def CategoryTheory.Functor.curryingEquiv {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 types of bifunctors given by currying.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.curryingEquiv_symm_apply_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (G : Functor (C × D) E) (X : C) (Y : D) :
                              ((curryingEquiv.symm G).obj X).obj Y = G.obj (X, Y)
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.curryingEquiv_symm_apply_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (G : Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) :
                              ((curryingEquiv.symm G).obj X).map g = G.map (CategoryStruct.id X, g)
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.curryingEquiv_symm_apply_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (G : Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) :
                              ((curryingEquiv.symm G).map f).app Y = G.map (f, CategoryStruct.id Y)
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.curryingEquiv_apply_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) :
                              (curryingEquiv F).obj X = (F.obj X.1).obj X.2
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.curryingEquiv_apply_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) :
                              (curryingEquiv F).map f = CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
                              source
                              def CategoryTheory.Functor.curryingFlipEquiv {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
                              Functor D (Functor C E) ≃ Functor (C × D) E

                              The flipped equivalence of types of bifunctors given by currying.

                              Equations
                              Instances For
                                source
                                @[simp]
                                theorem CategoryTheory.Functor.curryingFlipEquiv_symm_apply_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor (C × D) E) (k : D) (j : C) :
                                ((curryingFlipEquiv.symm a✝).obj k).obj j = a✝.obj (j, k)
                                source
                                @[simp]
                                theorem CategoryTheory.Functor.curryingFlipEquiv_symm_apply_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor (C × D) E) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) :
                                ((curryingFlipEquiv.symm a✝).map f).app j = a✝.map (CategoryStruct.id j, f)
                                source
                                @[simp]
                                theorem CategoryTheory.Functor.curryingFlipEquiv_symm_apply_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor (C × D) E) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                                ((curryingFlipEquiv.symm a✝).obj k).map f = a✝.map (f, CategoryStruct.id k)
                                source
                                @[simp]
                                theorem CategoryTheory.Functor.curryingFlipEquiv_apply_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor D (Functor C E)) (X : C × D) :
                                (curryingFlipEquiv a✝).obj X = (a✝.obj X.2).obj X.1
                                source
                                @[simp]
                                theorem CategoryTheory.Functor.curryingFlipEquiv_apply_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor D (Functor C E)) {X Y : C × D} (f : X ⟶ Y) :
                                (curryingFlipEquiv a✝).map f = CategoryStruct.comp ((a✝.map f.2).app X.1) ((a✝.obj Y.2).map f.1)