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]

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

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))

theorem CategoryTheory.SimplicialCategory.homEquiv_id {C : Type u} [CategoryTheory.Category.{v, u} C] [self : CategoryTheory.SimplicialCategory C] (K : C) : (CategoryTheory.SimplicialCategory.homEquiv K K) (CategoryTheory.CategoryStruct.id K) = CategoryTheory.eId SSet K

theorem CategoryTheory.SimplicialCategory.homEquiv_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [self : CategoryTheory.SimplicialCategory C] {K : C} {L : C} {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))

@[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 { unop := 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.SimplicialCategory.homEquiv K L).trans (CategoryTheory.SimplicialCategory.sHom K L).unitHomEquiv

noncomputable def CategoryTheory.SimplicialCategory.sHomWhiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {K : C} {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

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

@[simp]

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

theorem CategoryTheory.SimplicialCategory.sHomWhiskerRight_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {K : C} {K' : C} {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)

@[simp]

theorem CategoryTheory.SimplicialCategory.sHomWhiskerRight_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {K : C} {K' : C} {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)

noncomputable def CategoryTheory.SimplicialCategory.sHomWhiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (K : C) {L : C} {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

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

@[simp]

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

theorem CategoryTheory.SimplicialCategory.sHomWhiskerLeft_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (K : C) {L : C} {L' : C} {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)

@[simp]

theorem CategoryTheory.SimplicialCategory.sHomWhiskerLeft_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (K : C) {L : C} {L' : C} {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.sHom_whisker_exchange_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {K : C} {K' : C} {L : C} {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)

theorem CategoryTheory.SimplicialCategory.sHom_whisker_exchange {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {K : C} {K' : C} {L : C} {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)

@[simp]

theorem CategoryTheory.SimplicialCategory.sHomFunctor_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : ∀ {X Y : Cᵒᵖ} (φ : X ⟶ Y) (L : C), ((CategoryTheory.SimplicialCategory.sHomFunctor C).map φ).app L = CategoryTheory.SimplicialCategory.sHomWhiskerRight φ.unop L

@[simp]

theorem CategoryTheory.SimplicialCategory.sHomFunctor_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (K : Cᵒᵖ) : ∀ {X Y : C} (φ : X ⟶ Y), ((CategoryTheory.SimplicialCategory.sHomFunctor C).obj K).map φ = CategoryTheory.SimplicialCategory.sHomWhiskerLeft K.unop φ

@[simp]

theorem CategoryTheory.SimplicialCategory.sHomFunctor_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (K : Cᵒᵖ) (L : C) : ((CategoryTheory.SimplicialCategory.sHomFunctor C).obj K).obj L = CategoryTheory.SimplicialCategory.sHom K.unop L

noncomputable def 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

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