Functors to Type are closed.

Show that C ⥤ Type max w v u is monoidal closed for C a category in Type u with morphisms in Type v, and w an arbitrary universe.

TODO

It should be shown that C ⥤ Type max w v u is cartesian closed.

@[simp]

theorem CategoryTheory.FunctorToTypes.functorHomEquiv_symm_apply_app_app {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type (max w v u))) (G : CategoryTheory.Functor C (Type (max w v u))) (H : CategoryTheory.Functor C (Type (max w v u))) : ∀ (a : CategoryTheory.MonoidalCategory.tensorObj F G ⟶ H) (X : C) (a_1 : G.obj X) (Y : C) (f : (Opposite.unop (CategoryTheory.coyoneda.rightOp.obj X)).obj Y) (a_2 : F.obj Y), (((CategoryTheory.FunctorToTypes.functorHomEquiv F G H).symm a).app X a_1).app Y f a_2 = a.app Y (a_2, G.map f a_1)

@[simp]

theorem CategoryTheory.FunctorToTypes.functorHomEquiv_apply_app {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type (max w v u))) (G : CategoryTheory.Functor C (Type (max w v u))) (H : CategoryTheory.Functor C (Type (max w v u))) : ∀ (a : G ⟶ F.functorHom H) (X : C) (x : (CategoryTheory.MonoidalCategory.tensorObj F G).obj X), ((CategoryTheory.FunctorToTypes.functorHomEquiv F G H) a).app X x = match x with | (x, y) => (a.app X y).app X (CategoryTheory.CategoryStruct.id X) x

def CategoryTheory.FunctorToTypes.functorHomEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type (max w v u))) (G : CategoryTheory.Functor C (Type (max w v u))) (H : CategoryTheory.Functor C (Type (max w v u))) : (G ⟶ F.functorHom H) ≃ (CategoryTheory.MonoidalCategory.tensorObj F G ⟶ H)

When F G H : C ⥤ Type max w v u, we have (G ⟶ F.functorHom H) ≃ (F ⊗ G ⟶ H).

Equations

• CategoryTheory.FunctorToTypes.functorHomEquiv F G H = (F.functorHomEquiv H G).trans (F.homObjEquiv H G)

@[simp]

theorem CategoryTheory.FunctorToTypes.rightAdj_map_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type (max w v u))} {G : CategoryTheory.Functor C (Type (max w v u))} {H : CategoryTheory.Functor C (Type (max w v u))} (f : G ⟶ H) (c : C) (a : (F.functorHom G).obj c) (d : C) (b : (Opposite.unop (CategoryTheory.coyoneda.rightOp.obj c)).obj d) : ∀ (a_1 : F.obj d), (CategoryTheory.FunctorToTypes.rightAdj_map f c a).app d b a_1 = CategoryTheory.CategoryStruct.comp (a.app d b) (f.app d) a_1

def CategoryTheory.FunctorToTypes.rightAdj_map {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type (max w v u))} {G : CategoryTheory.Functor C (Type (max w v u))} {H : CategoryTheory.Functor C (Type (max w v u))} (f : G ⟶ H) (c : C) (a : (F.functorHom G).obj c) : (F.functorHom H).obj c

Given a morphism f : G ⟶ H, an object c : C, and an element of (F.functorHom G).obj c, construct an element of (F.functorHom H).obj c.

Equations

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

@[simp]

theorem CategoryTheory.FunctorToTypes.rightAdj_obj_map_app {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type (max w v u))) (G : CategoryTheory.Functor C (Type (max w v u))) : ∀ {X Y : C} (f : X ⟶ Y) (a : (F.homObjFunctor G).obj (CategoryTheory.coyoneda.rightOp.obj X)) (X_1 : C) (a_1 : (Opposite.unop (CategoryTheory.coyoneda.rightOp.obj Y)).obj X_1) (a_2 : F.obj X_1), (((CategoryTheory.FunctorToTypes.rightAdj F).obj G).map f a).app X_1 a_1 a_2 = a.app X_1 (CategoryTheory.CategoryStruct.comp f a_1) a_2

@[simp]

theorem CategoryTheory.FunctorToTypes.rightAdj_map_app_app {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type (max w v u))) : ∀ {X Y : CategoryTheory.Functor C (Type (max w v u))} (f : X ⟶ Y) (c : C) (a : (F.functorHom X).obj c) (d : C) (b : (Opposite.unop (CategoryTheory.coyoneda.rightOp.obj c)).obj d) (a_1 : F.obj d), (((CategoryTheory.FunctorToTypes.rightAdj F).map f).app c a).app d b a_1 = f.app d (a.app d b a_1)

@[simp]

theorem CategoryTheory.FunctorToTypes.rightAdj_obj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type (max w v u))) (G : CategoryTheory.Functor C (Type (max w v u))) (X : C) : ((CategoryTheory.FunctorToTypes.rightAdj F).obj G).obj X = F.HomObj G (CategoryTheory.coyoneda.obj (Opposite.op X))

def CategoryTheory.FunctorToTypes.rightAdj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type (max w v u))) : CategoryTheory.Functor (CategoryTheory.Functor C (Type (max w v u))) (CategoryTheory.Functor C (Type (max w v u)))

A right adjoint of tensorLeft F.

Equations

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

def CategoryTheory.FunctorToTypes.adj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type (max w v u))) : CategoryTheory.MonoidalCategory.tensorLeft F ⊣ CategoryTheory.FunctorToTypes.rightAdj F

The adjunction tensorLeft F ⊣ rightAdj F.

Equations

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

instance CategoryTheory.FunctorToTypes.closed {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type (max w v u))) : CategoryTheory.Closed F

Equations

• CategoryTheory.FunctorToTypes.closed F = { rightAdj := CategoryTheory.FunctorToTypes.rightAdj F, adj := CategoryTheory.FunctorToTypes.adj F }

instance CategoryTheory.FunctorToTypes.monoidalClosed {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.MonoidalClosed (CategoryTheory.Functor C (Type (max w v u)))

Equations

• CategoryTheory.FunctorToTypes.monoidalClosed = { closed := inferInstance }