Functor categories are enriched

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

def CategoryTheory.Enriched.FunctorCategory.diagram (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.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_obj_obj (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) (X : Jᵒᵖ) (X✝ : J) : ((CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂).obj X).obj X✝ = CategoryTheory.EnrichedCategory.Hom (F₁.obj (Opposite.unop X)) (F₂.obj X✝)

@[simp]

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

@[simp]

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

@[reducible, inline]

abbrev CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.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₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.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₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] (j : J) : CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂ ⟶ CategoryTheory.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₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] {i j : J} (f : i ⟶ j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.EnrichedCategory.Hom (F₁.obj i) (F₂.obj i))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom (F₁.obj i) (F₂.obj i)) ((CategoryTheory.eHomEquiv V) (F₂.map f))) (CategoryTheory.eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.EnrichedCategory.Hom (F₁.obj j) (F₂.obj j))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight ((CategoryTheory.eHomEquiv V) (F₁.map f)) (CategoryTheory.EnrichedCategory.Hom (F₁.obj j) (F₂.obj j))) (CategoryTheory.eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j))))

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₁] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedId V F₁) (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₁) j) = CategoryTheory.eId V (F₁.obj j)

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

theorem CategoryTheory.Enriched.FunctorCategory.enrichedComp_π (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃) (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₃) j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂) j) (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₂ F₃) j)) (CategoryTheory.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₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃] (j : J) {Z : V} (h : ((CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₃).obj (Opposite.op j)).obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₃) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂) j) (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₂ F₃) j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.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₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] {F₁ F₂ F₃ : CategoryTheory.Functor J C} [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) : (CategoryTheory.Enriched.FunctorCategory.homEquiv V) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ((CategoryTheory.Enriched.FunctorCategory.homEquiv V) f) ((CategoryTheory.Enriched.FunctorCategory.homEquiv V) g)) (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃))

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

noncomputable def CategoryTheory.Enriched.FunctorCategory.enrichedOrdinaryCategory (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (J : Type u₃) [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] [∀ (F₁ F₂ : CategoryTheory.Functor J C), CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] : CategoryTheory.EnrichedOrdinaryCategory V (CategoryTheory.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.