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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {K K' : C} (f : K ⟶ K') (L : C) : CategoryTheory.SimplicialCategory.sHom K' L ⟶ CategoryTheory.SimplicialCategory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (K L : C) : CategoryTheory.SimplicialCategory.sHomWhiskerRight (CategoryTheory.CategoryStruct.id K) L = CategoryTheory.CategoryStruct.id (CategoryTheory.SimplicialCategory.sHom K L)

@[simp]

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

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.SimplicialCategory.sHomWhiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (K : C) {L L' : C} (g : L ⟶ L') : CategoryTheory.SimplicialCategory.sHom K L ⟶ CategoryTheory.SimplicialCategory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (K L : C) : CategoryTheory.SimplicialCategory.sHomWhiskerLeft K (CategoryTheory.CategoryStruct.id L) = CategoryTheory.CategoryStruct.id (CategoryTheory.SimplicialCategory.sHom K L)

@[simp]

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

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

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

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

noncomputable instance CategoryTheory.SimplicialCategory.instSSet_infinityCosmos : CategoryTheory.SimplicialCategory SSet

Equations

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

noncomputable instance CategoryTheory.SimplicialCategory.instSymmetricCategorySSet_infinityCosmos : CategoryTheory.SymmetricCategory SSet

Equations

• CategoryTheory.SimplicialCategory.instSymmetricCategorySSet_infinityCosmos = inferInstance