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.lean.

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).

• app (c : C) (a : 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) : 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) : x = y

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} : x = y ↔ x.app = y.app

def CategoryTheory.Functor.homObjEquiv {C : Type u} [Category.{v, u} C] (F G A : Functor C (Type w)) : F.HomObj G A ≃ (MonoidalCategoryStruct.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} [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) : ((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} [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) : ((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} [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) : f.app X a = g.app X a

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.

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} [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) : (ofNatTrans f).app X x✝ = f.app 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.

Equations

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

@[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) : (id A).app X x✝ = CategoryStruct.id (F.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

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} [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) : (f.comp g).app X a = CategoryStruct.comp (f.app X a) (g.app X a)

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'.

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} [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) (Δ : C) (a : A'.obj Δ) : (map f x).app Δ a = x.app Δ (f.app Δ a)

def CategoryTheory.Functor.homObjFunctor {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F G : Functor C D) : Functor (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_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))ᵒᵖ) : (F.homObjFunctor G).obj A = F.HomObj G (Opposite.unop A)

@[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) : ((F.homObjFunctor G).map f x).app X a = x.app X (f.unop.app X a)

def CategoryTheory.Functor.functorHom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F G : Functor C D) : 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.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) : x = y

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} : x = y ↔ ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f

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'))) : (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_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) : (((F.functorHomEquiv G A).symm x).app X a).app Y f = x.app Y (A.map f a)

@[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} : (MonoidalCategoryStruct.tensorUnit (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_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✝) : (natTransEquiv.symm f).app x✝ x✝¹ = HomObj.ofNatTrans f

@[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} : ((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} [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) : (MonoidalCategoryStruct.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} [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) : (MonoidalCategoryStruct.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} [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.