Functor categories are enriched

If C is a V-enriched ordinary category, then J ⥤ C is also both a V-enriched ordinary category and a J ⥤ V-enriched ordinary category, provided C has suitable limits.

We first define the V-enriched structure on J ⥤ C by saying that if F₁ and F₂ are in J ⥤ C, then enrichedHom V F₁ F₂ : V is a suitable limit involving F₁.obj j ⟶[V] F₂.obj j for all j : C. The J ⥤ V object of morphisms functorEnrichedHom V F₁ F₂ : J ⥤ V is defined by sending j : J to the previously defined enrichedHom for the "restriction" of F₁ and F₂ to the category Under j. The definition isLimitConeFunctorEnrichedHom shows that enriched V F₁ F₂ is the limit of the functor functorEnrichedHom V F₁ F₂.

def CategoryTheory.Enriched.FunctorCategory.diagram (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) : Functor Jᵒᵖ (Functor J V)

Given two functors F₁ and F₂ from a category J to a V-enriched ordinary category C, this is the diagram Jᵒᵖ ⥤ J ⥤ V whose end shall be the V-morphisms in J ⥤ V from F₁ to F₂.

Equations

• CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂ = F₁.op.comp ((CategoryTheory.eHomFunctor V C).comp ((CategoryTheory.whiskeringLeft J C V).obj F₂))

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.diagram_map_app (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) {X✝ Y✝ : Jᵒᵖ} (f : X✝ ⟶ Y✝) (X : J) : ((diagram V F₁ F₂).map f).app X = eHomWhiskerRight V (F₁.map f.unop) (F₂.obj X)

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.diagram_obj_obj (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) (X : Jᵒᵖ) (X✝ : J) : ((diagram V F₁ F₂).obj X).obj X✝ = EnrichedCategory.Hom (F₁.obj (Opposite.unop X)) (F₂.obj X✝)

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.diagram_obj_map (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) (X : Jᵒᵖ) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : ((diagram V F₁ F₂).obj X).map f = eHomWhiskerLeft V (F₁.obj (Opposite.unop X)) (F₂.map f)

@[reducible, inline]

abbrev CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) : Prop

The condition that the end diagram V F₁ F₂ exists, see enrichedHom.

Equations

• CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂ = CategoryTheory.Limits.HasEnd (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Enriched.FunctorCategory.enrichedHom (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasEnrichedHom V F₁ F₂] : V

The V-enriched hom from F₁ to F₂ when F₁ and F₂ are functors J ⥤ C and C is a V-enriched category.

Equations

• CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂ = CategoryTheory.Limits.end_ (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Enriched.FunctorCategory.enrichedHomπ (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasEnrichedHom V F₁ F₂] (j : J) : enrichedHom V F₁ F₂ ⟶ EnrichedCategory.Hom (F₁.obj j) (F₂.obj j)

The projection enrichedHom V F₁ F₂ ⟶ F₁.obj j ⟶[V] F₂.obj j in the category V for any j : J when F₁ and F₂ are functors J ⥤ C and C is a V-enriched category.

Equations

• CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ j = CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂) j

theorem CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasEnrichedHom V F₁ F₂] {i j : J} (f : i ⟶ j) : CategoryStruct.comp (enrichedHomπ V F₁ F₂ i) (eHomWhiskerLeft V (F₁.obj i) (F₂.map f)) = CategoryStruct.comp (enrichedHomπ V F₁ F₂ j) (eHomWhiskerRight V (F₁.map f) (F₂.obj j))

theorem CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasEnrichedHom V F₁ F₂] {i j : J} (f : i ⟶ j) {Z : V} (h : EnrichedCategory.Hom (F₁.obj i) (F₂.obj j) ⟶ Z) : CategoryStruct.comp (enrichedHomπ V F₁ F₂ i) (CategoryStruct.comp (eHomWhiskerLeft V (F₁.obj i) (F₂.map f)) h) = CategoryStruct.comp (enrichedHomπ V F₁ F₂ j) (CategoryStruct.comp (eHomWhiskerRight V (F₁.map f) (F₂.obj j)) h)

theorem CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition' (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasEnrichedHom V F₁ F₂] {i j : J} (f : i ⟶ j) : CategoryStruct.comp (enrichedHomπ V F₁ F₂ i) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (EnrichedCategory.Hom (F₁.obj i) (F₂.obj i))).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (EnrichedCategory.Hom (F₁.obj i) (F₂.obj i)) ((eHomEquiv V) (F₂.map f))) (eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)))) = CategoryStruct.comp (enrichedHomπ V F₁ F₂ j) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (EnrichedCategory.Hom (F₁.obj j) (F₂.obj j))).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ((eHomEquiv V) (F₁.map f)) (EnrichedCategory.Hom (F₁.obj j) (F₂.obj j))) (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j))))

theorem CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition'_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasEnrichedHom V F₁ F₂] {i j : J} (f : i ⟶ j) {Z : V} (h : EnrichedCategory.Hom (F₁.obj i) (F₂.obj j) ⟶ Z) : CategoryStruct.comp (enrichedHomπ V F₁ F₂ i) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (EnrichedCategory.Hom (F₁.obj i) (F₂.obj i))).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (EnrichedCategory.Hom (F₁.obj i) (F₂.obj i)) ((eHomEquiv V) (F₂.map f))) (CategoryStruct.comp (eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)) h))) = CategoryStruct.comp (enrichedHomπ V F₁ F₂ j) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (EnrichedCategory.Hom (F₁.obj j) (F₂.obj j))).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ((eHomEquiv V) (F₁.map f)) (EnrichedCategory.Hom (F₁.obj j) (F₂.obj j))) (CategoryStruct.comp (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)) h)))

noncomputable def CategoryTheory.Enriched.FunctorCategory.homEquiv (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] {F₁ F₂ : Functor J C} [HasEnrichedHom V F₁ F₂] : (F₁ ⟶ F₂) ≃ (𝟙_ V ⟶ enrichedHom V F₁ F₂)

Given functors F₁ and F₂ in J ⥤ C, where C is a V-enriched ordinary category, this is the bijection (F₁ ⟶ F₂) ≃ (𝟙_ V ⟶ enrichedHom V F₁ F₂).

Equations

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

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.homEquiv_apply_π (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] {F₁ F₂ : Functor J C} [HasEnrichedHom V F₁ F₂] (τ : F₁ ⟶ F₂) (j : J) : CategoryStruct.comp ((homEquiv V) τ) (enrichedHomπ V F₁ F₂ j) = (eHomEquiv V) (τ.app j)

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.homEquiv_apply_π_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] {F₁ F₂ : Functor J C} [HasEnrichedHom V F₁ F₂] (τ : F₁ ⟶ F₂) (j : J) {Z : V} (h : EnrichedCategory.Hom (F₁.obj j) (F₂.obj j) ⟶ Z) : CategoryStruct.comp ((homEquiv V) τ) (CategoryStruct.comp (enrichedHomπ V F₁ F₂ j) h) = CategoryStruct.comp ((eHomEquiv V) (τ.app j)) h

noncomputable def CategoryTheory.Enriched.FunctorCategory.enrichedId (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ : Functor J C) [HasEnrichedHom V F₁ F₁] : 𝟙_ V ⟶ enrichedHom V F₁ F₁

The identity for the V-enrichment of the category J ⥤ C.

Equations

• CategoryTheory.Enriched.FunctorCategory.enrichedId V F₁ = (CategoryTheory.Enriched.FunctorCategory.homEquiv V) (CategoryTheory.CategoryStruct.id F₁)

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.enrichedId_π (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ : Functor J C) [HasEnrichedHom V F₁ F₁] (j : J) : CategoryStruct.comp (enrichedId V F₁) (Limits.end_.π (diagram V F₁ F₁) j) = eId V (F₁.obj j)

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.enrichedId_π_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ : Functor J C) [HasEnrichedHom V F₁ F₁] (j : J) {Z : V} (h : ((diagram V F₁ F₁).obj (Opposite.op j)).obj j ⟶ Z) : CategoryStruct.comp (enrichedId V F₁) (CategoryStruct.comp (Limits.end_.π (diagram V F₁ F₁) j) h) = CategoryStruct.comp (eId V (F₁.obj j)) h

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.homEquiv_id (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ : Functor J C) [HasEnrichedHom V F₁ F₁] : (homEquiv V) (CategoryStruct.id F₁) = enrichedId V F₁

noncomputable def CategoryTheory.Enriched.FunctorCategory.enrichedComp (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : Functor J C) [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V F₂ F₃] [HasEnrichedHom V F₁ F₃] : MonoidalCategoryStruct.tensorObj (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) ⟶ enrichedHom V F₁ F₃

The composition for the V-enrichment of the category J ⥤ C.

Equations

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

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.enrichedComp_π (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : Functor J C) [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V F₂ F₃] [HasEnrichedHom V F₁ F₃] (j : J) : CategoryStruct.comp (enrichedComp V F₁ F₂ F₃) (Limits.end_.π (diagram V F₁ F₃) j) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (Limits.end_.π (diagram V F₁ F₂) j) (Limits.end_.π (diagram V F₂ F₃) j)) (eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j))

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.enrichedComp_π_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : Functor J C) [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V F₂ F₃] [HasEnrichedHom V F₁ F₃] (j : J) {Z : V} (h : ((diagram V F₁ F₃).obj (Opposite.op j)).obj j ⟶ Z) : CategoryStruct.comp (enrichedComp V F₁ F₂ F₃) (CategoryStruct.comp (Limits.end_.π (diagram V F₁ F₃) j) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (Limits.end_.π (diagram V F₁ F₂) j) (Limits.end_.π (diagram V F₂ F₃) j)) (CategoryStruct.comp (eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j)) h)

theorem CategoryTheory.Enriched.FunctorCategory.homEquiv_comp (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] {F₁ F₂ F₃ : Functor J C} [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V F₂ F₃] [HasEnrichedHom V F₁ F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) : (homEquiv V) (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (𝟙_ V)).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ((homEquiv V) f) ((homEquiv V) g)) (enrichedComp V F₁ F₂ F₃))

theorem CategoryTheory.Enriched.FunctorCategory.homEquiv_comp_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] {F₁ F₂ F₃ : Functor J C} [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V F₂ F₃] [HasEnrichedHom V F₁ F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) {Z : V} (h : enrichedHom V F₁ F₃ ⟶ Z) : CategoryStruct.comp ((homEquiv V) (CategoryStruct.comp f g)) h = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (𝟙_ V)).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ((homEquiv V) f) ((homEquiv V) g)) (CategoryStruct.comp (enrichedComp V F₁ F₂ F₃) h))

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.enriched_id_comp (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasEnrichedHom V F₁ F₁] [HasEnrichedHom V F₁ F₂] : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (enrichedHom V F₁ F₂)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (enrichedId V F₁) (enrichedHom V F₁ F₂)) (enrichedComp V F₁ F₁ F₂)) = CategoryStruct.id (enrichedHom V F₁ F₂)

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.enriched_id_comp_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasEnrichedHom V F₁ F₁] [HasEnrichedHom V F₁ F₂] {Z : V} (h : enrichedHom V F₁ F₂ ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (enrichedHom V F₁ F₂)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (enrichedId V F₁) (enrichedHom V F₁ F₂)) (CategoryStruct.comp (enrichedComp V F₁ F₁ F₂) h)) = h

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.enriched_comp_id (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V F₂ F₂] : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (enrichedHom V F₁ F₂)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (enrichedHom V F₁ F₂) (enrichedId V F₂)) (enrichedComp V F₁ F₂ F₂)) = CategoryStruct.id (enrichedHom V F₁ F₂)

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.enriched_comp_id_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V F₂ F₂] {Z : V} (h : enrichedHom V F₁ F₂ ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (enrichedHom V F₁ F₂)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (enrichedHom V F₁ F₂) (enrichedId V F₂)) (CategoryStruct.comp (enrichedComp V F₁ F₂ F₂) h)) = h

theorem CategoryTheory.Enriched.FunctorCategory.enriched_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ F₄ : Functor J C) [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₃] [HasEnrichedHom V F₁ F₄] [HasEnrichedHom V F₂ F₃] [HasEnrichedHom V F₂ F₄] [HasEnrichedHom V F₃ F₄] : CategoryStruct.comp (MonoidalCategoryStruct.associator (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (enrichedComp V F₁ F₂ F₃) (enrichedHom V F₃ F₄)) (enrichedComp V F₁ F₃ F₄)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (enrichedHom V F₁ F₂) (enrichedComp V F₂ F₃ F₄)) (enrichedComp V F₁ F₂ F₄)

theorem CategoryTheory.Enriched.FunctorCategory.enriched_assoc_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ F₄ : Functor J C) [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₃] [HasEnrichedHom V F₁ F₄] [HasEnrichedHom V F₂ F₃] [HasEnrichedHom V F₂ F₄] [HasEnrichedHom V F₃ F₄] {Z : V} (h : enrichedHom V F₁ F₄ ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (enrichedComp V F₁ F₂ F₃) (enrichedHom V F₃ F₄)) (CategoryStruct.comp (enrichedComp V F₁ F₃ F₄) h)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (enrichedHom V F₁ F₂) (enrichedComp V F₂ F₃ F₄)) (CategoryStruct.comp (enrichedComp V F₁ F₂ F₄) h)

noncomputable def CategoryTheory.Enriched.FunctorCategory.enrichedOrdinaryCategory (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] (C : Type u₂) [Category.{v₂, u₂} C] (J : Type u₃) [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] [∀ (F₁ F₂ : Functor J C), HasEnrichedHom V F₁ F₂] : EnrichedOrdinaryCategory V (Functor J C)

If C is a V-enriched ordinary category, and C has suitable limits, then J ⥤ C is also a V-enriched ordinary category.

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom' (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] {K : Type u₄} [Category.{v₄, u₄} K] [EnrichedOrdinaryCategory V C] {F₁ F₂ : Functor J C} (G : Functor K J) [HasEnrichedHom V F₁ F₂] {F₁' F₂' : Functor K C} [HasEnrichedHom V F₁' F₂'] (e₁ : G.comp F₁ ≅ F₁') (e₂ : G.comp F₂ ≅ F₂') : enrichedHom V F₁ F₂ ⟶ enrichedHom V F₁' F₂'

If F₁ and F₂ are functors J ⥤ C, G : K ⥤ J, and F₁' and F₂' are functors K ⥤ C that are respectively isomorphic to G ⋙ F₁ and G ⋙ F₂, then this is the induced morphism enrichedHom V F₁ F₂ ⟶ enrichedHom V F₁' F₂' in V when C is a category enriched in V.

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] {K : Type u₄} [Category.{v₄, u₄} K] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) (G : Functor K J) [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V (G.comp F₁) (G.comp F₂)] : enrichedHom V F₁ F₂ ⟶ enrichedHom V (G.comp F₁) (G.comp F₂)

If F₁ and F₂ are functors J ⥤ C, and G : K ⥤ J, then this is the induced morphism enrichedHom V F₁ F₂ ⟶ enrichedHom V (G ⋙ F₁) (G ⋙ F₂) in V when C is a category enriched in V.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) : Prop

Given functors F₁ and F₂ in J ⥤ C, where C is a category enriched in V, this condition allows the definition of functorEnrichedHom V F₁ F₂ : J ⥤ V.

Equations

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

instance CategoryTheory.Enriched.FunctorCategory.instHasEnrichedHomUnderCompMapForget (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] {j j' : J} (f : j ⟶ j') : HasEnrichedHom V ((Under.map f).comp ((Under.forget j).comp F₁)) ((Under.map f).comp ((Under.forget j).comp F₂))

noncomputable def CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] : Functor J V

Given functors F₁ and F₂ in J ⥤ C, where C is a category enriched in V, this is the enriched hom functor from F₁ to F₂ in J ⥤ V.

Equations

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

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom_map (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : (functorEnrichedHom V F₁ F₂).map f = precompEnrichedHom' V (Under.map f) (Iso.refl ((Under.map f).comp ((Under.forget X✝).comp F₁))) (Iso.refl ((Under.map f).comp ((Under.forget X✝).comp F₂)))

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom_obj (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] (j : J) : (functorEnrichedHom V F₁ F₂).obj j = enrichedHom V ((Under.forget j).comp F₁) ((Under.forget j).comp F₂)

noncomputable def CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂] : Limits.Cone (functorEnrichedHom V F₁ F₂)

The (limit) cone expressing that the limit of functorEnrichedHom V F₁ F₂ is enrichedHom V F₁ F₂.

Equations

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

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom_π_app (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂] (j : J) : (coneFunctorEnrichedHom V F₁ F₂).π.app j = precompEnrichedHom V F₁ F₂ (Under.forget j)

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom_pt (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂] : (coneFunctorEnrichedHom V F₁ F₂).pt = enrichedHom V F₁ F₂

noncomputable def CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.lift {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] {F₁ F₂ : Functor J C} [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂] (s : Limits.Cone (functorEnrichedHom V F₁ F₂)) : s.pt ⟶ enrichedHom V F₁ F₂

Auxiliary definition for Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.

Equations

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

theorem CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.fac {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] {F₁ F₂ : Functor J C} [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂] (s : Limits.Cone (functorEnrichedHom V F₁ F₂)) (j : J) : CategoryStruct.comp (lift s) ((coneFunctorEnrichedHom V F₁ F₂).π.app j) = s.π.app j

noncomputable def CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂] : Limits.IsLimit (coneFunctorEnrichedHom V F₁ F₂)

The limit of functorEnrichedHom V F₁ F₂ is enrichedHom V F₁ F₂.

Equations

• CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom V F₁ F₂ = { lift := CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.lift, fac := ⋯, uniq := ⋯ }

noncomputable def CategoryTheory.Enriched.FunctorCategory.functorEnrichedId (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ : Functor J C) [HasFunctorEnrichedHom V F₁ F₁] : 𝟙_ (Functor J V) ⟶ functorEnrichedHom V F₁ F₁

The identity for the J ⥤ V-enrichment of the category J ⥤ C.

Equations

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

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.functorEnrichedId_app (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ : Functor J C) [HasFunctorEnrichedHom V F₁ F₁] (j : J) : (functorEnrichedId V F₁).app j = enrichedId V ((Under.forget j).comp F₁)

noncomputable def CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₂ F₃] [HasFunctorEnrichedHom V F₁ F₃] : MonoidalCategoryStruct.tensorObj (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) ⟶ functorEnrichedHom V F₁ F₃

The composition for the J ⥤ V-enrichment of the category J ⥤ C.

Equations

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

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp_app (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₂ F₃] [HasFunctorEnrichedHom V F₁ F₃] (j : J) : (functorEnrichedComp V F₁ F₂ F₃).app j = enrichedComp V ((Under.forget j).comp F₁) ((Under.forget j).comp F₂) ((Under.forget j).comp F₃)

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.functorEnriched_id_comp (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₁ F₁] : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (functorEnrichedHom V F₁ F₂)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (functorEnrichedId V F₁) (functorEnrichedHom V F₁ F₂)) (functorEnrichedComp V F₁ F₁ F₂)) = CategoryStruct.id (functorEnrichedHom V F₁ F₂)

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.functorEnriched_id_comp_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₁ F₁] {Z : Functor J V} (h : functorEnrichedHom V F₁ F₂ ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (functorEnrichedHom V F₁ F₂)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (functorEnrichedId V F₁) (functorEnrichedHom V F₁ F₂)) (CategoryStruct.comp (functorEnrichedComp V F₁ F₁ F₂) h)) = h

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.functorEnriched_comp_id (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₂ F₂] : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (functorEnrichedHom V F₁ F₂)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (functorEnrichedHom V F₁ F₂) (functorEnrichedId V F₂)) (functorEnrichedComp V F₁ F₂ F₂)) = CategoryStruct.id (functorEnrichedHom V F₁ F₂)

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.functorEnriched_comp_id_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₂ F₂] {Z : Functor J V} (h : functorEnrichedHom V F₁ F₂ ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (functorEnrichedHom V F₁ F₂)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (functorEnrichedHom V F₁ F₂) (functorEnrichedId V F₂)) (CategoryStruct.comp (functorEnrichedComp V F₁ F₂ F₂) h)) = h

theorem CategoryTheory.Enriched.FunctorCategory.functorEnriched_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ F₄ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₂ F₃] [HasFunctorEnrichedHom V F₃ F₄] [HasFunctorEnrichedHom V F₁ F₃] [HasFunctorEnrichedHom V F₂ F₄] [HasFunctorEnrichedHom V F₁ F₄] : CategoryStruct.comp (MonoidalCategoryStruct.associator (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (functorEnrichedComp V F₁ F₂ F₃) (functorEnrichedHom V F₃ F₄)) (functorEnrichedComp V F₁ F₃ F₄)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (functorEnrichedHom V F₁ F₂) (functorEnrichedComp V F₂ F₃ F₄)) (functorEnrichedComp V F₁ F₂ F₄)

theorem CategoryTheory.Enriched.FunctorCategory.functorEnriched_assoc_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ F₄ : Functor J C) [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₂ F₃] [HasFunctorEnrichedHom V F₃ F₄] [HasFunctorEnrichedHom V F₁ F₃] [HasFunctorEnrichedHom V F₂ F₄] [HasFunctorEnrichedHom V F₁ F₄] {Z : Functor J V} (h : functorEnrichedHom V F₁ F₄ ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (functorEnrichedComp V F₁ F₂ F₃) (functorEnrichedHom V F₃ F₄)) (CategoryStruct.comp (functorEnrichedComp V F₁ F₃ F₄) h)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (functorEnrichedHom V F₁ F₂) (functorEnrichedComp V F₂ F₃ F₄)) (CategoryStruct.comp (functorEnrichedComp V F₁ F₂ F₄) h)

noncomputable def CategoryTheory.Enriched.FunctorCategory.functorEnrichedCategory (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] (C : Type u₂) [Category.{v₂, u₂} C] (J : Type u₃) [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] [∀ (F₁ F₂ : Functor J C), HasFunctorEnrichedHom V F₁ F₂] : EnrichedCategory (Functor J V) (Functor J C)

If C is a V-enriched ordinary category, and C has suitable limits, then J ⥤ C is also a J ⥤ V-enriched ordinary category.

Equations

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

noncomputable def CategoryTheory.Enriched.FunctorCategory.functorHomEquiv (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] {F₁ F₂ : Functor J C} [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂] : (F₁ ⟶ F₂) ≃ (𝟙_ (Functor J V) ⟶ functorEnrichedHom V F₁ F₂)

Given functors F₁ and F₂ in J ⥤ C, where C is a V-enriched ordinary category, this is the bijection (F₁ ⟶ F₂) ≃ (𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₂).

Equations

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

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_apply_app (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] {F₁ F₂ : Functor J C} [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂] (a✝ : F₁ ⟶ F₂) (X : J) : ((functorHomEquiv V) a✝).app X = CategoryStruct.comp ((homEquiv V) a✝) (precompEnrichedHom V F₁ F₂ (Under.forget X))

theorem CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_id (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] (F₁ : Functor J C) [HasFunctorEnrichedHom V F₁ F₁] [HasEnrichedHom V F₁ F₁] : (functorHomEquiv V) (CategoryStruct.id F₁) = functorEnrichedId V F₁

theorem CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_comp (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] {C : Type u₂} [Category.{v₂, u₂} C] {J : Type u₃} [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] {F₁ F₂ F₃ : Functor J C} [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₂ F₃] [HasEnrichedHom V F₂ F₃] [HasFunctorEnrichedHom V F₁ F₃] [HasEnrichedHom V F₁ F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) : (functorHomEquiv V) (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (𝟙_ (Functor J V))).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ((functorHomEquiv V) f) ((functorHomEquiv V) g)) (functorEnrichedComp V F₁ F₂ F₃))

noncomputable def CategoryTheory.Enriched.FunctorCategory.functorEnrichedOrdinaryCategory (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] (C : Type u₂) [Category.{v₂, u₂} C] (J : Type u₃) [Category.{v₃, u₃} J] [EnrichedOrdinaryCategory V C] [∀ (F₁ F₂ : Functor J C), HasFunctorEnrichedHom V F₁ F₂] [∀ (F₁ F₂ : Functor J C), HasEnrichedHom V F₁ F₂] : EnrichedOrdinaryCategory (Functor J V) (Functor J C)

If C is a V-enriched ordinary category, and C has suitable limits, then J ⥤ C is also a J ⥤ V-enriched ordinary category.

Equations

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