Documentation

Mathlib.CategoryTheory.Functor.FunctorHom

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.

theorem CategoryTheory.Functor.HomObj.ext_iff {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 = y x.app = y.app
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.appx = y

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

Instances For
    @[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)
    @[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)

    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.
    Instances For
      @[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) :
      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

      Given a natural transformation F ⟶ G, get a term of HomObj F G A by "ignoring" A.

      Equations
      Instances For
        @[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)

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

        Equations
        Instances For
          @[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)

          Given a morphism A' ⟶ A, send a term of HomObj F G A to a term of HomObj F G A'.

          Equations
          Instances For
            @[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)

            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.
            Instances For

              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)
              Instances For
                theorem CategoryTheory.Functor.functorHom_ext_iff {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} :
                x = y ∀ (Y : C) (f : X Y), x.app Y f = y.app Y f
                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
                @[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)
                @[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)))

                The equivalence (A ⟶ F.functorHom G) ≃ HomObj F G A.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[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.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)))

                  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.
                  Instances For
                    @[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)
                    Equations
                    • One or more equations did not get rendered due to their size.