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) when K, X, and Y are simplicial sets
• develop the notion of "simplicial tensor" K ⊗ₛ X : C with K : SSet and X : C an object in a simplicial category C
• 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]

@[reducible, inline]

noncomputable abbrev CategoryTheory.SimplicialCategory.sHomWhiskerRight {C : Type u} [Category.{v, u} C] [SimplicialCategory C] {K K' : C} (f : K ⟶ K') (L : C) : sHom K' L ⟶ sHom K L

The morphism sHom K' L ⟶ sHom K L induced by a morphism K ⟶ K'.

Equations

• CategoryTheory.SimplicialCategory.sHomWhiskerRight f L = CategoryTheory.eHomWhiskerRight SSet f L

@[simp]

theorem CategoryTheory.SimplicialCategory.sHomWhiskerRight_id {C : Type u} [Category.{v, u} C] [SimplicialCategory C] (K L : C) : sHomWhiskerRight (CategoryStruct.id K) L = CategoryStruct.id (sHom K L)

@[simp]

theorem CategoryTheory.SimplicialCategory.sHomWhiskerRight_comp {C : Type u} [Category.{v, u} C] [SimplicialCategory C] {K K' K'' : C} (f : K ⟶ K') (f' : K' ⟶ K'') (L : C) : sHomWhiskerRight (CategoryStruct.comp f f') L = CategoryStruct.comp (sHomWhiskerRight f' L) (sHomWhiskerRight f L)

theorem CategoryTheory.SimplicialCategory.sHomWhiskerRight_comp_assoc {C : Type u} [Category.{v, u} C] [SimplicialCategory C] {K K' K'' : C} (f : K ⟶ K') (f' : K' ⟶ K'') (L : C) {Z : SSet} (h : sHom K L ⟶ Z) : CategoryStruct.comp (sHomWhiskerRight (CategoryStruct.comp f f') L) h = CategoryStruct.comp (sHomWhiskerRight f' L) (CategoryStruct.comp (sHomWhiskerRight f L) h)

@[reducible, inline]

noncomputable abbrev CategoryTheory.SimplicialCategory.sHomWhiskerLeft {C : Type u} [Category.{v, u} C] [SimplicialCategory C] (K : C) {L L' : C} (g : L ⟶ L') : sHom K L ⟶ sHom K L'

The morphism sHom K L ⟶ sHom K L' induced by a morphism L ⟶ L'.

Equations

• CategoryTheory.SimplicialCategory.sHomWhiskerLeft K g = CategoryTheory.eHomWhiskerLeft SSet K g

@[simp]

theorem CategoryTheory.SimplicialCategory.sHomWhiskerLeft_id {C : Type u} [Category.{v, u} C] [SimplicialCategory C] (K L : C) : sHomWhiskerLeft K (CategoryStruct.id L) = CategoryStruct.id (sHom K L)

@[simp]

theorem CategoryTheory.SimplicialCategory.sHomWhiskerLeft_comp {C : Type u} [Category.{v, u} C] [SimplicialCategory C] (K : C) {L L' L'' : C} (g : L ⟶ L') (g' : L' ⟶ L'') : sHomWhiskerLeft K (CategoryStruct.comp g g') = CategoryStruct.comp (sHomWhiskerLeft K g) (sHomWhiskerLeft K g')

theorem CategoryTheory.SimplicialCategory.sHomWhiskerLeft_comp_assoc {C : Type u} [Category.{v, u} C] [SimplicialCategory C] (K : C) {L L' L'' : C} (g : L ⟶ L') (g' : L' ⟶ L'') {Z : SSet} (h : sHom K L'' ⟶ Z) : CategoryStruct.comp (sHomWhiskerLeft K (CategoryStruct.comp g g')) h = CategoryStruct.comp (sHomWhiskerLeft K g) (CategoryStruct.comp (sHomWhiskerLeft K g') h)

theorem CategoryTheory.SimplicialCategory.sHom_whisker_exchange {C : Type u} [Category.{v, u} C] [SimplicialCategory C] {K K' L L' : C} (f : K ⟶ K') (g : L ⟶ L') : CategoryStruct.comp (sHomWhiskerLeft K' g) (sHomWhiskerRight f L') = CategoryStruct.comp (sHomWhiskerRight f L) (sHomWhiskerLeft K g)

theorem CategoryTheory.SimplicialCategory.sHom_whisker_exchange_assoc {C : Type u} [Category.{v, u} C] [SimplicialCategory C] {K K' L L' : C} (f : K ⟶ K') (g : L ⟶ L') {Z : SSet} (h : sHom K L' ⟶ Z) : CategoryStruct.comp (sHomWhiskerLeft K' g) (CategoryStruct.comp (sHomWhiskerRight f L') h) = CategoryStruct.comp (sHomWhiskerRight f L) (CategoryStruct.comp (sHomWhiskerLeft K g) h)

noncomputable instance CategoryTheory.SimplicialCategory.instSSet_infinityCosmos : SimplicialCategory SSet

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.SimplicialCategory.instMonoidalClosedSSet_infinityCosmos : MonoidalClosed SSet

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.SimplicialCategory.instSymmetricCategorySSet_infinityCosmos : SymmetricCategory SSet

Equations

• CategoryTheory.SimplicialCategory.instSymmetricCategorySSet_infinityCosmos = inferInstance