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.

@[simp]

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

@[simp]

theorem SSet.leftUnitor_inv_app_apply (K : SSet) {Δ : SimplexCategoryᵒᵖ} (x : K.obj Δ) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor (K.obj Δ)).inv) 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.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor (K.obj Δ)).hom) x = x.1

@[simp]

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

def SSet.unitHomEquiv (K : SSet) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet ⟶ K) ≃ K.obj (Opposite.op { len := 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 { len := 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 { len := 0 }} : f = g

theorem SSet.stdSimplex.ext₀_iff {X : SSet} {f g : X ⟶ stdSimplex.obj { len := 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)

instance SSet.instFiniteTensorUnit : (CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet).Finite

instance SSet.instHasDimensionLETensorUnitOfNatNat : (CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet).HasDimensionLE 0

@[instance_reducible]

instance SSet.instMonoidalOpFunctor : opFunctor.Monoidal

Equations

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

def SSet.Subcomplex.prod {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).Subcomplex

The external product of subcomplexes of simplicial sets.

Equations

• A.prod B = { obj := fun (Δ : SimplexCategoryᵒᵖ) => A.obj Δ ×ˢ B.obj Δ, map := ⋯ }

@[simp]

theorem SSet.Subcomplex.prod_obj {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) (Δ : SimplexCategoryᵒᵖ) : (A.prod B).obj Δ = A.obj Δ ×ˢ B.obj Δ

theorem SSet.Subcomplex.prod_monotone {X Y : SSet} {A₁ A₂ : X.Subcomplex} (hX : A₁ ≤ A₂) {B₁ B₂ : Y.Subcomplex} (hY : B₁ ≤ B₂) : A₁.prod B₁ ≤ A₂.prod B₂

theorem SSet.Subcomplex.prod_le_top_prod {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) : A.prod B ≤ ⊤.prod B

theorem SSet.Subcomplex.prod_le_prod_top {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) : A.prod B ≤ A.prod ⊤

theorem SSet.Subcomplex.range_tensorHom {X₁ X₂ Y₁ Y₂ : SSet} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) : range (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) = (range f₁).prod (range f₂)

def SSet.Subcomplex.prodIso {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) : (A.prod B).toSSet ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj A.toSSet B.toSSet

The isomorphism (A.prod B).toSSet ≅ A.toSSet ⊗ B.toSSet.

Equations

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

@[simp]

theorem SSet.Subcomplex.prodIso_inv {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) : (A.prodIso B).inv = lift (CategoryTheory.MonoidalCategoryStruct.tensorHom A.ι B.ι) ⋯

@[simp]

theorem SSet.Subcomplex.prodIso_hom {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) : (A.prodIso B).hom = CategoryTheory.CartesianMonoidalCategory.lift (lift (CategoryTheory.CategoryStruct.comp (A.prod B).ι (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) ⋯) (lift (CategoryTheory.CategoryStruct.comp (A.prod B).ι (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) ⋯)

noncomputable def SSet.ι₀ {X : SSet} : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X (stdSimplex.obj { len := 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 { len := 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 { len := 1 }) ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (stdSimplex.obj { len := 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 { len := 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 { len := 1 })) h) = h

@[simp]

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

@[simp]

theorem SSet.ι₀_snd_assoc (X : SSet) {Z : SSet} (h : stdSimplex.obj { len := 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X (stdSimplex.obj { len := 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) : ((CategoryTheory.ConcreteCategory.hom (ι₀.app m)) x).1 = x

@[simp]

theorem SSet.ι₀_app_snd_apply {X : SSet} {m : ℕ} (x : X.obj (Opposite.op { len := m })) (k : Fin (m + 1)) : ((CategoryTheory.ConcreteCategory.hom (ι₀.app (Opposite.op { len := m }))) x).2 k = 0

noncomputable def SSet.ι₁ {X : SSet} : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X (stdSimplex.obj { len := 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 { len := 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 { len := 1 })) h) = h

@[simp]

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

@[simp]

theorem SSet.ι₁_snd_assoc (X : SSet) {Z : SSet} (h : stdSimplex.obj { len := 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X (stdSimplex.obj { len := 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 { len := 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 { len := 1 }) ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (stdSimplex.obj { len := 1 })) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ι₁ h)

@[simp]

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

@[simp]

theorem SSet.ι₁_app_snd_apply {X : SSet} {m : ℕ} (x : X.obj (Opposite.op { len := m })) (k : Fin (m + 1)) : ((CategoryTheory.ConcreteCategory.hom (ι₁.app (Opposite.op { len := m }))) x).2 k = 1

@[simp]

theorem SSet.prod_map_fst (X Y : SSet) {m n : SimplexCategoryᵒᵖ} (f : m ⟶ n) (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj m) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.map f) (Y.map f))) z).1 = (CategoryTheory.ConcreteCategory.hom (X.map f)) z.1

@[simp]

theorem SSet.prod_map_snd (X Y : SSet) {m n : SimplexCategoryᵒᵖ} (f : m ⟶ n) (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj m) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.map f) (Y.map f))) z).2 = (CategoryTheory.ConcreteCategory.hom (Y.map f)) z.2

@[simp]

theorem SSet.prod_δ_fst (X Y : SSet) {n : ℕ} (i : Fin (n + 2)) (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj (Opposite.op { len := n + 1 })) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i)) z).1 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) z.1

@[simp]

theorem SSet.prod_δ_snd (X Y : SSet) {n : ℕ} (i : Fin (n + 2)) (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj (Opposite.op { len := n + 1 })) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i)) z).2 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Y i)) z.2

@[simp]

theorem SSet.prod_σ_fst (X Y : SSet) {n : ℕ} (i : Fin (n + 1)) (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj (Opposite.op { len := n })) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i)) z).1 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X i)) z.1

@[simp]

theorem SSet.prod_σ_snd (X Y : SSet) {n : ℕ} (i : Fin (n + 1)) (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj (Opposite.op { len := n })) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i)) z).2 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ Y i)) z.2

def SSet.Subcomplex.unionProd {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).Subcomplex

Given S ≤ X and T ≤ Y, this is the subcomplex of X ⊗ Y given by (X ⊗ T) ⊔ (S ⊗ Y).

Equations

• S.unionProd T = ⊤.prod T ⊔ S.prod ⊤

theorem SSet.Subcomplex.mem_unionProd_iff {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj n) : x ∈ (S.unionProd T).obj n ↔ x.2 ∈ T.obj n ∨ x.1 ∈ S.obj n

theorem SSet.Subcomplex.top_prod_le_unionProd {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : ⊤.prod T ≤ S.unionProd T

theorem SSet.Subcomplex.prod_top_le_unionProd {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : S.prod ⊤ ≤ S.unionProd T

theorem SSet.Subcomplex.prod_le_unionProd {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : S.prod T ≤ S.unionProd T

theorem SSet.Subcomplex.preimage_op_unionProd {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (S.unionProd T).op.preimage (CategoryTheory.Functor.LaxMonoidal.μ opFunctor X Y) = S.op.unionProd T.op

theorem SSet.Subcomplex.preimage_unionProd {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) {X' Y' : SSet} (f : X' ⟶ X) (g : Y' ⟶ Y) : (S.unionProd T).preimage (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = (S.preimage f).unionProd (T.preimage g)

noncomputable def SSet.Subcomplex.unionProd.ι₁ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : CategoryTheory.MonoidalCategoryStruct.tensorObj X T.toSSet ⟶ (S.unionProd T).toSSet

The inclusion X ⊗ T ⟶ S.unionProd T as simplicial sets.

Equations

• SSet.Subcomplex.unionProd.ι₁ S T = SSet.Subcomplex.lift (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X T.ι) ⋯

noncomputable def SSet.Subcomplex.unionProd.ι₂ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : CategoryTheory.MonoidalCategoryStruct.tensorObj S.toSSet Y ⟶ (S.unionProd T).toSSet

The inclusion S ⊗ Y ⟶ S.unionProd T as simplicial sets

Equations

• SSet.Subcomplex.unionProd.ι₂ S T = SSet.Subcomplex.lift (CategoryTheory.MonoidalCategoryStruct.whiskerRight S.ι Y) ⋯

@[simp]

theorem SSet.Subcomplex.unionProd.ι₁_ι {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : CategoryTheory.CategoryStruct.comp (ι₁ S T) (S.unionProd T).ι = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X T.ι

@[simp]

theorem SSet.Subcomplex.unionProd.ι₁_ι_assoc {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) {Z : SSet} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (ι₁ S T) (CategoryTheory.CategoryStruct.comp (S.unionProd T).ι h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X T.ι) h

@[simp]

theorem SSet.Subcomplex.unionProd.ι₂_ι {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : CategoryTheory.CategoryStruct.comp (ι₂ S T) (S.unionProd T).ι = CategoryTheory.MonoidalCategoryStruct.whiskerRight S.ι Y

@[simp]

theorem SSet.Subcomplex.unionProd.ι₂_ι_assoc {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) {Z : SSet} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (ι₂ S T) (CategoryTheory.CategoryStruct.comp (S.unionProd T).ι h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight S.ι Y) h

theorem SSet.Subcomplex.unionProd.bicartSq {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (S.prod T).BicartSq (⊤.prod T) (S.prod ⊤) (S.unionProd T)

theorem SSet.Subcomplex.unionProd.isPushout {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : CategoryTheory.IsPushout (CategoryTheory.MonoidalCategoryStruct.whiskerRight S.ι T.toSSet) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft S.toSSet T.ι) (ι₁ S T) (ι₂ S T)

@[simp]

theorem SSet.Subcomplex.unionProd.preimage_β_hom {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (S.unionProd T).preimage (β_ Y X).hom = T.unionProd S

@[simp]

theorem SSet.Subcomplex.unionProd.preimage_β_inv {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (S.unionProd T).preimage (β_ X Y).inv = T.unionProd S

@[simp]

theorem SSet.Subcomplex.unionProd.image_β_hom {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (S.unionProd T).image (β_ X Y).hom = T.unionProd S

@[simp]

theorem SSet.Subcomplex.unionProd.image_β_inv {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (S.unionProd T).image (β_ Y X).inv = T.unionProd S

noncomputable def SSet.Subcomplex.unionProd.symmIso {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (S.unionProd T).toSSet ≅ (T.unionProd S).toSSet

The isomorphism unionProd S T ≅ unionProd T S as simplicial sets.

Equations

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

@[simp]

theorem SSet.Subcomplex.unionProd.symmIso_inv {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (symmIso S T).inv = lift (CategoryTheory.CategoryStruct.comp (T.unionProd S).ι (β_ Y X).hom) ⋯

@[simp]

theorem SSet.Subcomplex.unionProd.symmIso_hom {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (symmIso S T).hom = lift (CategoryTheory.CategoryStruct.comp (S.unionProd T).ι (β_ X Y).hom) ⋯

@[instance_reducible]

instance SSet.Truncated.instMonoidalTruncation (n : ℕ) : (truncation n).Monoidal

Equations

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

@[simp]

theorem SSet.Truncated.tensor_map_apply_fst {n : ℕ} {X Y : Truncated n} {d e : (SimplexCategory.Truncated n)ᵒᵖ} (f : d ⟶ e) (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj d) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.map f) (Y.map f))) x).1 = (CategoryTheory.ConcreteCategory.hom (X.map f)) x.1

@[simp]

theorem SSet.Truncated.tensor_map_apply_snd {n : ℕ} {X Y : Truncated n} {d e : (SimplexCategory.Truncated n)ᵒᵖ} (f : d ⟶ e) (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj d) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.map f) (Y.map f))) x).2 = (CategoryTheory.ConcreteCategory.hom (Y.map f)) x.2