The monoidal category structure on simplicial sets

This file defines an instance of chosen finite products for the category SSet. It follows from the fact the SSet if a category of functors to the category of types and that the category of types have chosen finite products. As a result, we obtain a monoidal category structure on SSet.

noncomputable instance SSet.instChosenFiniteProducts : CategoryTheory.ChosenFiniteProducts SSet

Equations

• SSet.instChosenFiniteProducts = inferInstance

@[simp]

theorem SSet.leftUnitor_hom_app_apply (K : SSet) {Δ : SimplexCategoryᵒᵖ} (x : (CategoryTheory.MonoidalCategory.tensorObj (𝟙_ SSet) K).obj Δ) : (CategoryTheory.MonoidalCategory.leftUnitor K).hom.app Δ x = x.2

@[simp]

theorem SSet.leftUnitor_inv_app_apply (K : SSet) {Δ : SimplexCategoryᵒᵖ} (x : K.obj Δ) : (CategoryTheory.MonoidalCategory.leftUnitor K).inv.app Δ x = (PUnit.unit, x)

@[simp]

theorem SSet.rightUnitor_hom_app_apply (K : SSet) {Δ : SimplexCategoryᵒᵖ} (x : (CategoryTheory.MonoidalCategory.tensorObj K (𝟙_ SSet)).obj Δ) : (CategoryTheory.MonoidalCategory.rightUnitor K).hom.app Δ x = x.1

@[simp]

theorem SSet.rightUnitor_inv_app_apply (K : SSet) {Δ : SimplexCategoryᵒᵖ} (x : K.obj Δ) : (CategoryTheory.MonoidalCategory.rightUnitor K).inv.app Δ x = (x, PUnit.unit)

@[simp]

theorem SSet.tensorHom_app_apply {K K' L L' : SSet} (f : K ⟶ K') (g : L ⟶ L') {Δ : SimplexCategoryᵒᵖ} (x : (CategoryTheory.MonoidalCategory.tensorObj K L).obj Δ) : (CategoryTheory.MonoidalCategory.tensorHom f g).app Δ x = (f.app Δ x.1, g.app Δ x.2)

@[simp]

theorem SSet.whiskerLeft_app_apply (K : SSet) {L L' : SSet} (g : L ⟶ L') {Δ : SimplexCategoryᵒᵖ} (x : (CategoryTheory.MonoidalCategory.tensorObj K L).obj Δ) : (CategoryTheory.MonoidalCategory.whiskerLeft K g).app Δ x = (x.1, g.app Δ x.2)

@[simp]

theorem SSet.whiskerRight_app_apply {K K' : SSet} (f : K ⟶ K') (L : SSet) {Δ : SimplexCategoryᵒᵖ} (x : (CategoryTheory.MonoidalCategory.tensorObj K L).obj Δ) : (CategoryTheory.MonoidalCategory.whiskerRight f L).app Δ x = (f.app Δ x.1, x.2)

@[simp]

theorem SSet.associator_hom_app_apply (K L M : SSet) {Δ : SimplexCategoryᵒᵖ} (x : (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj K L) M).obj Δ) : (CategoryTheory.MonoidalCategory.associator K L M).hom.app Δ x = (x.1.1, x.1.2, x.2)

@[simp]

theorem SSet.associator_inv_app_apply (K L M : SSet) {Δ : SimplexCategoryᵒᵖ} (x : (CategoryTheory.MonoidalCategory.tensorObj K (CategoryTheory.MonoidalCategory.tensorObj L M)).obj Δ) : (CategoryTheory.MonoidalCategory.associator K L M).inv.app Δ x = ((x.1, x.2.1), x.2.2)

def SSet.unitHomEquiv (K : SSet) : (𝟙_ SSet ⟶ K) ≃ K.obj (Opposite.op (SimplexCategory.mk 0))

The bijection (𝟙_ SSet ⟶ K) ≃ K _[0].

Equations

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