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.

instance SSet.instCartesianMonoidalCategory : CategoryTheory.CartesianMonoidalCategory SSet

Equations

• SSet.instCartesianMonoidalCategory = inferInstance

instance SSet.instMonoidalClosed : CategoryTheory.MonoidalClosed SSet

Equations

• SSet.instMonoidalClosed = inferInstanceAs (CategoryTheory.MonoidalClosed (CategoryTheory.Functor SimplexCategoryᵒᵖ (Type ?u.5)))

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem SSet.rightUnitor_inv_app_apply (K : SSet) {Δ : SimplexCategoryᵒᵖ} (x : K.obj Δ) : (CategoryTheory.MonoidalCategoryStruct.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.MonoidalCategoryStruct.tensorObj K L).obj Δ) : (CategoryTheory.MonoidalCategoryStruct.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.MonoidalCategoryStruct.tensorObj K L).obj Δ) : (CategoryTheory.MonoidalCategoryStruct.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.MonoidalCategoryStruct.tensorObj K L).obj Δ) : (CategoryTheory.MonoidalCategoryStruct.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.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj K L) M).obj Δ) : (CategoryTheory.MonoidalCategoryStruct.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.MonoidalCategoryStruct.tensorObj K (CategoryTheory.MonoidalCategoryStruct.tensorObj L M)).obj Δ) : (CategoryTheory.MonoidalCategoryStruct.associator K L M).inv.app Δ x = ((x.1, x.2.1), x.2.2)

def SSet.unitHomEquiv (K : SSet) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit 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.

def SSet.stdSimplex.isTerminalObj₀ : CategoryTheory.Limits.IsTerminal (stdSimplex.obj (SimplexCategory.mk 0))

The object Δ[0] is terminal in SSet.

Equations

• SSet.stdSimplex.isTerminalObj₀ = CategoryTheory.Limits.IsTerminal.ofUniqueHom (fun (x : SSet) => SSet.const (SSet.stdSimplex.obj₀Equiv.symm 0)) ⋯

theorem SSet.stdSimplex.ext₀ {X : SSet} {f g : X ⟶ stdSimplex.obj (SimplexCategory.mk 0)} : f = g

theorem SSet.stdSimplex.ext₀_iff {X : SSet} {f g : X ⟶ stdSimplex.obj (SimplexCategory.mk 0)} : f = g ↔ True

instance SSet.instFiniteObjOppositeSimplexCategoryTensorObj (X Y : SSet) (n : SimplexCategoryᵒᵖ) [Finite (X.obj n)] [Finite (Y.obj n)] : Finite ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj n)

noncomputable def SSet.ι₀ {X : SSet} : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X (stdSimplex.obj (SimplexCategory.mk 1))

The inclusion X ⟶ X ⊗ Δ[1] which is 0 on the second factor.

Equations

• SSet.ι₀ = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) (SSet.const (SSet.stdSimplex.obj₀Equiv.symm 0))

@[simp]

theorem SSet.ι₀_comp {X Y : SSet} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (stdSimplex.obj (SimplexCategory.mk 1))) = CategoryTheory.CategoryStruct.comp f ι₀

@[simp]

theorem SSet.ι₀_comp_assoc {X Y : SSet} (f : X ⟶ Y) {Z : SSet} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y (stdSimplex.obj (SimplexCategory.mk 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (stdSimplex.obj (SimplexCategory.mk 1))) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ι₀ h)

@[simp]

theorem SSet.ι₀_fst (X : SSet) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.SemiCartesianMonoidalCategory.fst X (stdSimplex.obj (SimplexCategory.mk 1))) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem SSet.ι₀_fst_assoc (X : SSet) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X (stdSimplex.obj (SimplexCategory.mk 1))) h) = h

@[simp]

theorem SSet.ι₀_snd (X : SSet) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.SemiCartesianMonoidalCategory.snd X (stdSimplex.obj (SimplexCategory.mk 1))) = const (stdSimplex.obj₀Equiv.symm 0)

@[simp]

theorem SSet.ι₀_snd_assoc (X : SSet) {Z : SSet} (h : stdSimplex.obj (SimplexCategory.mk 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X (stdSimplex.obj (SimplexCategory.mk 1))) h) = CategoryTheory.CategoryStruct.comp (const (stdSimplex.obj₀Equiv.symm 0)) h

@[simp]

theorem SSet.ι₀_app_fst {X : SSet} {m : SimplexCategoryᵒᵖ} (x : X.obj m) : (ι₀.app m x).1 = x

noncomputable def SSet.ι₁ {X : SSet} : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X (stdSimplex.obj (SimplexCategory.mk 1))

The inclusion X ⟶ X ⊗ Δ[1] which is 1 on the second factor.

Equations

• SSet.ι₁ = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) (SSet.const (SSet.stdSimplex.obj₀Equiv.symm 1))

@[simp]

theorem SSet.ι₁_fst (X : SSet) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.SemiCartesianMonoidalCategory.fst X (stdSimplex.obj (SimplexCategory.mk 1))) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem SSet.ι₁_fst_assoc (X : SSet) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X (stdSimplex.obj (SimplexCategory.mk 1))) h) = h

@[simp]

theorem SSet.ι₁_snd (X : SSet) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.SemiCartesianMonoidalCategory.snd X (stdSimplex.obj (SimplexCategory.mk 1))) = const (stdSimplex.obj₀Equiv.symm 1)

@[simp]

theorem SSet.ι₁_snd_assoc (X : SSet) {Z : SSet} (h : stdSimplex.obj (SimplexCategory.mk 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X (stdSimplex.obj (SimplexCategory.mk 1))) h) = CategoryTheory.CategoryStruct.comp (const (stdSimplex.obj₀Equiv.symm 1)) h

@[simp]

theorem SSet.ι₁_comp {X Y : SSet} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (stdSimplex.obj (SimplexCategory.mk 1))) = CategoryTheory.CategoryStruct.comp f ι₁

@[simp]

theorem SSet.ι₁_comp_assoc {X Y : SSet} (f : X ⟶ Y) {Z : SSet} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y (stdSimplex.obj (SimplexCategory.mk 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (stdSimplex.obj (SimplexCategory.mk 1))) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ι₁ h)

@[simp]

theorem SSet.ι₁_app_fst {X : SSet} {m : SimplexCategoryᵒᵖ} (x : X.obj m) : (ι₁.app m x).1 = x