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.

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

One or more equations did not get rendered due to their size.

Instances For

@[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

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

CategoryTheory.curryingIso = CategoryTheory.Cat.isoOfEquiv CategoryTheory.Functor.currying ⋯ ⋯ ⋯ ⋯

Instances For

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

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

@[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

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

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

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

@[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

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

CategoryTheory.flippingIso = CategoryTheory.Cat.isoOfEquiv CategoryTheory.Functor.flipping ⋯ ⋯ ⋯ ⋯

Instances For

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

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

Equations

One or more equations did not get rendered due to their size.

instance CategoryTheory.Cat.cartesianClosed :

CartesianClosed Cat

Equations

CategoryTheory.Cat.cartesianClosed = { closed := fun (C : CategoryTheory.Cat) => CategoryTheory.Cat.closed ↑C }

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

@[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