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.
- 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!
Instances
The 𝟙_ V
-shaped generalized element giving the identity in a V
-enriched category.
Instances For
The composition V
-morphism for a V
-enriched category.
Instances For
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.
Instances For
Construct an honest category from a Type v
-enriched category.
Instances For
Construct a Type v
-enriched category from an honest category.
Instances For
We verify that an enriched category in Type u
is just the same thing as an honest category.
Instances For
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
?)
Instances For
Typecheck an object of C
as an object of ForgetEnrichment W C
.
Instances For
Typecheck an object of ForgetEnrichment W C
as an object of C
.
Instances For
Typecheck a (𝟙_ W)
-shaped W
-morphism as a morphism in ForgetEnrichment W C
.
Instances For
Typecheck a morphism in ForgetEnrichment W C
as a (𝟙_ W)
-shaped W
-morphism.
Instances For
The identity in the "underlying" category of an enriched category.
Composition in the "underlying" category of an enriched category.
- 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.
Instances For
The identity enriched functor.
Instances For
Composition of enriched functors.
Instances For
An enriched functor induces an honest functor of the underlying categories,
by mapping the (𝟙_ W)
-shaped morphisms.
Instances For
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
.)
- 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.
Instances For
A presheaf isomorphic to the Yoneda embedding of
the V
-object of natural transformations from F
to G
.
Instances For
We verify that an enriched functor between Type v
enriched categories
is just the same thing as an honest functor.
Instances For
We verify that the presheaf representing natural transformations
between Type v
-enriched functors is actually represented by
the usual type of natural transformations!