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.

See Mathlib.CategoryTheory.Closed.FunctorToTypes.

structure CategoryTheory.Functor.HomObj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D) (A : CategoryTheory.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).

• app : (c : C) → A.obj c → (F.obj c ⟶ G.obj c)

  The morphism F.obj c ⟶ G.obj c associated with a : A.obj c.

• naturality : ∀ {c d : C} (f : c ⟶ d) (a : A.obj c), CategoryTheory.CategoryStruct.comp (F.map f) (self.app d (A.map f a)) = CategoryTheory.CategoryStruct.comp (self.app c a) (G.map f)

theorem CategoryTheory.Functor.HomObj.ext {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {D : Type u'} {inst_1 : CategoryTheory.Category.{v', u'} D} {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} {x y : F.HomObj G A}, x.app = y.app → x = y

@[simp]

theorem CategoryTheory.Functor.HomObj.naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} (self : F.HomObj G A) {c : C} {d : C} (f : c ⟶ d) (a : A.obj c) : CategoryTheory.CategoryStruct.comp (F.map f) (self.app d (A.map f a)) = CategoryTheory.CategoryStruct.comp (self.app c a) (G.map f)

def CategoryTheory.Functor.homObjEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (A : CategoryTheory.Functor C (Type w)) : F.HomObj G A ≃ (CategoryTheory.MonoidalCategory.tensorObj F A ⟶ G)

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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (A : CategoryTheory.Functor C (Type w)) (a : F.HomObj G A) (X : C) : ∀ (x : (CategoryTheory.MonoidalCategory.tensorObj F A).obj X), ((F.homObjEquiv G A) a).app X x = match x with | (x, y) => a.app X y x

@[simp]

theorem CategoryTheory.Functor.homObjEquiv_symm_apply_app {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (A : CategoryTheory.Functor C (Type w)) (a : CategoryTheory.MonoidalCategory.tensorObj F A ⟶ G) (X : C) (y : A.obj X) (x : F.obj X) : ((F.homObjEquiv G A).symm a).app X y x = a.app X (x, y)

@[simp]

theorem CategoryTheory.Functor.HomObj.naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} (self : F.HomObj G A) {c : C} {d : C} (f : c ⟶ d) (a : A.obj c) {Z : D} (h : G.obj d ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (self.app d (A.map f a)) h) = CategoryTheory.CategoryStruct.comp (self.app c a) (CategoryTheory.CategoryStruct.comp (G.map f) h)

theorem CategoryTheory.Functor.HomObj.congr_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} {f : F.HomObj G A} {g : F.HomObj G A} (h : f = g) (X : C) (a : A.obj X) : f.app X a = g.app X a

def CategoryTheory.Functor.HomObj.ofNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {A : CategoryTheory.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.

Equations

• CategoryTheory.Functor.HomObj.ofNatTrans f = { app := fun (X : C) (x : A.obj X) => f.app X, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.HomObj.ofNatTrans_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} (f : F ⟶ G) (X : C) : ∀ (x : A.obj X), (CategoryTheory.Functor.HomObj.ofNatTrans f).app X x = f.app X

def CategoryTheory.Functor.HomObj.id {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} (A : CategoryTheory.Functor C (Type w)) : F.HomObj F A

The identity HomObj F F A.

Equations

• CategoryTheory.Functor.HomObj.id A = CategoryTheory.Functor.HomObj.ofNatTrans (CategoryTheory.CategoryStruct.id F)

@[simp]

theorem CategoryTheory.Functor.HomObj.id_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} (A : CategoryTheory.Functor C (Type w)) (X : C) : ∀ (x : A.obj X), (CategoryTheory.Functor.HomObj.id A).app X x = CategoryTheory.CategoryStruct.id (F.obj X)

def CategoryTheory.Functor.HomObj.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} {M : CategoryTheory.Functor C D} (f : F.HomObj G A) (g : G.HomObj M A) : F.HomObj M A

Composition of f : HomObj F G A with g : HomObj G M A.

Equations

• f.comp g = { app := fun (X : C) (a : A.obj X) => CategoryTheory.CategoryStruct.comp (f.app X a) (g.app X a), naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.HomObj.comp_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} {M : CategoryTheory.Functor C D} (f : F.HomObj G A) (g : G.HomObj M A) (X : C) (a : A.obj X) : (f.comp g).app X a = CategoryTheory.CategoryStruct.comp (f.app X a) (g.app X a)

def CategoryTheory.Functor.HomObj.map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} {A' : CategoryTheory.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'.

Equations

• CategoryTheory.Functor.HomObj.map f x = { app := fun (Δ : C) (a : A'.obj Δ) => x.app Δ (f.app Δ a), naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.HomObj.map_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} {A' : CategoryTheory.Functor C (Type w)} (f : A' ⟶ A) (x : F.HomObj G A) (Δ : C) (a : A'.obj Δ) : (CategoryTheory.Functor.HomObj.map f x).app Δ a = x.app Δ (f.app Δ a)

def CategoryTheory.Functor.homObjFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.Functor C (Type w))ᵒᵖ (Type (max w v' u))

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_map_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D) {A : (CategoryTheory.Functor C (Type w))ᵒᵖ} {A' : (CategoryTheory.Functor C (Type w))ᵒᵖ} (f : A ⟶ A') (x : F.HomObj G (Opposite.unop A)) (X : C) (a : (Opposite.unop A').obj X) : ((F.homObjFunctor G).map f x).app X a = x.app X (f.unop.app X a)

@[simp]

theorem CategoryTheory.Functor.homObjFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D) (A : (CategoryTheory.Functor C (Type w))ᵒᵖ) : (F.homObjFunctor G).obj A = F.HomObj G (Opposite.unop A)

def CategoryTheory.Functor.functorHom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D) : CategoryTheory.Functor C (Type (max v' v u))

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.

Equations

• F.functorHom G = CategoryTheory.coyoneda.rightOp.comp (F.homObjFunctor G)

theorem CategoryTheory.Functor.functorHom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {X : C} {x : (F.functorHom G).obj X} {y : (F.functorHom G).obj X} (h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f) : x = y

def CategoryTheory.Functor.functorHomEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D) (A : CategoryTheory.Functor C (Type (max u v v'))) : (A ⟶ F.functorHom G) ≃ F.HomObj G A

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_apply_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D) (A : CategoryTheory.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 (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op X)))

@[simp]

theorem CategoryTheory.Functor.functorHomEquiv_symm_apply_app_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D) (A : CategoryTheory.Functor C (Type (max u v v'))) (x : F.HomObj G A) (X : C) (a : A.obj X) (Y : C) (f : (Opposite.unop (CategoryTheory.coyoneda.rightOp.obj X)).obj Y) : (((F.functorHomEquiv G A).symm x).app X a).app Y f = x.app Y (A.map f a)

def CategoryTheory.Functor.natTransEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} : (𝟙_ (CategoryTheory.Functor C (Type (max v' v u))) ⟶ F.functorHom G) ≃ (F ⟶ G)

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_apply_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (f : 𝟙_ (CategoryTheory.Functor C (Type (max v' v u))) ⟶ F.functorHom G) (X : C) : (CategoryTheory.Functor.natTransEquiv f).app X = (f.app X PUnit.unit).app X (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op X)))

@[simp]

theorem CategoryTheory.Functor.natTransEquiv_symm_apply_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (f : F ⟶ G) : ∀ (x : C) (x_1 : (𝟙_ (CategoryTheory.Functor C (Type (max v' v u)))).obj x), (CategoryTheory.Functor.natTransEquiv.symm f).app x x_1 = CategoryTheory.Functor.HomObj.ofNatTrans f

@[simp]

theorem CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D) (f : F ⟶ G) {X : C} {a : (𝟙_ (CategoryTheory.Functor C (Type (max v' v u)))).obj X} (Y : C) {φ : X ⟶ Y} : ((CategoryTheory.Functor.natTransEquiv.symm f).app X a).app Y φ = f.app Y

@[simp]

theorem CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (K : CategoryTheory.Functor C D) (L : CategoryTheory.Functor C D) (X : C) (f : K ⟶ K) (x : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ (Type (max (max u v) v'))) ((K.functorHom L).obj X)) : (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Functor.natTransEquiv.symm f) (K.functorHom L)).app X x = (CategoryTheory.Functor.HomObj.ofNatTrans f, x.2)

@[simp]

theorem CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (K : CategoryTheory.Functor C D) (L : CategoryTheory.Functor C D) (X : C) (f : L ⟶ L) (x : CategoryTheory.MonoidalCategory.tensorObj ((K.functorHom L).obj X) (𝟙_ (Type (max (max u v) v')))) : (CategoryTheory.MonoidalCategory.whiskerLeft (K.functorHom L) (CategoryTheory.Functor.natTransEquiv.symm f)).app X x = (x.1, CategoryTheory.Functor.HomObj.ofNatTrans f)

@[simp]

theorem CategoryTheory.Enriched.Functor.whiskerLeft_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (K : CategoryTheory.Functor C D) (L : CategoryTheory.Functor C D) (M : CategoryTheory.Functor C D) (N : CategoryTheory.Functor C D) (g : CategoryTheory.MonoidalCategory.tensorObj (L.functorHom M) (M.functorHom N) ⟶ L.functorHom N) {X : C} (a : (CategoryTheory.MonoidalCategory.tensorObj (K.functorHom L) (CategoryTheory.MonoidalCategory.tensorObj (L.functorHom M) (M.functorHom N))).obj X) : (CategoryTheory.MonoidalCategory.whiskerLeft (K.functorHom L) g).app X a = (a.1, g.app X a.2)

@[simp]

theorem CategoryTheory.Enriched.Functor.whiskerRight_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (K : CategoryTheory.Functor C D) (L : CategoryTheory.Functor C D) (M : CategoryTheory.Functor C D) (N : CategoryTheory.Functor C D) (f : CategoryTheory.MonoidalCategory.tensorObj (K.functorHom L) (L.functorHom M) ⟶ K.functorHom M) {X : C} (a : (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj (K.functorHom L) (L.functorHom M)) (M.functorHom N)).obj X) : (CategoryTheory.MonoidalCategory.whiskerRight f (M.functorHom N)).app X a = (f.app X a.1, a.2)

@[simp]

theorem CategoryTheory.Enriched.Functor.associator_inv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (K : CategoryTheory.Functor C D) (L : CategoryTheory.Functor C D) (M : CategoryTheory.Functor C D) (N : CategoryTheory.Functor C D) {X : C} (x : (CategoryTheory.MonoidalCategory.tensorObj (K.functorHom L) (CategoryTheory.MonoidalCategory.tensorObj (L.functorHom M) (M.functorHom N))).obj X) : (CategoryTheory.MonoidalCategory.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (K : CategoryTheory.Functor C D) (L : CategoryTheory.Functor C D) (M : CategoryTheory.Functor C D) (N : CategoryTheory.Functor C D) {X : C} (x : (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj (K.functorHom L) (L.functorHom M)) (M.functorHom N)).obj X) : (CategoryTheory.MonoidalCategory.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] : CategoryTheory.EnrichedCategory (CategoryTheory.Functor C (Type (max v' v u))) (CategoryTheory.Functor C D)

Equations

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