Simplicial categories #
A simplicial category is a category C
that is enriched over the
category of simplicial sets in such a way that morphisms in
C
identify to the 0
-simplices of the enriched hom.
TODO #
- construct a simplicial category structure on simplicial objects, so that it applies in particular to simplicial sets
- obtain the adjunction property
(K ⊗ X ⟶ Y) ≃ (K ⟶ sHom X Y)
whenK
,X
, andY
are simplicial sets - develop the notion of "simplicial tensor"
K ⊗ₛ X : C
withK : SSet
andX : C
an object in a simplicial categoryC
- define the notion of path between
0
-simplices of simplicial sets - deduce the notion of homotopy between morphisms in a simplicial category
- obtain that homotopies in simplicial categories can be interpreted as given
by morphisms
Δ[1] ⊗ X ⟶ Y
.
References #
- [Daniel G. Quillen, Homotopical algebra, II §1][quillen-1967]
A simplicial category is a category C
that is enriched over the
category of simplicial sets in such a way that morphisms in
C
identify to the 0
-simplices of the enriched hom.
- Hom : C → C → SSet
- id : (X : C) → 𝟙_ SSet ⟶ 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.whiskerRight (CategoryTheory.EnrichedCategory.id X) (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.whiskerLeft (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.whiskerRight (CategoryTheory.EnrichedCategory.comp W X Y) (CategoryTheory.EnrichedCategory.Hom Y Z)) (CategoryTheory.EnrichedCategory.comp W Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom W X) (CategoryTheory.EnrichedCategory.comp X Y Z)) (CategoryTheory.EnrichedCategory.comp W X Z)
- homEquiv : (K L : C) → (K ⟶ L) ≃ (𝟙_ SSet ⟶ CategoryTheory.EnrichedCategory.Hom K L)
morphisms identify to
0
-simplices of the enriched hom - homEquiv_id : ∀ (K : C), (CategoryTheory.SimplicialCategory.homEquiv K K) (CategoryTheory.CategoryStruct.id K) = CategoryTheory.eId SSet K
- homEquiv_comp : ∀ {K L M : C} (f : K ⟶ L) (g : L ⟶ M), (CategoryTheory.SimplicialCategory.homEquiv K M) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ SSet)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ((CategoryTheory.SimplicialCategory.homEquiv K L) f) ((CategoryTheory.SimplicialCategory.homEquiv L M) g)) (CategoryTheory.eComp SSet K L M))
Instances
Abbreviation for the enriched hom of a simplicial category.
Equations
Instances For
Abbreviation for the enriched composition in a simplicial category.
Equations
Instances For
The bijection (K ⟶ L) ≃ sHom K L _[0]
for all objects K
and L
in a simplicial category.
Equations
- CategoryTheory.SimplicialCategory.homEquiv' K L = (CategoryTheory.SimplicialCategory.homEquiv K L).trans (CategoryTheory.SimplicialCategory.sHom K L).unitHomEquiv
Instances For
The morphism sHom K' L ⟶ sHom K L
induced by a morphism K ⟶ K'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The morphism sHom K L ⟶ sHom K L'
induced by a morphism L ⟶ L'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bifunctor Cᵒᵖ ⥤ C ⥤ SSet.{v}
which sends K : Cᵒᵖ
and L : C
to sHom K.unop L
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.SimplicialCategory.instSymmetricCategorySSet = inferInstance