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 ⟶ X ⟶[V] X
• comp (X Y Z : C) : MonoidalCategoryStruct.tensorObj (X ⟶[V] Y) (Y ⟶[V] Z) ⟶ X ⟶[V] Z
• id_comp (X Y : C) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (X ⟶[V] Y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (id X) (X ⟶[V] Y)) (comp X X Y)) = CategoryStruct.id (X ⟶[V] Y)
• comp_id (X Y : C) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (id Y)) (comp X Y Y)) = CategoryStruct.id (X ⟶[V] Y)
• assoc (W X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (comp W X Y) (Y ⟶[V] Z)) (comp W Y Z)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (comp X Y Z)) (comp W X Z)
• homEquiv {X Y : C} : (X ⟶ Y) ≃ (MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] 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 ⟶ X ⟶[V] 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') [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 : (X ⟶[V] 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) : (X' ⟶[V] Y) ⟶ X ⟶[V] 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') [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 (X ⟶[V] 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 : (X ⟶[V] 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) (Y ⟶[V] 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 : (X ⟶[V] Z) ⟶ Z✝) : CategoryStruct.comp (eComp V X' Y Z) (CategoryStruct.comp (eHomWhiskerRight V f Z) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eHomWhiskerRight V f Y) (Y ⟶[V] 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') : (X ⟶[V] Y) ⟶ X ⟶[V] 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') [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 (X ⟶[V] 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 : (X ⟶[V] 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 (X ⟶[V] 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 : (X ⟶[V] Z') ⟶ Z✝) : CategoryStruct.comp (eComp V X Y Z) (CategoryStruct.comp (eHomWhiskerLeft V X g) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X ⟶[V] 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) (Y ⟶[V] Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X ⟶[V] 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 : (X ⟶[V] Z) ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eHomWhiskerLeft V X α.hom) (Y ⟶[V] Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X ⟶[V] 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) (Y₁ ⟶[V] Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X ⟶[V] 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 : (X ⟶[V] Z) ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eHomWhiskerLeft V X α.inv) (Y₁ ⟶[V] Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X ⟶[V] 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 : (X ⟶[V] 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.

Equations

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

@[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 = Opposite.unop X ⟶[V] 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) φ

@[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

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

Equations

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

def CategoryTheory.ForgetEnrichment.equivInverse (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (D : Type u') [Category.{v', u'} D] [EnrichedOrdinaryCategory V D] : Functor D (ForgetEnrichment V D)

If D is already an enriched ordinary category, there is a canonical functor from D to ForgetEnrichment V D.

Equations

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

@[simp]

theorem CategoryTheory.ForgetEnrichment.equivInverse_obj (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (D : Type u') [Category.{v', u'} D] [EnrichedOrdinaryCategory V D] (X : D) : (equivInverse V D).obj X = of V X

@[simp]

theorem CategoryTheory.ForgetEnrichment.equivInverse_map (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (D : Type u') [Category.{v', u'} D] [EnrichedOrdinaryCategory V D] {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (equivInverse V D).map f = homOf V ((eHomEquiv V) f)

def CategoryTheory.ForgetEnrichment.equivFunctor (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (D : Type u') [Category.{v', u'} D] [EnrichedOrdinaryCategory V D] : Functor (ForgetEnrichment V D) D

If D is already an enriched ordinary category, there is a canonical functor from ForgetEnrichment V D to D.

Equations

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

@[simp]

theorem CategoryTheory.ForgetEnrichment.equivFunctor_obj (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (D : Type u') [Category.{v', u'} D] [EnrichedOrdinaryCategory V D] (X : ForgetEnrichment V D) : (equivFunctor V D).obj X = «to» V X

@[simp]

theorem CategoryTheory.ForgetEnrichment.equivFunctor_map (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (D : Type u') [Category.{v', u'} D] [EnrichedOrdinaryCategory V D] {X✝ Y✝ : ForgetEnrichment V D} (f : X✝ ⟶ Y✝) : (equivFunctor V D).map f = (eHomEquiv V).symm (homTo V f)

def CategoryTheory.ForgetEnrichment.equiv (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {D : Type u'} [Category.{v', u'} D] [EnrichedOrdinaryCategory V D] : ForgetEnrichment V D ≌ D

If D is already an enriched ordinary category, it is equivalent to ForgetEnrichment V D.

Equations

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

@[simp]

theorem CategoryTheory.ForgetEnrichment.equiv_inverse (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {D : Type u'} [Category.{v', u'} D] [EnrichedOrdinaryCategory V D] : (equiv V).inverse = equivInverse V D

@[simp]

theorem CategoryTheory.ForgetEnrichment.equiv_unitIso (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {D : Type u'} [Category.{v', u'} D] [EnrichedOrdinaryCategory V D] : (equiv V).unitIso = NatIso.ofComponents (fun (X : ForgetEnrichment V D) => Iso.refl ((Functor.id (ForgetEnrichment V D)).obj X)) ⋯

@[simp]

theorem CategoryTheory.ForgetEnrichment.equiv_counitIso (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {D : Type u'} [Category.{v', u'} D] [EnrichedOrdinaryCategory V D] : (equiv V).counitIso = NatIso.ofComponents (fun (X : D) => Iso.refl (((equivInverse V D).comp (equivFunctor V D)).obj X)) ⋯

@[simp]

theorem CategoryTheory.ForgetEnrichment.equiv_functor (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {D : Type u'} [Category.{v', u'} D] [EnrichedOrdinaryCategory V D] : (equiv V).functor = equivFunctor 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.

Equations

• CategoryTheory.eCoyoneda V X = (CategoryTheory.eHomFunctor V C).obj (Opposite.op X)

instance CategoryTheory.instCategoryTransportEnrichment {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] : Category.{v, u} (TransportEnrichment F C)

Equations

• CategoryTheory.instCategoryTransportEnrichment C F = inferInstanceAs (CategoryTheory.Category.{?u.70, ?u.68} C)

def CategoryTheory.TransportEnrichment.ofOrdinaryEnrichedCategoryEquiv {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] : TransportEnrichment F C ≌ C

If C is an ordinary enriched category, the category structure on TransportEnrichment F C is trivially equivalent to the one on C itself.

Equations

• CategoryTheory.TransportEnrichment.ofOrdinaryEnrichedCategoryEquiv C F = CategoryTheory.Equivalence.refl

noncomputable def CategoryTheory.TransportEnrichment.enrichedOrdinaryCategory {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (h : ∀ (v : V), Function.Bijective fun (f : MonoidalCategoryStruct.tensorUnit V ⟶ v) => CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) : EnrichedOrdinaryCategory W (TransportEnrichment F C)

If for a lax monoidal functor F : V ⥤ W the canonical function (𝟙_ V ⟶ v) → (𝟙_ W ⟶ F.obj v) is bijective, and C is an enriched ordinary category on V, then F induces the structure of a W-enriched ordinary category on TransportEnrichment F C, i.e. on the same underlying category C.

Equations

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

def CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (D : Type u) [EnrichedCategory V D] (e : (v : V) → (MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) : Functor (TransportEnrichment F (ForgetEnrichment V D)) (ForgetEnrichment W (TransportEnrichment F D))

The functor that makes up TransportEnrichment.forgetEnrichmentEquiv.

Equations

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

@[simp]

theorem CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_map {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (D : Type u) [EnrichedCategory V D] (e : (v : V) → (MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) {X Y : TransportEnrichment F (ForgetEnrichment V D)} (f : X ⟶ Y) : (forgetEnrichmentEquivFunctor F D e h).map f = ForgetEnrichment.homOf W ((e (X ⟶[V] Y)) (ForgetEnrichment.homTo V f))

@[simp]

theorem CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_obj {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (D : Type u) [EnrichedCategory V D] (e : (v : V) → (MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) (X : TransportEnrichment F (ForgetEnrichment V D)) : (forgetEnrichmentEquivFunctor F D e h).obj X = ForgetEnrichment.of W X

def CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (D : Type u) [EnrichedCategory V D] (e : (v : V) → (MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) : Functor (ForgetEnrichment W (TransportEnrichment F D)) (TransportEnrichment F (ForgetEnrichment V D))

The inverse functor that makes up TransportEnrichment.forgetEnrichmentEquiv.

Equations

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

@[simp]

theorem CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_obj {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (D : Type u) [EnrichedCategory V D] (e : (v : V) → (MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) (X : ForgetEnrichment W (TransportEnrichment F D)) : (forgetEnrichmentEquivInverse F D e h).obj X = ForgetEnrichment.of V (ForgetEnrichment.to W X)

@[simp]

theorem CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_map {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (D : Type u) [EnrichedCategory V D] (e : (v : V) → (MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) {X✝ Y✝ : ForgetEnrichment W (TransportEnrichment F D)} (f : X✝ ⟶ Y✝) : (forgetEnrichmentEquivInverse F D e h).map f = ForgetEnrichment.homOf V ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f))

def CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (D : Type u) [EnrichedCategory V D] (e : (v : V) → (MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) : TransportEnrichment F (ForgetEnrichment V D) ≌ ForgetEnrichment W (TransportEnrichment F D)

If D is a V-enriched category, then forgetting the enrichment and transporting the resulting enriched ordinary category along a functor F : V ⥤ W, for which f ↦ Functor.LaxMonoidal.ε F ≫ F.map f has an inverse, results in a category equivalent to transporting along F and then forgetting about the resulting W-enrichment.

Equations

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

@[simp]

theorem CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_unitIso {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (D : Type u) [EnrichedCategory V D] (e : (v : V) → (MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) : (forgetEnrichmentEquiv F D e h).unitIso = NatIso.ofComponents (fun (x : TransportEnrichment F (ForgetEnrichment V D)) => Iso.refl ((Functor.id (TransportEnrichment F (ForgetEnrichment V D))).obj x)) ⋯

@[simp]

theorem CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_functor {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (D : Type u) [EnrichedCategory V D] (e : (v : V) → (MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) : (forgetEnrichmentEquiv F D e h).functor = forgetEnrichmentEquivFunctor F D e h

@[simp]

theorem CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_inverse {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (D : Type u) [EnrichedCategory V D] (e : (v : V) → (MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) : (forgetEnrichmentEquiv F D e h).inverse = forgetEnrichmentEquivInverse F D e h

@[simp]

theorem CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_counitIso {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {W : Type u''} [Category.{v'', u''} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (D : Type u) [EnrichedCategory V D] (e : (v : V) → (MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map f)) : (forgetEnrichmentEquiv F D e h).counitIso = NatIso.ofComponents (fun (x : ForgetEnrichment W (TransportEnrichment F D)) => Iso.refl (((forgetEnrichmentEquivInverse F D e h).comp (forgetEnrichmentEquivFunctor F D e h)).obj x)) ⋯