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 notion reduce to the usual ones.

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

• Hom : C → C → V
• id : (X : C) → CategoryTheory.MonoidalCategory.tensorUnit 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.tensorHom (CategoryTheory.EnrichedCategory.id X) (CategoryTheory.CategoryStruct.id (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.tensorHom (CategoryTheory.CategoryStruct.id (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.tensorHom (CategoryTheory.EnrichedCategory.comp W X Y) (CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom Y Z))) (CategoryTheory.EnrichedCategory.comp W Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom W X)) (CategoryTheory.EnrichedCategory.comp X Y Z)) (CategoryTheory.EnrichedCategory.comp W X Z)

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!

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.e_assoc_assoc (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (W : C) (X : C) (Y : C) (Z : C) {Z : V} (h : CategoryTheory.EnrichedCategory.Hom W Z ⟶ Z) : 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.tensorHom (CategoryTheory.eComp V W X Y) (CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom Y Z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W Y Z) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom W X)) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W X Z) h)

@[simp]

theorem CategoryTheory.e_assoc (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (W : C) (X : C) (Y : C) (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.tensorHom (CategoryTheory.eComp V W X Y) (CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom Y Z))) (CategoryTheory.eComp V W Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom W X)) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.eComp V W X Z)

def CategoryTheory.TransportEnrichment {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {W : Type v} [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] : CategoryTheory.LaxMonoidalFunctor V W → 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} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {W : Type v} [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.LaxMonoidalFunctor V W) : CategoryTheory.EnrichedCategory W (CategoryTheory.TransportEnrichment F C)

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

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

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

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

def CategoryTheory.enrichedCategoryTypeEquivCategory (C : Type u₁) : CategoryTheory.EnrichedCategory (Type v) C ≃ CategoryTheory.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 + 1)) [CategoryTheory.Category.{v, v + 1} W] [CategoryTheory.MonoidalCategory W] (C : Type u₁) [CategoryTheory.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 + 1)) [CategoryTheory.Category.{v, v + 1} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] (X : C) : CategoryTheory.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 + 1)) [CategoryTheory.Category.{v, v + 1} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.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 + 1)) [CategoryTheory.Category.{v, v + 1} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] (X : C) : CategoryTheory.ForgetEnrichment.to W (CategoryTheory.ForgetEnrichment.of W X) = X

@[simp]

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

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

def CategoryTheory.ForgetEnrichment.homOf {C : Type u₁} (W : Type (v + 1)) [CategoryTheory.Category.{v, v + 1} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] {X : C} {Y : C} (f : CategoryTheory.MonoidalCategory.tensorUnit W ⟶ CategoryTheory.EnrichedCategory.Hom X Y) : CategoryTheory.ForgetEnrichment.of W X ⟶ CategoryTheory.ForgetEnrichment.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 + 1)) [CategoryTheory.Category.{v, v + 1} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] {X : CategoryTheory.ForgetEnrichment W C} {Y : CategoryTheory.ForgetEnrichment W C} (f : X ⟶ Y) : CategoryTheory.MonoidalCategory.tensorUnit W ⟶ CategoryTheory.EnrichedCategory.Hom (CategoryTheory.ForgetEnrichment.to W X) (CategoryTheory.ForgetEnrichment.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 + 1)) [CategoryTheory.Category.{v, v + 1} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] {X : C} {Y : C} (f : CategoryTheory.MonoidalCategory.tensorUnit W ⟶ CategoryTheory.EnrichedCategory.Hom X Y) : CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.ForgetEnrichment.homOf W f) = f

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

• obj : C → D
• map : (X Y : C) → CategoryTheory.EnrichedCategory.Hom X Y ⟶ CategoryTheory.EnrichedCategory.Hom (CategoryTheory.EnrichedFunctor.obj s X) (CategoryTheory.EnrichedFunctor.obj s Y)
• map_id : ∀ (X : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (CategoryTheory.EnrichedFunctor.map s X X) = CategoryTheory.eId V (CategoryTheory.EnrichedFunctor.obj s X)
• map_comp : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (CategoryTheory.EnrichedFunctor.map s X Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.EnrichedFunctor.map s X Y) (CategoryTheory.EnrichedFunctor.map s Y Z)) (CategoryTheory.eComp V (CategoryTheory.EnrichedFunctor.obj s X) (CategoryTheory.EnrichedFunctor.obj s Y) (CategoryTheory.EnrichedFunctor.obj s Z))

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.EnrichedFunctor.id_map (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] (C : Type u₁) [CategoryTheory.EnrichedCategory V C] (X : C) (Y : C) : CategoryTheory.EnrichedFunctor.map (CategoryTheory.EnrichedFunctor.id V C) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom X Y)

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

The identity enriched functor.

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

@[simp]

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

@[simp]

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

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

Composition of enriched functors.

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

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

We now turn to natural transformations between V-functors.

The mostly 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.)

theorem CategoryTheory.GradedNatTrans.ext_iff {V : Type v} : ∀ {inst : CategoryTheory.Category.{w, v} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u₁} {inst_2 : CategoryTheory.EnrichedCategory V C} {D : Type u₂} {inst_3 : CategoryTheory.EnrichedCategory V D} {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (x y : CategoryTheory.GradedNatTrans A F G), x = y ↔ x.app = y.app

theorem CategoryTheory.GradedNatTrans.ext {V : Type v} : ∀ {inst : CategoryTheory.Category.{w, v} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u₁} {inst_2 : CategoryTheory.EnrichedCategory V C} {D : Type u₂} {inst_3 : CategoryTheory.EnrichedCategory V D} {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (x y : CategoryTheory.GradedNatTrans A F G), x.app = y.app → x = y

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

• app : (X : C) → A.fst ⟶ CategoryTheory.EnrichedCategory.Hom (CategoryTheory.EnrichedFunctor.obj F X) (CategoryTheory.EnrichedFunctor.obj G X)
• naturality : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.HalfBraiding.β A.snd (CategoryTheory.EnrichedCategory.Hom X Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.EnrichedFunctor.map F X Y) (CategoryTheory.GradedNatTrans.app s Y)) (CategoryTheory.eComp V (CategoryTheory.EnrichedFunctor.obj F X) (CategoryTheory.EnrichedFunctor.obj F Y) (CategoryTheory.EnrichedFunctor.obj G Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.GradedNatTrans.app s X) (CategoryTheory.EnrichedFunctor.map G X Y)) (CategoryTheory.eComp V (CategoryTheory.EnrichedFunctor.obj F X) (CategoryTheory.EnrichedFunctor.obj G X) (CategoryTheory.EnrichedFunctor.obj G Y))

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.

@[simp]

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

@[simp]

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

def CategoryTheory.enrichedNatTransYoneda {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] [CategoryTheory.BraidedCategory V] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V C D) : CategoryTheory.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.enrichedFunctorTypeEquivFunctor_apply_map {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.EnrichedFunctor (Type v) C D) : ∀ {X Y : C} (f : X ⟶ Y), (↑CategoryTheory.enrichedFunctorTypeEquivFunctor F).map f = CategoryTheory.EnrichedFunctor.map (Type v) CategoryTheory.types CategoryTheory.typesMonoidal C 𝒞 D 𝒟 F X Y f

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_map {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.Functor C D) (X : C) (Y : C) (f : CategoryTheory.EnrichedCategory.Hom X Y) : CategoryTheory.EnrichedFunctor.map (Type v) CategoryTheory.types CategoryTheory.typesMonoidal C 𝒞 D 𝒟 (↑CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F) X Y f = F.map f

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

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

def CategoryTheory.enrichedNatTransYonedaTypeIsoYonedaNatTrans {C : Type v} [CategoryTheory.EnrichedCategory (Type v) C] {D : Type v} [CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.EnrichedFunctor (Type v) C D) (G : CategoryTheory.EnrichedFunctor (Type v) C D) : CategoryTheory.enrichedNatTransYoneda F G ≅ CategoryTheory.yoneda.obj (↑CategoryTheory.enrichedFunctorTypeEquivFunctor F ⟶ ↑CategoryTheory.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!