Documentation

Mathlib.CategoryTheory.Category.Cat.CartesianClosed

Cartesian closed structure on Cat #

The category of small categories is cartesian closed, with the exponential at a category C defined by the functor category mapping out of C.

Adjoint transposition is defined by currying and uncurrying.

TODO: It would be useful to investigate and formalize further compatibilities along the lines of Cat.ihom_obj and Cat.ihom_map, relating currying of functors with currying in monoidal closed categories and precomposition with left whiskering. These may not be definitional equalities but may have to be phrased using eqToIso.

source
def CategoryTheory.Cat.exp (C : Type u) [Category.{v, u} C] :
Functor Cat Cat

A category C induces a functor from Cat to itself defined by forming the category of functors out of C.

Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Cat.exp_obj (C : Type u) [Category.{v, u} C] (D : Cat) :
      (exp C).obj D = of (Functor C ↑D)
      source
      @[simp]
      theorem CategoryTheory.Cat.exp_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : Cat} (F : X✝ ⟶ Y✝) :
      (exp C).map F = (Functor.whiskeringRight C ↑X✝ ↑Y✝).obj F
      source
      def CategoryTheory.curryingIso {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
      Cat.of (Functor C (Functor D E)) ≅ Cat.of (Functor (C × D) E)

      The isomorphism of categories of bifunctors given by currying.

      Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.curryingIso_inv_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✝) :
          ((curryingIso.inv.obj F).obj X).map g = F.map (CategoryStruct.id X, g)
          source
          @[simp]
          theorem CategoryTheory.curryingIso_inv_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) :
          ((curryingIso.inv.obj F).obj X).obj Y = F.obj (X, Y)
          source
          @[simp]
          theorem CategoryTheory.curryingIso_hom_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) :
          (curryingIso.hom.obj F).obj X = (F.obj X.1).obj X.2
          source
          @[simp]
          theorem CategoryTheory.curryingIso_inv_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) :
          ((curryingIso.inv.map T).app X).app Y = T.app (X, Y)
          source
          @[simp]
          theorem CategoryTheory.curryingIso_hom_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) :
          (curryingIso.hom.obj F).map f = CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
          source
          @[simp]
          theorem CategoryTheory.curryingIso_inv_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) :
          ((curryingIso.inv.obj F).map f).app Y = F.map (f, CategoryStruct.id Y)
          source
          @[simp]
          theorem CategoryTheory.curryingIso_hom_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) :
          (curryingIso.hom.map T).app X = (T.app X.1).app X.2
          source
          def CategoryTheory.flippingIso {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
          Cat.of (Functor C (Functor D E)) ≅ Cat.of (Functor D (Functor C E))

          The isomorphism of categories of bifunctors given by flipping the arguments.

          Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.flippingIso_hom_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) :
              ((flippingIso.hom.obj F).obj k).obj j = (F.obj j).obj k
              source
              @[simp]
              theorem CategoryTheory.flippingIso_hom_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) :
              ((flippingIso.hom.map φ).app Y).app X = (φ.app X).app Y
              source
              @[simp]
              theorem CategoryTheory.flippingIso_inv_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) :
              ((flippingIso.inv.obj F).obj k).obj j = (F.obj j).obj k
              source
              @[simp]
              theorem CategoryTheory.flippingIso_hom_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✝) :
              ((flippingIso.hom.obj F).obj k).map f = (F.map f).app k
              source
              @[simp]
              theorem CategoryTheory.flippingIso_inv_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) :
              ((flippingIso.inv.map φ).app Y).app X = (φ.app X).app Y
              source
              @[simp]
              theorem CategoryTheory.flippingIso_inv_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✝) :
              ((flippingIso.inv.obj F).obj k).map f = (F.map f).app k
              source
              @[simp]
              theorem CategoryTheory.flippingIso_hom_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) :
              ((flippingIso.hom.obj F).map f).app j = (F.obj j).map f
              source
              @[simp]
              theorem CategoryTheory.flippingIso_inv_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) :
              ((flippingIso.inv.obj F).map f).app j = (F.obj j).map f
              source
              instance CategoryTheory.Cat.closed (C : Type u) [Category.{u, u} C] :
              Closed (of C)
              Equations
                source
                instance CategoryTheory.Cat.cartesianClosed :
                CartesianClosed Cat
                Equations
                  source
                  @[simp]
                  theorem CategoryTheory.Cat.ihom_obj (C : Type u) [Category.{u, u} C] (D : Type u) [Category.{u, u} D] :
                  (ihom (of C)).obj (of D) = of (Functor C D)
                  source
                  @[simp]
                  theorem CategoryTheory.Cat.ihom_map (C : Type u) [Category.{u, u} C] {D E : Type u} [Category.{u, u} D] [Category.{u, u} E] (F : Functor D E) :
                  (ihom (of C)).map F.toCatHom = (Functor.whiskeringRight C D E).obj F