Enriched categories

We set up the basic theory of V-enriched categories, for V an arbitrary monoidal category.

We do not assume here that V is a concrete category, so there does not need to be an "honest" underlying category!

Use X ⟶[V] Y to obtain the V object of morphisms from X to Y.

This file contains the definitions of V-enriched categories and V-functors.

We don't yet define the V-object of natural transformations between a pair of V-functors (this requires limits in V), but we do provide a presheaf isomorphic to the Yoneda embedding of this object.

We verify that when V = Type v, all these notions reduce to the usual ones.

References

• [Kim Morrison, David Penneys, Monoidal Categories Enriched in Braided Monoidal Categories] [morrison-penney-enriched]

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

A V-category is a category enriched in a monoidal category V.

Note that we do not assume that V is a concrete category, so there may not be an "honest" underlying category at all!

• Hom : C → C → V

  X ⟶[V] Y is the V object of morphisms from X to Y.

• id (X : C) : MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] X

  The identity morphism of this category

• comp (X Y Z : C) : MonoidalCategoryStruct.tensorObj (X ⟶[V] Y) (Y ⟶[V] Z) ⟶ X ⟶[V] Z

  Composition of two morphisms in this category

• 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)

def CategoryTheory.«term_⟶[_]_» : Lean.TrailingParserDescr

X ⟶[V] Y is the V object of morphisms from X to Y.

def CategoryTheory.eId (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] (X : C) : MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] X

The 𝟙_ V-shaped generalized element giving the identity in a V-enriched category.

def CategoryTheory.eComp (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] (X Y Z : C) : MonoidalCategoryStruct.tensorObj (X ⟶[V] Y) (Y ⟶[V] Z) ⟶ X ⟶[V] Z

The composition V-morphism for a V-enriched category.

@[simp]

theorem CategoryTheory.e_id_comp (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] (X Y : C) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (X ⟶[V] Y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eId V X) (X ⟶[V] Y)) (eComp V X X Y)) = CategoryStruct.id (X ⟶[V] Y)

@[simp]

theorem CategoryTheory.e_id_comp_assoc (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] (X Y : C) {Z : V} (h : (X ⟶[V] Y) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (X ⟶[V] Y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eId V X) (X ⟶[V] Y)) (CategoryStruct.comp (eComp V X X Y) h)) = h

@[simp]

theorem CategoryTheory.e_comp_id (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] (X Y : C) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (eId V Y)) (eComp V X Y Y)) = CategoryStruct.id (X ⟶[V] Y)

@[simp]

theorem CategoryTheory.e_comp_id_assoc (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] (X Y : C) {Z : V} (h : (X ⟶[V] Y) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (eId V Y)) (CategoryStruct.comp (eComp V X Y Y) h)) = h

@[simp]

theorem CategoryTheory.e_assoc (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] (W X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eComp V W X Y) (Y ⟶[V] Z)) (eComp V W Y Z)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (eComp V X Y Z)) (eComp V W X Z)

@[simp]

theorem CategoryTheory.e_assoc_assoc (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] (W X Y Z : C) {Z✝ : V} (h : (W ⟶[V] Z) ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eComp V W X Y) (Y ⟶[V] Z)) (CategoryStruct.comp (eComp V W Y Z) h)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (eComp V X Y Z)) (CategoryStruct.comp (eComp V W X Z) h)

theorem CategoryTheory.e_assoc' (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] (W X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (eComp V X Y Z)) (eComp V W X Z)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eComp V W X Y) (Y ⟶[V] Z)) (eComp V W Y Z)

theorem CategoryTheory.e_assoc'_assoc (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] (W X Y Z : C) {Z✝ : V} (h : (W ⟶[V] Z) ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (eComp V X Y Z)) (CategoryStruct.comp (eComp V W X Z) h)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (eComp V W X Y) (Y ⟶[V] Z)) (CategoryStruct.comp (eComp V W Y Z) h)

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

A type synonym for C, which should come equipped with a V-enriched category structure. In a moment we will equip this with the W-enriched category structure obtained by applying the functor F : LaxMonoidalFunctor V W to each hom object.

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

theorem CategoryTheory.TransportEnrichment.eId_eq {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {W : Type v'} [Category.{w', v'} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (X : TransportEnrichment F C) : eId W X = CategoryStruct.comp (Functor.LaxMonoidal.ε F) (F.map (eId V X))

theorem CategoryTheory.TransportEnrichment.eComp_eq {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {W : Type v'} [Category.{w', v'} W] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] (X Y Z : TransportEnrichment F C) : eComp W X Y Z = CategoryStruct.comp (Functor.LaxMonoidal.μ F (X ⟶[V] Y) (Y ⟶[V] Z)) (F.map (eComp V X Y Z))

def CategoryTheory.categoryOfEnrichedCategoryType (C : Type u₁) [𝒞 : EnrichedCategory (Type v) C] : Category.{v, u₁} C

Construct an honest category from a Type v-enriched category.

def CategoryTheory.enrichedCategoryTypeOfCategory (C : Type u₁) [𝒞 : Category.{v, u₁} C] : EnrichedCategory (Type v) C

Construct a Type v-enriched category from an honest category.

def CategoryTheory.enrichedCategoryTypeEquivCategory (C : Type u₁) : EnrichedCategory (Type v) C ≃ Category.{v, u₁} C

We verify that an enriched category in Type u is just the same thing as an honest category.

def CategoryTheory.ForgetEnrichment (W : Type v) [Category.{w, v} W] [MonoidalCategory W] (C : Type u₁) [EnrichedCategory W C] : Type u₁

A type synonym for C, which should come equipped with a V-enriched category structure. In a moment we will equip this with the (honest) category structure so that X ⟶ Y is (𝟙_ W) ⟶ (X ⟶[W] Y).

We obtain this category by transporting the enrichment in V along the lax monoidal functor coyonedaTensorUnit, then using the equivalence of Type-enriched categories with honest categories.

This is sometimes called the "underlying" category of an enriched category, although some care is needed as the functor coyonedaTensorUnit, which always exists, does not necessarily coincide with "the forgetful functor" from V to Type, if such exists. When V is any of Type, Top, AddCommGroup, or Module R, coyonedaTensorUnit is just the usual forgetful functor, however. For V = Algebra R, the usual forgetful functor is coyoneda of R[X], not of R. (Perhaps we should have a typeclass for this situation: ConcreteMonoidal?)

def CategoryTheory.ForgetEnrichment.of {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] (X : C) : ForgetEnrichment W C

Typecheck an object of C as an object of ForgetEnrichment W C.

def CategoryTheory.ForgetEnrichment.to {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] (X : ForgetEnrichment W C) : C

Typecheck an object of ForgetEnrichment W C as an object of C.

@[simp]

theorem CategoryTheory.ForgetEnrichment.to_of {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] (X : C) : «to» W (of W X) = X

@[simp]

theorem CategoryTheory.ForgetEnrichment.of_to {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] (X : ForgetEnrichment W C) : of W («to» W X) = X

instance CategoryTheory.categoryForgetEnrichment {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] : Category.{w, u₁} (ForgetEnrichment W C)

def CategoryTheory.ForgetEnrichment.homOf {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] {X Y : C} (f : MonoidalCategoryStruct.tensorUnit W ⟶ X ⟶[W] Y) : of W X ⟶ of W Y

Typecheck a (𝟙_ W)-shaped W-morphism as a morphism in ForgetEnrichment W C.

def CategoryTheory.ForgetEnrichment.homTo {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] {X Y : ForgetEnrichment W C} (f : X ⟶ Y) : MonoidalCategoryStruct.tensorUnit W ⟶ «to» W X ⟶[W] «to» W Y

Typecheck a morphism in ForgetEnrichment W C as a (𝟙_ W)-shaped W-morphism.

@[simp]

theorem CategoryTheory.ForgetEnrichment.homTo_homOf {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] {X Y : C} (f : MonoidalCategoryStruct.tensorUnit W ⟶ X ⟶[W] Y) : homTo W (homOf W f) = f

@[simp]

theorem CategoryTheory.ForgetEnrichment.homOf_homTo {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] {X Y : ForgetEnrichment W C} (f : X ⟶ Y) : homOf W (homTo W f) = f

@[simp]

theorem CategoryTheory.ForgetEnrichment.homTo_id {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] (X : ForgetEnrichment W C) : homTo W (CategoryStruct.id X) = eId W («to» W X)

The identity in the "underlying" category of an enriched category.

@[simp]

theorem CategoryTheory.ForgetEnrichment.homOf_eId {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] (X : C) : homOf W (eId W X) = CategoryStruct.id (of W X)

@[simp]

theorem CategoryTheory.ForgetEnrichment.homTo_comp {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] {X Y Z : ForgetEnrichment W C} (f : X ⟶ Y) (g : Y ⟶ Z) : homTo W (CategoryStruct.comp f g) = CategoryStruct.comp (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit W)).inv (MonoidalCategoryStruct.tensorHom (homTo W f) (homTo W g))) (eComp W («to» W X) («to» W Y) («to» W Z))

Composition in the "underlying" category of an enriched category.

@[simp]

theorem CategoryTheory.ForgetEnrichment.homOf_comp {C : Type u₁} (W : Type v) [Category.{w, v} W] [MonoidalCategory W] [EnrichedCategory W C] {X Y Z : C} (f : MonoidalCategoryStruct.tensorUnit W ⟶ X ⟶[W] Y) (g : MonoidalCategoryStruct.tensorUnit W ⟶ Y ⟶[W] Z) : homOf W (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit W)).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (eComp W X Y Z))) = CategoryStruct.comp (homOf W f) (homOf W g)

structure CategoryTheory.EnrichedFunctor (V : Type v) [Category.{w, v} V] [MonoidalCategory V] (C : Type u₁) [EnrichedCategory V C] (D : Type u₂) [EnrichedCategory V D] : Type (max (max u₁ u₂) w)

A V-functor F between V-enriched categories has a V-morphism from X ⟶[V] Y to F.obj X ⟶[V] F.obj Y, satisfying the usual axioms.

• obj : C → D

  The application of this functor to an object

• map (X Y : C) : (X ⟶[V] Y) ⟶ self.obj X ⟶[V] self.obj Y

  The V-morphism from X ⟶[V] Y to F.obj X ⟶[V] F.obj Y, for all X Y : C

• map_id (X : C) : CategoryStruct.comp (eId V X) (self.map X X) = eId V (self.obj X)
• map_comp (X Y Z : C) : CategoryStruct.comp (eComp V X Y Z) (self.map X Z) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (self.map X Y) (self.map Y Z)) (eComp V (self.obj X) (self.obj Y) (self.obj Z))

@[simp]

theorem CategoryTheory.EnrichedFunctor.map_id_assoc {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] (self : EnrichedFunctor V C D) (X : C) {Z : V} (h : (self.obj X ⟶[V] self.obj X) ⟶ Z) : CategoryStruct.comp (eId V X) (CategoryStruct.comp (self.map X X) h) = CategoryStruct.comp (eId V (self.obj X)) h

@[simp]

theorem CategoryTheory.EnrichedFunctor.map_comp_assoc {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] (self : EnrichedFunctor V C D) (X Y Z : C) {Z✝ : V} (h : (self.obj X ⟶[V] self.obj Z) ⟶ Z✝) : CategoryStruct.comp (eComp V X Y Z) (CategoryStruct.comp (self.map X Z) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (self.map X Y) (self.map Y Z)) (CategoryStruct.comp (eComp V (self.obj X) (self.obj Y) (self.obj Z)) h)

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

The identity enriched functor.

@[simp]

theorem CategoryTheory.EnrichedFunctor.id_map (V : Type v) [Category.{w, v} V] [MonoidalCategory V] (C : Type u₁) [EnrichedCategory V C] (x✝ x✝¹ : C) : (id V C).map x✝ x✝¹ = CategoryStruct.id (x✝ ⟶[V] x✝¹)

@[simp]

theorem CategoryTheory.EnrichedFunctor.id_obj (V : Type v) [Category.{w, v} V] [MonoidalCategory V] (C : Type u₁) [EnrichedCategory V C] (X : C) : (id V C).obj X = X

instance CategoryTheory.EnrichedFunctor.instInhabited (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] : Inhabited (EnrichedFunctor V C C)

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

Composition of enriched functors.

@[simp]

theorem CategoryTheory.EnrichedFunctor.comp_obj (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} {D : Type u₂} {E : Type u₃} [EnrichedCategory V C] [EnrichedCategory V D] [EnrichedCategory V E] (F : EnrichedFunctor V C D) (G : EnrichedFunctor V D E) (X : C) : (comp V F G).obj X = G.obj (F.obj X)

@[simp]

theorem CategoryTheory.EnrichedFunctor.comp_map (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} {D : Type u₂} {E : Type u₃} [EnrichedCategory V C] [EnrichedCategory V D] [EnrichedCategory V E] (F : EnrichedFunctor V C D) (G : EnrichedFunctor V D E) (x✝ x✝¹ : C) : (comp V F G).map x✝ x✝¹ = CategoryStruct.comp (F.map x✝ x✝¹) (G.map (F.obj x✝) (F.obj x✝¹))

theorem CategoryTheory.EnrichedFunctor.ext (V : Type v) [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} {D : Type u₂} [EnrichedCategory V C] [EnrichedCategory V D] {F G : EnrichedFunctor V C D} (h_obj : ∀ (X : C), F.obj X = G.obj X) (h_map : ∀ (X Y : C), CategoryStruct.comp (F.map X Y) (eqToHom ⋯) = G.map X Y) : F = G

def CategoryTheory.EnrichedFunctor.forget {W : Type v'} [Category.{w', v'} W] [MonoidalCategory W] {C : Type u₁} [EnrichedCategory W C] {D : Type u₂} [EnrichedCategory W D] (F : EnrichedFunctor W C D) : Functor (ForgetEnrichment W C) (ForgetEnrichment W D)

An enriched functor induces an honest functor of the underlying categories, by mapping the (𝟙_ W)-shaped morphisms.

@[simp]

theorem CategoryTheory.EnrichedFunctor.forget_map {W : Type v'} [Category.{w', v'} W] [MonoidalCategory W] {C : Type u₁} [EnrichedCategory W C] {D : Type u₂} [EnrichedCategory W D] (F : EnrichedFunctor W C D) {X✝ Y✝ : ForgetEnrichment W C} (f : X✝ ⟶ Y✝) : F.forget.map f = ForgetEnrichment.homOf W (CategoryStruct.comp (ForgetEnrichment.homTo W f) (F.map (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝)))

@[simp]

theorem CategoryTheory.EnrichedFunctor.forget_obj {W : Type v'} [Category.{w', v'} W] [MonoidalCategory W] {C : Type u₁} [EnrichedCategory W C] {D : Type u₂} [EnrichedCategory W D] (F : EnrichedFunctor W C D) (X : ForgetEnrichment W C) : F.forget.obj X = ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X))

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

EnrichedFunctor.forget distributes over composition of enriched functors up to isomorphism.

@[simp]

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

@[simp]

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

def CategoryTheory.EnrichedFunctor.forgetId (W : Type v') [Category.{w', v'} W] [MonoidalCategory W] (C : Type u₁) [EnrichedCategory W C] : (id W C).forget ≅ Functor.id (ForgetEnrichment W C)

EnrichedFunctor.forget maps the identity enriched functor to a functor isomorphic to Functor.id.

@[simp]

theorem CategoryTheory.EnrichedFunctor.forgetId_inv_app (W : Type v') [Category.{w', v'} W] [MonoidalCategory W] (C : Type u₁) [EnrichedCategory W C] (X : ForgetEnrichment W C) : (forgetId W C).inv.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.EnrichedFunctor.forgetId_hom_app (W : Type v') [Category.{w', v'} W] [MonoidalCategory W] (C : Type u₁) [EnrichedCategory W C] (X : ForgetEnrichment W C) : (forgetId W C).hom.app X = CategoryStruct.id X

We now turn to natural transformations between V-functors.

The most commonly encountered definition of an enriched natural transformation is a collection of morphisms

(𝟙_ W) ⟶ (F.obj X ⟶[V] G.obj X)

satisfying an appropriate analogue of the naturality square. (c.f. https://ncatlab.org/nlab/show/enriched+natural+transformation)

This is the same thing as a natural transformation F.forget ⟶ G.forget.

We formalize this as EnrichedNatTrans F G, which is a Type.

However, there's also something much nicer: with appropriate additional hypotheses, there is a V-object EnrichedNatTransObj F G which contains more information, and from which one can recover EnrichedNatTrans F G ≃ (𝟙_ V) ⟶ EnrichedNatTransObj F G.

Using these as the hom-objects, we can build a V-enriched category with objects the V-functors.

For EnrichedNatTransObj to exist, it suffices to have V braided and complete.

Before assuming V is complete, we assume it is braided and define a presheaf enrichedNatTransYoneda F G which is isomorphic to the Yoneda embedding of EnrichedNatTransObj F G whether or not that object actually exists.

This presheaf has components (enrichedNatTransYoneda F G).obj A what we call the A-graded enriched natural transformations, which are collections of morphisms

A ⟶ (F.obj X ⟶[V] G.obj X)

satisfying a similar analogue of the naturality square, this time incorporating a half-braiding on A.

(We actually define EnrichedNatTrans F G as the special case A := 𝟙_ V with the trivial half-braiding, and when defining enrichedNatTransYoneda F G we use the half-braidings coming from the ambient braiding on V.)

structure CategoryTheory.GradedNatTrans {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] (A : Center V) (F G : EnrichedFunctor V C D) : Type (max u₁ w)

The type of A-graded natural transformations between V-functors F and G. This is the type of morphisms in V from A to the V-object of natural transformations.

• app (X : C) : A.fst ⟶ F.obj X ⟶[V] G.obj X

  The A-graded transformation from F to G

• naturality (X Y : C) : CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map X Y) (self.app Y)) (eComp V (F.obj X) (F.obj Y) (G.obj Y))) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (self.app X) (G.map X Y)) (eComp V (F.obj X) (G.obj X) (G.obj Y))

  app is a natural transformation.

theorem CategoryTheory.GradedNatTrans.ext_iff {V : Type v} {inst✝ : Category.{w, v} V} {inst✝¹ : MonoidalCategory V} {C : Type u₁} {inst✝² : EnrichedCategory V C} {D : Type u₂} {inst✝³ : EnrichedCategory V D} {A : Center V} {F G : EnrichedFunctor V C D} {x y : GradedNatTrans A F G} : x = y ↔ x.app = y.app

theorem CategoryTheory.GradedNatTrans.ext {V : Type v} {inst✝ : Category.{w, v} V} {inst✝¹ : MonoidalCategory V} {C : Type u₁} {inst✝² : EnrichedCategory V C} {D : Type u₂} {inst✝³ : EnrichedCategory V D} {A : Center V} {F G : EnrichedFunctor V C D} {x y : GradedNatTrans A F G} (app : x.app = y.app) : x = y

theorem CategoryTheory.GradedNatTrans.naturality_assoc {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] {A : Center V} {F G : EnrichedFunctor V C D} (self : GradedNatTrans A F G) (X Y : C) {Z : V} (h : (F.obj X ⟶[V] G.obj Y) ⟶ Z) : CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map X Y) (self.app Y)) (CategoryStruct.comp (eComp V (F.obj X) (F.obj Y) (G.obj Y)) h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (self.app X) (G.map X Y)) (CategoryStruct.comp (eComp V (F.obj X) (G.obj X) (G.obj Y)) h)

app is a natural transformation.

structure CategoryTheory.EnrichedNatTrans {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] (F G : EnrichedFunctor V C D) : Type (max u₁ w)

A natural transformation between two enriched functors is a 𝟙_ V-graded natural transformation.

• out : F.forget ⟶ G.forget

  The underlying natural transformation of an enriched transformation.

instance CategoryTheory.EnrichedFunctor.category {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] : Category.{max u₁ w, max (max u₂ u₁) w} (EnrichedFunctor V C D)

Enriched functors form a category with the morphisms between functors F and G being enriched natural transformations, i.e. natural transformations F.forget ⟶ G.forget.

@[simp]

theorem CategoryTheory.EnrichedFunctor.category_comp_out {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] {X✝ Y✝ Z✝ : EnrichedFunctor V C D} (F : EnrichedNatTrans X✝ Y✝) (G : EnrichedNatTrans Y✝ Z✝) : (CategoryStruct.comp F G).out = CategoryStruct.comp F.out G.out

@[simp]

theorem CategoryTheory.EnrichedFunctor.category_id_out {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) : (CategoryStruct.id F).out = CategoryStruct.id F.forget

theorem CategoryTheory.EnrichedFunctor.hom_ext {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] {F G : EnrichedFunctor V C D} {α β : F ⟶ G} (h : ∀ (X : C), α.out.app X = β.out.app X) : α = β

theorem CategoryTheory.EnrichedFunctor.hom_ext_iff {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] {F G : EnrichedFunctor V C D} {α β : F ⟶ G} : α = β ↔ ∀ (X : C), α.out.app X = β.out.app X

def CategoryTheory.EnrichedFunctor.isoMk {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] {F G : EnrichedFunctor V C D} (h : F.forget ≅ G.forget) : F ≅ G

To construct an isomorphism between enriched functors F and G, it suffices to construct a natural isomorphism between F.forget and G.forget.

@[simp]

theorem CategoryTheory.EnrichedFunctor.isoMk_hom_out {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] {F G : EnrichedFunctor V C D} (h : F.forget ≅ G.forget) : (isoMk h).hom.out = h.hom

@[simp]

theorem CategoryTheory.EnrichedFunctor.isoMk_inv_out {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] {F G : EnrichedFunctor V C D} (h : F.forget ≅ G.forget) : (isoMk h).inv.out = h.inv

def CategoryTheory.enrichedNatTransYoneda {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] [BraidedCategory V] (F G : EnrichedFunctor V C D) : Functor Vᵒᵖ (Type (max u₁ w))

A presheaf isomorphic to the Yoneda embedding of the V-object of natural transformations from F to G.

@[simp]

theorem CategoryTheory.enrichedNatTransYoneda_map_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] [BraidedCategory V] (F G : EnrichedFunctor V C D) {X✝ Y✝ : Vᵒᵖ} (f : X✝ ⟶ Y✝) (σ : GradedNatTrans ((Center.ofBraided V).obj (Opposite.unop X✝)) F G) (X : C) : ((enrichedNatTransYoneda F G).map f σ).app X = CategoryStruct.comp f.unop (σ.app X)

@[simp]

theorem CategoryTheory.enrichedNatTransYoneda_obj {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u₁} [EnrichedCategory V C] {D : Type u₂} [EnrichedCategory V D] [BraidedCategory V] (F G : EnrichedFunctor V C D) (A : Vᵒᵖ) : (enrichedNatTransYoneda F G).obj A = GradedNatTrans ((Center.ofBraided V).obj (Opposite.unop A)) F G

def CategoryTheory.enrichedFunctorTypeEquivFunctor {C : Type u₁} [𝒞 : EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : EnrichedCategory (Type v) D] : EnrichedFunctor (Type v) C D ≃ Functor C D

We verify that an enriched functor between Type v enriched categories is just the same thing as an honest functor.

@[simp]

theorem CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_obj {C : Type u₁} [𝒞 : EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : EnrichedCategory (Type v) D] (F : EnrichedFunctor (Type v) C D) (X : C) : (enrichedFunctorTypeEquivFunctor F).obj X = F.obj X

@[simp]

theorem CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_map {C : Type u₁} [𝒞 : EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : EnrichedCategory (Type v) D] (F : EnrichedFunctor (Type v) C D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (enrichedFunctorTypeEquivFunctor F).map f = F.map X✝ Y✝ f

@[simp]

theorem CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_map {C : Type u₁} [𝒞 : EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : EnrichedCategory (Type v) D] (F : Functor C D) (x✝ x✝¹ : C) (f : x✝ ⟶[Type v] x✝¹) : (enrichedFunctorTypeEquivFunctor.symm F).map x✝ x✝¹ f = F.map f

@[simp]

theorem CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_obj {C : Type u₁} [𝒞 : EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : EnrichedCategory (Type v) D] (F : Functor C D) (X : C) : (enrichedFunctorTypeEquivFunctor.symm F).obj X = F.obj X

def CategoryTheory.enrichedNatTransYonedaTypeIsoYonedaNatTrans {C : Type v} [EnrichedCategory (Type v) C] {D : Type v} [EnrichedCategory (Type v) D] (F G : EnrichedFunctor (Type v) C D) : enrichedNatTransYoneda F G ≅ yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)

We verify that the presheaf representing natural transformations between Type v-enriched functors is actually represented by the usual type of natural transformations!