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
.
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_comp (X Y : C) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (Hom X Y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (id X) (Hom X Y)) (comp X X Y)) = CategoryStruct.id (Hom X Y)
- comp_id (X Y : C) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (Hom X Y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (Hom X Y) (id Y)) (comp X Y Y)) = CategoryStruct.id (Hom X Y)
- assoc (W X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.associator (Hom W X) (Hom X Y) (Hom Y Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (comp W X Y) (Hom Y Z)) (comp W Y Z)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (Hom W X) (comp X Y Z)) (comp W X Z)
morphisms
X ā¶ Y
in the category identify morphismsš_ V ā¶ (X ā¶[V] Y)
inV
- homEquiv_comp {X Y Z : C} (f : X ā¶ Y) (g : Y ā¶ Z) : homEquiv (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (š_ V)).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (homEquiv f) (homEquiv g)) (eComp V X Y Z))
Instances
The bijection (X ā¶ Y) ā (š_ V ā¶ (X ā¶[V] Y))
given by a
EnrichedOrdinaryCategory
instance.
Instances For
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.
Instances For
Whiskering commutes with the enriched composition.
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.
Instances For
Whiskering commutes with the enriched composition.
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
.
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.
Instances For
Equations
- CategoryTheory.ForgetEnrichment.EnrichedOrdinaryCategory V = CategoryTheory.EnrichedOrdinaryCategory.mk (fun {X Y : CategoryTheory.ForgetEnrichment V D} => Equiv.refl (X ā¶ Y)) āÆ āÆ
enriched coyoneda functor (X ā¶[V] _) : C ā„¤ V
.
Equations
- CategoryTheory.eCoyoneda V X = (CategoryTheory.eHomFunctor V C).obj (Opposite.op X)