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]

abbrev CategoryTheory.SimplicialCategory (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max (max u (v + 1)) v)

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.

Equations

• CategoryTheory.SimplicialCategory C = CategoryTheory.EnrichedOrdinaryCategory SSet C

@[reducible, inline]

abbrev CategoryTheory.SimplicialCategory.sHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (K : C) (L : C) : SSet

Abbreviation for the enriched hom of a simplicial category.

Equations

• CategoryTheory.SimplicialCategory.sHom K L = CategoryTheory.EnrichedCategory.Hom K L

@[reducible, inline]

abbrev CategoryTheory.SimplicialCategory.sHomComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (K : C) (L : C) (M : C) : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.SimplicialCategory.sHom K L) (CategoryTheory.SimplicialCategory.sHom L M) ⟶ CategoryTheory.SimplicialCategory.sHom K M

Abbreviation for the enriched composition in a simplicial category.

Equations

• CategoryTheory.SimplicialCategory.sHomComp K L M = CategoryTheory.eComp SSet K L M

def CategoryTheory.SimplicialCategory.homEquiv' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (K : C) (L : C) : (K ⟶ L) ≃ (CategoryTheory.SimplicialCategory.sHom K L).obj (Opposite.op (SimplexCategory.mk 0))

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.eHomEquiv SSet).trans (CategoryTheory.SimplicialCategory.sHom K L).unitHomEquiv

@[reducible, inline]

noncomputable abbrev CategoryTheory.SimplicialCategory.sHomFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C SSet)

The bifunctor Cᵒᵖ ⥤ C ⥤ SSet.{v} which sends K : Cᵒᵖ and L : C to sHom K.unop L.

Equations

• CategoryTheory.SimplicialCategory.sHomFunctor C = CategoryTheory.eHomFunctor SSet C