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') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] (C : Type u) [CategoryTheory.Category.{v, u} C] extends CategoryTheory.EnrichedCategory : 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) → 𝟙_ V ⟶ CategoryTheory.EnrichedCategory.Hom X X
• comp : (X Y Z : C) → CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.EnrichedCategory.Hom X Y) (CategoryTheory.EnrichedCategory.Hom Y Z) ⟶ CategoryTheory.EnrichedCategory.Hom X Z
• id_comp : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.EnrichedCategory.Hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.EnrichedCategory.id X) (CategoryTheory.EnrichedCategory.Hom X Y)) (CategoryTheory.EnrichedCategory.comp X X Y)) = CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom X Y)
• comp_id : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.EnrichedCategory.Hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom X Y) (CategoryTheory.EnrichedCategory.id Y)) (CategoryTheory.EnrichedCategory.comp X Y Y)) = CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom X Y)
• assoc : ∀ (W X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.EnrichedCategory.Hom W X) (CategoryTheory.EnrichedCategory.Hom X Y) (CategoryTheory.EnrichedCategory.Hom Y Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.EnrichedCategory.comp W X Y) (CategoryTheory.EnrichedCategory.Hom Y Z)) (CategoryTheory.EnrichedCategory.comp W Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom W X) (CategoryTheory.EnrichedCategory.comp X Y Z)) (CategoryTheory.EnrichedCategory.comp W X Z)
• homEquiv : {X Y : C} → (X ⟶ Y) ≃ (𝟙_ V ⟶ CategoryTheory.EnrichedCategory.Hom X Y)

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

• homEquiv_id : ∀ (X : C), CategoryTheory.EnrichedOrdinaryCategory.homEquiv (CategoryTheory.CategoryStruct.id X) = CategoryTheory.eId V X
• homEquiv_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.EnrichedOrdinaryCategory.homEquiv (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.EnrichedOrdinaryCategory.homEquiv f) (CategoryTheory.EnrichedOrdinaryCategory.homEquiv g)) (CategoryTheory.eComp V X Y Z))

theorem CategoryTheory.EnrichedOrdinaryCategory.homEquiv_id {V : Type u'} : ∀ {inst : CategoryTheory.Category.{v', u'} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u} {inst_2 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.EnrichedOrdinaryCategory V C] (X : C), CategoryTheory.EnrichedOrdinaryCategory.homEquiv (CategoryTheory.CategoryStruct.id X) = CategoryTheory.eId V X

theorem CategoryTheory.EnrichedOrdinaryCategory.homEquiv_comp {V : Type u'} : ∀ {inst : CategoryTheory.Category.{v', u'} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u} {inst_2 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.EnrichedOrdinaryCategory.homEquiv (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.EnrichedOrdinaryCategory.homEquiv f) (CategoryTheory.EnrichedOrdinaryCategory.homEquiv g)) (CategoryTheory.eComp V X Y Z))

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

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

Equations

• CategoryTheory.eHomEquiv V = CategoryTheory.EnrichedOrdinaryCategory.homEquiv

@[simp]

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.ForgetEnrichment.EnrichedOrdinaryCategory V = CategoryTheory.EnrichedOrdinaryCategory.mk (fun {X Y : CategoryTheory.ForgetEnrichment V D} => Equiv.refl (X ⟶ Y)) ⋯ ⋯