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.
def
CategoryTheory.FunctorToTypes.functorHomEquiv
{C : Type u}
[Category.{v, u} C]
(F G H : Functor C (Type (max w v u)))
:
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)
Instances For
@[simp]
theorem
CategoryTheory.FunctorToTypes.functorHomEquiv_symm_apply_app_app
{C : Type u}
[Category.{v, u} C]
(F G H : Functor C (Type (max w v u)))
(a✝ : MonoidalCategoryStruct.tensorObj F G ⟶ H)
(X : C)
(a : G.obj X)
(Y : C)
(f : (Opposite.unop (coyoneda.rightOp.obj X)).obj Y)
(a✝¹ : F.obj Y)
:
@[simp]
theorem
CategoryTheory.FunctorToTypes.functorHomEquiv_apply_app
{C : Type u}
[Category.{v, u} C]
(F G H : Functor C (Type (max w v u)))
(a✝ : G ⟶ F.functorHom H)
(X : C)
(x✝ : (MonoidalCategoryStruct.tensorObj F G).obj X)
:
((functorHomEquiv F G H) a✝).app X x✝ = match x✝ with
| (x, y) => (a✝.app X y).app X (CategoryStruct.id X) x
def
CategoryTheory.FunctorToTypes.rightAdj_map
{C : Type u}
[Category.{v, u} C]
{F G H : 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.
Instances For
@[simp]
theorem
CategoryTheory.FunctorToTypes.rightAdj_map_app
{C : Type u}
[Category.{v, u} C]
{F G H : Functor C (Type (max w v u))}
(f : G ⟶ H)
(c : C)
(a : (F.functorHom G).obj c)
(d : C)
(b : (Opposite.unop (coyoneda.rightOp.obj c)).obj d)
(a✝ : F.obj d)
:
def
CategoryTheory.FunctorToTypes.rightAdj
{C : Type u}
[Category.{v, u} C]
(F : 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.
Instances For
@[simp]
theorem
CategoryTheory.FunctorToTypes.rightAdj_obj_map_app
{C : Type u}
[Category.{v, u} C]
(F G : Functor C (Type (max w v u)))
{X✝ Y✝ : C}
(f : X✝ ⟶ Y✝)
(a✝ : (F.homObjFunctor G).obj (coyoneda.rightOp.obj X✝))
(X : C)
(a : (Opposite.unop (coyoneda.rightOp.obj Y✝)).obj X)
(a✝¹ : F.obj X)
:
@[simp]
theorem
CategoryTheory.FunctorToTypes.rightAdj_map_app_app
{C : Type u}
[Category.{v, u} C]
(F : Functor C (Type (max w v u)))
{X✝ Y✝ : Functor C (Type (max w v u))}
(f : X✝ ⟶ Y✝)
(c : C)
(a : (F.functorHom X✝).obj c)
(d : C)
(b : (Opposite.unop (coyoneda.rightOp.obj c)).obj d)
(a✝ : F.obj d)
:
@[simp]
theorem
CategoryTheory.FunctorToTypes.rightAdj_obj_obj
{C : Type u}
[Category.{v, u} C]
(F G : Functor C (Type (max w v u)))
(X : C)
:
def
CategoryTheory.FunctorToTypes.adj
{C : Type u}
[Category.{v, u} C]
(F : Functor C (Type (max w v u)))
:
The adjunction tensorLeft F ⊣ rightAdj F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.FunctorToTypes.closed
{C : Type u}
[Category.{v, u} C]
(F : Functor C (Type (max w v u)))
:
Closed F
Equations
- CategoryTheory.FunctorToTypes.closed F = { rightAdj := CategoryTheory.FunctorToTypes.rightAdj F, adj := CategoryTheory.FunctorToTypes.adj F }
instance
CategoryTheory.FunctorToTypes.monoidalClosed
{C : Type u}
[Category.{v, u} C]
:
MonoidalClosed (Functor C (Type (max w v u)))
Equations
- CategoryTheory.FunctorToTypes.monoidalClosed = { closed := inferInstance }