The bicategory of V-enriched categories

We define the bicategory EnrichedCat V of (bundled) V-enriched categories for a fixed monoidal category V.

Future work

• Define change of base and ForgetEnrichment as 2-functors.
• Define the bicategory of enriched ordinary categories.

def CategoryTheory.EnrichedCat (V : Type v) [Category.{w, v} V] [MonoidalCategory V] : Type (max (u + 1) (max u v) w)

Category of V-enriched categories for a monoidal category V.

@[implicit_reducible]

instance CategoryTheory.EnrichedCat.instCoeSortType (V : Type v) [Category.{w, v} V] [MonoidalCategory V] : CoeSort (EnrichedCat V) (Type u)

@[implicit_reducible]

instance CategoryTheory.EnrichedCat.str (V : Type v) [Category.{w, v} V] [MonoidalCategory V] (C : EnrichedCat V) : EnrichedCategory V ↑C

def CategoryTheory.EnrichedCat.of (V : Type v) [Category.{w, v} V] [MonoidalCategory V] (C : Type u) [EnrichedCategory V C] : EnrichedCat V

Construct a bundled EnrichedCat from the underlying type and the typeclass.

def CategoryTheory.EnrichedCat.whiskerLeft {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] (F : EnrichedFunctor V C D) {G H : EnrichedFunctor V D E} (α : G ⟶ H) : EnrichedFunctor.comp V F G ⟶ EnrichedFunctor.comp V F H

Whisker a V-enriched natural transformation on the left.

@[simp]

theorem CategoryTheory.EnrichedCat.whiskerLeft_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] (F : EnrichedFunctor V C D) {G H : EnrichedFunctor V D E} (α : G ⟶ H) (X : ForgetEnrichment V C) : (whiskerLeft F α).out.app X = α.out.app (ForgetEnrichment.of V (F.obj (ForgetEnrichment.to V X)))

def CategoryTheory.EnrichedCat.whiskerRight {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {F G : EnrichedFunctor V C D} (α : F ⟶ G) (H : EnrichedFunctor V D E) : EnrichedFunctor.comp V F H ⟶ EnrichedFunctor.comp V G H

Whisker a V-enriched natural transformation on the right.

@[simp]

theorem CategoryTheory.EnrichedCat.whiskerRight_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {F G : EnrichedFunctor V C D} (α : F ⟶ G) (H : EnrichedFunctor V D E) (X : ForgetEnrichment V C) : (whiskerRight α H).out.app X = ForgetEnrichment.homOf V (CategoryStruct.comp (ForgetEnrichment.homTo V (α.out.app X)) (H.map (F.obj (ForgetEnrichment.to V X)) (G.obj (ForgetEnrichment.to V X))))

def CategoryTheory.EnrichedCat.leftUnitor {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) : EnrichedFunctor.comp V (EnrichedFunctor.id V C) F ≅ F

Composing the V-enriched identity functor with any functor is isomorphic to that functor.

@[simp]

theorem CategoryTheory.EnrichedCat.leftUnitor_inv_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) (X : ForgetEnrichment V C) : (leftUnitor F).inv.out.app X = CategoryStruct.id (ForgetEnrichment.of V (F.obj (ForgetEnrichment.to V X)))

@[simp]

theorem CategoryTheory.EnrichedCat.leftUnitor_hom_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) (X : ForgetEnrichment V C) : (leftUnitor F).hom.out.app X = CategoryStruct.id (ForgetEnrichment.of V (F.obj (ForgetEnrichment.to V X)))

def CategoryTheory.EnrichedCat.rightUnitor {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) : EnrichedFunctor.comp V F (EnrichedFunctor.id V D) ≅ F

Composing any V-enriched functor with the identity functor is isomorphic to the former functor.

@[simp]

theorem CategoryTheory.EnrichedCat.rightUnitor_inv_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) (X : ForgetEnrichment V C) : (rightUnitor F).inv.out.app X = CategoryStruct.id (ForgetEnrichment.of V (F.obj (ForgetEnrichment.to V X)))

@[simp]

theorem CategoryTheory.EnrichedCat.rightUnitor_hom_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) (X : ForgetEnrichment V C) : (rightUnitor F).hom.out.app X = CategoryStruct.id (ForgetEnrichment.of V (F.obj (ForgetEnrichment.to V X)))

def CategoryTheory.EnrichedCat.associator {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {E' : Type u₃} [EnrichedCategory V E'] (F : EnrichedFunctor V C D) (G : EnrichedFunctor V D E) (H : EnrichedFunctor V E E') : EnrichedFunctor.comp V (EnrichedFunctor.comp V F G) H ≅ EnrichedFunctor.comp V F (EnrichedFunctor.comp V G H)

Composition of V-enriched functors is associative up to isomorphism.

@[simp]

theorem CategoryTheory.EnrichedCat.associator_hom_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {E' : Type u₃} [EnrichedCategory V E'] (F : EnrichedFunctor V C D) (G : EnrichedFunctor V D E) (H : EnrichedFunctor V E E') (X : ForgetEnrichment V C) : (associator F G H).hom.out.app X = CategoryStruct.id (ForgetEnrichment.of V (H.obj (G.obj (F.obj (ForgetEnrichment.to V X)))))

@[simp]

theorem CategoryTheory.EnrichedCat.associator_inv_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {E' : Type u₃} [EnrichedCategory V E'] (F : EnrichedFunctor V C D) (G : EnrichedFunctor V D E) (H : EnrichedFunctor V E E') (X : ForgetEnrichment V C) : (associator F G H).inv.out.app X = CategoryStruct.id (ForgetEnrichment.of V (H.obj (G.obj (F.obj (ForgetEnrichment.to V X)))))

theorem CategoryTheory.EnrichedCat.comp_whiskerRight {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {F G H : EnrichedFunctor V C D} (α : F ⟶ G) (β : G ⟶ H) (I : EnrichedFunctor V D E) : whiskerRight { out := CategoryStruct.comp α.out β.out } I = CategoryStruct.comp (whiskerRight α I) (whiskerRight β I)

theorem CategoryTheory.EnrichedCat.whisker_exchange {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {F G : EnrichedFunctor V C D} {H I : EnrichedFunctor V D E} (α : F ⟶ G) (β : H ⟶ I) : CategoryStruct.comp (whiskerLeft F β) (whiskerRight α I) = CategoryStruct.comp (whiskerRight α H) (whiskerLeft G β)

@[implicit_reducible]

instance CategoryTheory.EnrichedCat.bicategory {V : Type v} [Category.{w, v} V] [MonoidalCategory V] : Bicategory (EnrichedCat V)

The bicategory structure on EnrichedCat V for a monoidal category V.