Internal hom in functor categories #
Given functors F G : C ⥤ D, define a functor functorHom F G from C to Type max v' v u,
which is a proxy for the "internal hom" functor Hom(F ⊗ coyoneda(-), G). This is used to show
that the functor category C ⥤ D is enriched over C ⥤ Type max v' v u. This is also useful
for showing that C ⥤ Type max w v u is monoidal closed.
structure
CategoryTheory.Functor.HomObj
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(F G : Functor C D)
(A : Functor C (Type w))
:
Type (max (max u v') w)
Given functors F G : C ⥤ D, HomObj F G A is a proxy for the type
of "morphisms" F ⊗ A ⟶ G, where A : C ⥤ Type w (w an arbitrary universe).
The morphism
F.obj c ⟶ G.obj cassociated witha : A.obj c.- naturality {c d : C} (f : c ⟶ d) (a : A.obj c) : CategoryStruct.comp (F.map f) (self.app d (A.map f a)) = CategoryStruct.comp (self.app c a) (G.map f)
theorem
CategoryTheory.Functor.HomObj.ext
{C : Type u}
{inst✝ : Category.{v, u} C}
{D : Type u'}
{inst✝¹ : Category.{v', u'} D}
{F G : Functor C D}
{A : Functor C (Type w)}
{x y : F.HomObj G A}
(app : x.app = y.app)
:
theorem
CategoryTheory.Functor.HomObj.ext_iff
{C : Type u}
{inst✝ : Category.{v, u} C}
{D : Type u'}
{inst✝¹ : Category.{v', u'} D}
{F G : Functor C D}
{A : Functor C (Type w)}
{x y : F.HomObj G A}
:
def
CategoryTheory.Functor.homObjEquiv
{C : Type u}
[Category.{v, u} C]
(F G A : Functor C (Type w))
:
When F, G, and A are all functors C ⥤ Type w, then HomObj F G A is in
bijection with F ⊗ A ⟶ G.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Functor.homObjEquiv_apply_app
{C : Type u}
[Category.{v, u} C]
(F G A : Functor C (Type w))
(a : F.HomObj G A)
(X : C)
(x✝ : (MonoidalCategoryStruct.tensorObj F A).obj X)
:
@[simp]
theorem
CategoryTheory.Functor.homObjEquiv_symm_apply_app
{C : Type u}
[Category.{v, u} C]
(F G A : Functor C (Type w))
(a : MonoidalCategoryStruct.tensorObj F A ⟶ G)
(X : C)
(y : A.obj X)
(x : F.obj X)
:
@[simp]
theorem
CategoryTheory.Functor.HomObj.naturality_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
{A : Functor C (Type w)}
(self : F.HomObj G A)
{c d : C}
(f : c ⟶ d)
(a : A.obj c)
{Z : D}
(h : G.obj d ⟶ Z)
:
CategoryStruct.comp (F.map f) (CategoryStruct.comp (self.app d (A.map f a)) h) = CategoryStruct.comp (self.app c a) (CategoryStruct.comp (G.map f) h)
theorem
CategoryTheory.Functor.HomObj.congr_app
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
{A : Functor C (Type w)}
{f g : F.HomObj G A}
(h : f = g)
(X : C)
(a : A.obj X)
:
def
CategoryTheory.Functor.HomObj.ofNatTrans
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
{A : Functor C (Type w)}
(f : F ⟶ G)
:
F.HomObj G A
Given a natural transformation F ⟶ G, get a term of HomObj F G A by "ignoring" A.
@[simp]
theorem
CategoryTheory.Functor.HomObj.ofNatTrans_app
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
{A : Functor C (Type w)}
(f : F ⟶ G)
(X : C)
(x✝ : A.obj X)
:
def
CategoryTheory.Functor.HomObj.id
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F : Functor C D}
(A : Functor C (Type w))
:
F.HomObj F A
The identity HomObj F F A.
@[simp]
theorem
CategoryTheory.Functor.HomObj.id_app
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F : Functor C D}
(A : Functor C (Type w))
(X : C)
(x✝ : A.obj X)
:
def
CategoryTheory.Functor.HomObj.comp
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
{A : Functor C (Type w)}
{M : Functor C D}
(f : F.HomObj G A)
(g : G.HomObj M A)
:
F.HomObj M A
@[simp]
theorem
CategoryTheory.Functor.HomObj.comp_app
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
{A : Functor C (Type w)}
{M : Functor C D}
(f : F.HomObj G A)
(g : G.HomObj M A)
(X : C)
(a : A.obj X)
:
def
CategoryTheory.Functor.HomObj.map
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
{A A' : Functor C (Type w)}
(f : A' ⟶ A)
(x : F.HomObj G A)
:
F.HomObj G A'
Given a morphism A' ⟶ A, send a term of HomObj F G A to a term of HomObj F G A'.
def
CategoryTheory.Functor.homObjFunctor
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(F G : Functor C D)
:
The contravariant functor taking A : C ⥤ Type w to HomObj F G A, i.e. Hom(F ⊗ -, G).
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Functor.homObjFunctor_obj
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(F G : Functor C D)
(A : (Functor C (Type w))ᵒᵖ)
:
@[simp]
theorem
CategoryTheory.Functor.homObjFunctor_map_app
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(F G : Functor C D)
{A A' : (Functor C (Type w))ᵒᵖ}
(f : A ⟶ A')
(x : F.HomObj G (Opposite.unop A))
(X : C)
(a : (Opposite.unop A').obj X)
:
def
CategoryTheory.Functor.functorHom
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(F G : Functor C D)
:
Composition of homObjFunctor with the co-Yoneda embedding, i.e. Hom(F ⊗ coyoneda(-), G).
When F G : C ⥤ Type max v' v u, this is the internal hom of F and G: see
Mathlib/CategoryTheory/Closed/FunctorToTypes.lean.
Equations
- F.functorHom G = CategoryTheory.coyoneda.rightOp.comp (F.homObjFunctor G)
theorem
CategoryTheory.Functor.functorHom_ext
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
{X : C}
{x y : (F.functorHom G).obj X}
(h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f)
:
theorem
CategoryTheory.Functor.functorHom_ext_iff
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
{X : C}
{x y : (F.functorHom G).obj X}
:
def
CategoryTheory.Functor.functorHomEquiv
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(F G : Functor C D)
(A : Functor C (Type (max u v v')))
:
The equivalence (A ⟶ F.functorHom G) ≃ HomObj F G A.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Functor.functorHomEquiv_symm_apply_app_app
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(F G : Functor C D)
(A : Functor C (Type (max u v v')))
(x : F.HomObj G A)
(X : C)
(a : A.obj X)
(Y : C)
(f : (Opposite.unop (coyoneda.rightOp.obj X)).obj Y)
:
@[simp]
theorem
CategoryTheory.Functor.functorHomEquiv_apply_app
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(F G : Functor C D)
(A : Functor C (Type (max u v v')))
(φ : A ⟶ F.functorHom G)
(X : C)
(a : A.obj X)
:
((F.functorHomEquiv G A) φ).app X a = (φ.app X a).app X (CategoryStruct.id (Opposite.unop (Opposite.op X)))
def
CategoryTheory.Functor.natTransEquiv
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
:
Morphisms (𝟙_ (C ⥤ Type max v' v u) ⟶ F.functorHom G) are in bijection with
morphisms F ⟶ G.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Functor.natTransEquiv_symm_apply_app
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
(f : F ⟶ G)
(x✝ : C)
(x✝¹ : (MonoidalCategoryStruct.tensorUnit (Functor C (Type (max v' v u)))).obj x✝)
:
@[simp]
theorem
CategoryTheory.Functor.natTransEquiv_apply_app
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F G : Functor C D}
(f : MonoidalCategoryStruct.tensorUnit (Functor C (Type (max v' v u))) ⟶ F.functorHom G)
(X : C)
:
(natTransEquiv f).app X = (f.app X PUnit.unit).app X (CategoryStruct.id (Opposite.unop (Opposite.op X)))
@[simp]
theorem
CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(F G : Functor C D)
(f : F ⟶ G)
{X : C}
{a : (MonoidalCategoryStruct.tensorUnit (Functor C (Type (max v' v u)))).obj X}
(Y : C)
{φ : X ⟶ Y}
:
@[simp]
theorem
CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(K L : Functor C D)
(X : C)
(f : K ⟶ K)
(x :
MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (Type (max (max u v) v')))
((K.functorHom L).obj X))
:
(MonoidalCategoryStruct.whiskerRight (Functor.natTransEquiv.symm f) (K.functorHom L)).app X x = (Functor.HomObj.ofNatTrans f, x.2)
@[simp]
theorem
CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(K L : Functor C D)
(X : C)
(f : L ⟶ L)
(x :
MonoidalCategoryStruct.tensorObj ((K.functorHom L).obj X)
(MonoidalCategoryStruct.tensorUnit (Type (max (max u v) v'))))
:
(MonoidalCategoryStruct.whiskerLeft (K.functorHom L) (Functor.natTransEquiv.symm f)).app X x = (x.1, Functor.HomObj.ofNatTrans f)
@[simp]
theorem
CategoryTheory.Enriched.Functor.whiskerLeft_app_apply
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(K L M N : Functor C D)
(g : MonoidalCategoryStruct.tensorObj (L.functorHom M) (M.functorHom N) ⟶ L.functorHom N)
{X : C}
(a :
(MonoidalCategoryStruct.tensorObj (K.functorHom L)
(MonoidalCategoryStruct.tensorObj (L.functorHom M) (M.functorHom N))).obj
X)
:
@[simp]
theorem
CategoryTheory.Enriched.Functor.whiskerRight_app_apply
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(K L M N : Functor C D)
(f : MonoidalCategoryStruct.tensorObj (K.functorHom L) (L.functorHom M) ⟶ K.functorHom M)
{X : C}
(a :
(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (K.functorHom L) (L.functorHom M))
(M.functorHom N)).obj
X)
:
@[simp]
theorem
CategoryTheory.Enriched.Functor.associator_inv_apply
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(K L M N : Functor C D)
{X : C}
(x :
(MonoidalCategoryStruct.tensorObj (K.functorHom L)
(MonoidalCategoryStruct.tensorObj (L.functorHom M) (M.functorHom N))).obj
X)
:
(MonoidalCategoryStruct.associator ((K.functorHom L).obj X) ((L.functorHom M).obj X) ((M.functorHom N).obj X)).inv x = ((x.1, x.2.1), x.2.2)
@[simp]
theorem
CategoryTheory.Enriched.Functor.associator_hom_apply
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(K L M N : Functor C D)
{X : C}
(x :
(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (K.functorHom L) (L.functorHom M))
(M.functorHom N)).obj
X)
:
(MonoidalCategoryStruct.associator ((K.functorHom L).obj X) ((L.functorHom M).obj X) ((M.functorHom N).obj X)).hom x = (x.1.1, x.1.2, x.2)
noncomputable instance
CategoryTheory.Enriched.Functor.instEnrichedCategoryFunctorType
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
:
EnrichedCategory (Functor C (Type (max v' v u))) (Functor C D)
Equations
- One or more equations did not get rendered due to their size.