Enriched ordinary categories

If V is a monoidal category, a V-enriched category C does not need to be a category. However, when we have both Category C and EnrichedCategory V C, we may require that the type of morphisms X ⟶ Y in C identify to 𝟙_ V ⟶ EnrichedCategory.Hom X Y. This data shall be packaged in the typeclass EnrichedOrdinaryCategory V C.

In particular, if C is a V-enriched category, it is shown that the "underlying" category ForgetEnrichment V C is equipped with a EnrichedOrdinaryCategory V C instance.

Simplicial categories are implemented in AlgebraicTopology.SimplicialCategory.Basic using an abbreviation for EnrichedOrdinaryCategory SSet C.

class CategoryTheory.EnrichedOrdinaryCategory (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] extends CategoryTheory.EnrichedCategory V C : Type (max (max (max u u') v) v')

An enriched ordinary category is a category C that is also enriched over a category V in such a way that morphisms X ⟶ Y in C identify to morphisms 𝟙_ V ⟶ (X ⟶[V] Y) in V.

• Hom : C → C → V
• id (X : C) : MonoidalCategoryStruct.tensorUnit V ⟶ Hom X X
• comp (X Y Z : C) : MonoidalCategoryStruct.tensorObj (Hom X Y) (Hom Y Z) ⟶ Hom X Z
• id_comp (X Y : C) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (Hom X Y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (id X) (Hom X Y)) (comp X X Y)) = CategoryStruct.id (Hom X Y)
• comp_id (X Y : C) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (Hom X Y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (Hom X Y) (id Y)) (comp X Y Y)) = CategoryStruct.id (Hom X Y)
• assoc (W X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.associator (Hom W X) (Hom X Y) (Hom Y Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (comp W X Y) (Hom Y Z)) (comp W Y Z)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (Hom W X) (comp X Y Z)) (comp W X Z)
• homEquiv {X Y : C} : (X ⟶ Y) ≃ (MonoidalCategoryStruct.tensorUnit V ⟶ EnrichedCategory.Hom X Y)

  morphisms X ⟶ Y in the category identify morphisms 𝟙_ V ⟶ (X ⟶[V] Y) in V

• homEquiv_id (X : C) : homEquiv (CategoryStruct.id X) = eId V X
• homEquiv_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : homEquiv (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit V)).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (homEquiv f) (homEquiv g)) (eComp V X Y Z))

def CategoryTheory.eHomEquiv (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y : C} : (X ⟶ Y) ≃ (MonoidalCategoryStruct.tensorUnit V ⟶ EnrichedCategory.Hom X Y)

The bijection (X ⟶ Y) ≃ (𝟙_ V ⟶ (X ⟶[V] Y)) given by a EnrichedOrdinaryCategory instance.

@[simp]

theorem CategoryTheory.eHomEquiv_id (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X : C) : (eHomEquiv V) (CategoryStruct.id X) = eId V X

theorem CategoryTheory.eHomEquiv_comp (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (eHomEquiv V) (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit V)).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ((eHomEquiv V) f) ((eHomEquiv V) g)) (eComp V X Y Z))

theorem CategoryTheory.eHomEquiv_comp_assoc (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : V} (h : EnrichedCategory.Hom X Z ⟶ Z✝) : CategoryStruct.comp ((eHomEquiv V) (CategoryStruct.comp f g)) h = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit V)).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ((eHomEquiv V) f) ((eHomEquiv V) g)) (CategoryStruct.comp (eComp V X Y Z) h))

def CategoryTheory.eHomWhiskerRight (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X X' : C} (f : X ⟶ X') (Y : C) : EnrichedCategory.Hom X' Y ⟶ EnrichedCategory.Hom X Y

The morphism (X' ⟶[V] Y) ⟶ (X ⟶[V] Y) induced by a morphism X ⟶ X'.

@[simp]

theorem CategoryTheory.eHomWhiskerRight_id (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X Y : C) : eHomWhiskerRight V (CategoryStruct.id X) Y = CategoryStruct.id (EnrichedCategory.Hom X Y)

@[simp]

theorem CategoryTheory.eHomWhiskerRight_comp (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X X' X'' : C} (f : X ⟶ X') (f' : X' ⟶ X'') (Y : C) : eHomWhiskerRight V (CategoryStruct.comp f f') Y = CategoryStruct.comp (eHomWhiskerRight V f' Y) (eHomWhiskerRight V f Y)

theorem CategoryTheory.eHomWhiskerRight_comp_assoc (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X X' X'' : C} (f : X ⟶ X') (f' : X' ⟶ X'') (Y : C) {Z : V} (h : EnrichedCategory.Hom X Y ⟶ Z) : CategoryStruct.comp (eHomWhiskerRight V (CategoryStruct.comp f f') Y) h = CategoryStruct.comp (eHomWhiskerRight V f' Y) (CategoryStruct.comp (eHomWhiskerRight V f Y) h)

theorem CategoryTheory.eComp_eHomWhiskerRight (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X X' : C} (f : X ⟶ X') (Y Z : C) : CategoryStruct.comp (eComp V X' Y Z) (eHomWhiskerRight V f Z) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eHomWhiskerRight V f Y) (EnrichedCategory.Hom Y Z)) (eComp V X Y Z)

Whiskering commutes with the enriched composition.

theorem CategoryTheory.eComp_eHomWhiskerRight_assoc (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X X' : C} (f : X ⟶ X') (Y Z : C) {Z✝ : V} (h : EnrichedCategory.Hom X Z ⟶ Z✝) : CategoryStruct.comp (eComp V X' Y Z) (CategoryStruct.comp (eHomWhiskerRight V f Z) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eHomWhiskerRight V f Y) (EnrichedCategory.Hom Y Z)) (CategoryStruct.comp (eComp V X Y Z) h)

def CategoryTheory.eHomWhiskerLeft (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X : C) {Y Y' : C} (g : Y ⟶ Y') : EnrichedCategory.Hom X Y ⟶ EnrichedCategory.Hom X Y'

The morphism (X ⟶[V] Y) ⟶ (X ⟶[V] Y') induced by a morphism Y ⟶ Y'.

@[simp]

theorem CategoryTheory.eHomWhiskerLeft_id (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X Y : C) : eHomWhiskerLeft V X (CategoryStruct.id Y) = CategoryStruct.id (EnrichedCategory.Hom X Y)

@[simp]

theorem CategoryTheory.eHomWhiskerLeft_comp (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X : C) {Y Y' Y'' : C} (g : Y ⟶ Y') (g' : Y' ⟶ Y'') : eHomWhiskerLeft V X (CategoryStruct.comp g g') = CategoryStruct.comp (eHomWhiskerLeft V X g) (eHomWhiskerLeft V X g')

theorem CategoryTheory.eHomWhiskerLeft_comp_assoc (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X : C) {Y Y' Y'' : C} (g : Y ⟶ Y') (g' : Y' ⟶ Y'') {Z : V} (h : EnrichedCategory.Hom X Y'' ⟶ Z) : CategoryStruct.comp (eHomWhiskerLeft V X (CategoryStruct.comp g g')) h = CategoryStruct.comp (eHomWhiskerLeft V X g) (CategoryStruct.comp (eHomWhiskerLeft V X g') h)

theorem CategoryTheory.eComp_eHomWhiskerLeft (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X Y : C) {Z Z' : C} (g : Z ⟶ Z') : CategoryStruct.comp (eComp V X Y Z) (eHomWhiskerLeft V X g) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (EnrichedCategory.Hom X Y) (eHomWhiskerLeft V Y g)) (eComp V X Y Z')

Whiskering commutes with the enriched composition.

theorem CategoryTheory.eComp_eHomWhiskerLeft_assoc (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X Y : C) {Z Z' : C} (g : Z ⟶ Z') {Z✝ : V} (h : EnrichedCategory.Hom X Z' ⟶ Z✝) : CategoryStruct.comp (eComp V X Y Z) (CategoryStruct.comp (eHomWhiskerLeft V X g) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (EnrichedCategory.Hom X Y) (eHomWhiskerLeft V Y g)) (CategoryStruct.comp (eComp V X Y Z') h)

theorem CategoryTheory.eHom_whisker_cancel (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C} (α : Y ≅ Y₁) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eHomWhiskerLeft V X α.hom) (EnrichedCategory.Hom Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (EnrichedCategory.Hom X Y₁) (eHomWhiskerRight V α.inv Z)) (eComp V X Y₁ Z)) = eComp V X Y Z

Given an isomorphism α : Y ≅ Y₁ in C, the enriched composition map eComp V X Y Z : (X ⟶[V] Y) ⊗ (Y ⟶[V] Z) ⟶ (X ⟶[V] Z) factors through the V object (X ⟶[V] Y₁) ⊗ (Y₁ ⟶[V] Z) via the map defined by whiskering in the middle with α.hom and α.inv.

theorem CategoryTheory.eHom_whisker_cancel_assoc (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C} (α : Y ≅ Y₁) {Z✝ : V} (h : EnrichedCategory.Hom X Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eHomWhiskerLeft V X α.hom) (EnrichedCategory.Hom Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (EnrichedCategory.Hom X Y₁) (eHomWhiskerRight V α.inv Z)) (CategoryStruct.comp (eComp V X Y₁ Z) h)) = CategoryStruct.comp (eComp V X Y Z) h

theorem CategoryTheory.eHom_whisker_cancel_inv (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C} (α : Y ≅ Y₁) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eHomWhiskerLeft V X α.inv) (EnrichedCategory.Hom Y₁ Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (EnrichedCategory.Hom X Y) (eHomWhiskerRight V α.hom Z)) (eComp V X Y Z)) = eComp V X Y₁ Z

theorem CategoryTheory.eHom_whisker_cancel_inv_assoc (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C} (α : Y ≅ Y₁) {Z✝ : V} (h : EnrichedCategory.Hom X Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eHomWhiskerLeft V X α.inv) (EnrichedCategory.Hom Y₁ Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (EnrichedCategory.Hom X Y) (eHomWhiskerRight V α.hom Z)) (CategoryStruct.comp (eComp V X Y Z) h)) = CategoryStruct.comp (eComp V X Y₁ Z) h

theorem CategoryTheory.eHom_whisker_exchange (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X X' Y Y' : C} (f : X ⟶ X') (g : Y ⟶ Y') : CategoryStruct.comp (eHomWhiskerLeft V X' g) (eHomWhiskerRight V f Y') = CategoryStruct.comp (eHomWhiskerRight V f Y) (eHomWhiskerLeft V X g)

theorem CategoryTheory.eHom_whisker_exchange_assoc (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X X' Y Y' : C} (f : X ⟶ X') (g : Y ⟶ Y') {Z : V} (h : EnrichedCategory.Hom X Y' ⟶ Z) : CategoryStruct.comp (eHomWhiskerLeft V X' g) (CategoryStruct.comp (eHomWhiskerRight V f Y') h) = CategoryStruct.comp (eHomWhiskerRight V f Y) (CategoryStruct.comp (eHomWhiskerLeft V X g) h)

def CategoryTheory.eHomFunctor (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] : Functor Cᵒᵖ (Functor C V)

The bifunctor Cᵒᵖ ⥤ C ⥤ V which sends X : Cᵒᵖ and Y : C to X ⟶[V] Y.

@[simp]

theorem CategoryTheory.eHomFunctor_map_app (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X✝ Y✝ : Cᵒᵖ} (φ : X✝ ⟶ Y✝) (Y : C) : ((eHomFunctor V C).map φ).app Y = eHomWhiskerRight V φ.unop Y

@[simp]

theorem CategoryTheory.eHomFunctor_obj_obj (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X : Cᵒᵖ) (Y : C) : ((eHomFunctor V C).obj X).obj Y = EnrichedCategory.Hom (Opposite.unop X) Y

@[simp]

theorem CategoryTheory.eHomFunctor_obj_map (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X : Cᵒᵖ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((eHomFunctor V C).obj X).map φ = eHomWhiskerLeft V (Opposite.unop X) φ

instance CategoryTheory.ForgetEnrichment.EnrichedOrdinaryCategory (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {D : Type u_1} [EnrichedCategory V D] : CategoryTheory.EnrichedOrdinaryCategory V (ForgetEnrichment V D)

@[reducible, inline]

abbrev CategoryTheory.eCoyoneda (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X : C) : Functor C V

enriched coyoneda functor (X ⟶[V] _) : C ⥤ V.