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.

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.

@[simp]

theorem CategoryTheory.Cat.exp_obj (C : Type u) [Category.{v, u} C] (D : Cat) : (exp C).obj D = of (Functor C ↑D)

@[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.toFunctor).toCatHom

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.

@[simp]

theorem CategoryTheory.curryingIso_inv_toFunctor_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.toFunctor.obj F).obj X).map g = F.map (Prod.mkHom (CategoryStruct.id X) g)

@[simp]

theorem CategoryTheory.curryingIso_inv_toFunctor_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.toFunctor.obj F).map f).app Y = F.map (Prod.mkHom f (CategoryStruct.id Y))

@[simp]

theorem CategoryTheory.curryingIso_inv_toFunctor_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.toFunctor.map T).app X).app Y = T.app (X, Y)

@[simp]

theorem CategoryTheory.curryingIso_hom_toFunctor_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.toFunctor.obj F).obj X = (F.obj X.1).obj X.2

@[simp]

theorem CategoryTheory.curryingIso_hom_toFunctor_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.toFunctor.map T).app X = (T.app X.1).app X.2

@[simp]

theorem CategoryTheory.curryingIso_inv_toFunctor_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.toFunctor.obj F).obj X).obj Y = F.obj (X, Y)

@[simp]

theorem CategoryTheory.curryingIso_hom_toFunctor_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.toFunctor.obj F).map f = CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)

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.

@[simp]

theorem CategoryTheory.flippingIso_inv_toFunctor_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.toFunctor.map φ).app Y).app X = (φ.app X).app Y

@[simp]

theorem CategoryTheory.flippingIso_inv_toFunctor_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.toFunctor.obj F).obj k).obj j = (F.obj j).obj k

@[simp]

theorem CategoryTheory.flippingIso_inv_toFunctor_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.toFunctor.obj F).obj k).map f = (F.map f).app k

@[simp]

theorem CategoryTheory.flippingIso_hom_toFunctor_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.toFunctor.obj F).obj k).obj j = (F.obj j).obj k

@[simp]

theorem CategoryTheory.flippingIso_hom_toFunctor_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.toFunctor.obj F).obj k).map f = (F.map f).app k

@[simp]

theorem CategoryTheory.flippingIso_hom_toFunctor_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.toFunctor.obj F).map f).app j = (F.obj j).map f

@[simp]

theorem CategoryTheory.flippingIso_inv_toFunctor_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.toFunctor.obj F).map f).app j = (F.obj j).map f

@[simp]

theorem CategoryTheory.flippingIso_hom_toFunctor_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.toFunctor.map φ).app Y).app X = (φ.app X).app Y

@[implicit_reducible]

instance CategoryTheory.Cat.closed (C : Type u) [Category.{u, u} C] : Closed (of C)

@[implicit_reducible]

instance CategoryTheory.Cat.cartesianClosed : MonoidalClosed Cat

@[simp]

theorem CategoryTheory.Cat.ihom_obj (C : Type u) [Category.{u, u} C] (D : Type u) [Category.{u, u} D] : (of C ⟹ of D) = of (Functor C D)

@[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).toCatHom