Binary products Δ[n] ⊗ Δ[1]

In this file, we define a bijection SSet.prodStdSimplex₁.nonDegenerateEquiv between Fin (p + 1) and the type of nondegenerate (p + 1)-simplices of Δ[p] ⊗ Δ[1]. We use this enumeration of the nondegenerate simplices in order to define a filtration SSet.prodStdSimplex₁.filtration of Δ[p] ⊗ Δ[1] by subcomplexes.

noncomputable def SSet.prodStdSimplex₁.nonDegenerateEquiv {p : ℕ} : Fin (p + 1) ≃ ↑((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p }) (stdSimplex.obj { len := 1 })).nonDegenerate (p + 1))

This is an enumeration of the p + 1 nondegenerate dimension-(p + 1) simplices of Δ[p] ⊗ Δ[1]. It sends i : Fin (p + 1) to the nondegenerate simplex consisting of the vertices (0, 0) ≤ (1,0) ≤ ... ≤ (i, 0) ≤ (i, 1) ≤ ... ≤ (p, 1).

Equations

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

@[simp]

theorem SSet.prodStdSimplex₁.nonDegenerateEquiv_fst {p : ℕ} (i : Fin (p + 1)) : (↑(nonDegenerateEquiv i)).1 = stdSimplex.objEquiv.symm (SimplexCategory.σ i)

@[simp]

theorem SSet.prodStdSimplex₁.nonDegenerateEquiv_snd {p : ℕ} (i : Fin (p + 1)) : (↑(nonDegenerateEquiv i)).2 = stdSimplex.objMk₁ i.castSucc.succ

noncomputable def SSet.prodStdSimplex₁.filtration {p : ℕ} (j : Fin (p + 1)) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p }) (stdSimplex.obj { len := 1 })).Subcomplex

The filtration of Δ[p] ⊗ Δ[1] which sends j : Fin (p + 1) to the subcomplex generated by the non-degenerate (p + 1)-simplices nonDegenerateEquiv i for i ≤ j.

Equations

• SSet.prodStdSimplex₁.filtration j = ⨆ (i : ↑(Set.Iic j)), SSet.Subcomplex.ofSimplex ↑(SSet.prodStdSimplex₁.nonDegenerateEquiv ↑i)

theorem SSet.prodStdSimplex₁.ofSimplex_le_filtration {p : ℕ} {i j : Fin (p + 1)} (hij : i ≤ j) : Subcomplex.ofSimplex ↑(nonDegenerateEquiv i) ≤ filtration j

theorem SSet.prodStdSimplex₁.filtration_zero (p : ℕ) : filtration 0 = Subcomplex.ofSimplex ↑(nonDegenerateEquiv 0)

theorem SSet.prodStdSimplex₁.filtration_last (p : ℕ) : filtration (Fin.last p) = ⊤

theorem SSet.prodStdSimplex₁.filtration_monotone {p : ℕ} : Monotone filtration

@[reducible, inline]

noncomputable abbrev SSet.prodStdSimplex₁.intersectionNondeg {p : ℕ} (i j : Fin (p + 1)) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p }) (stdSimplex.obj { len := 1 })).Subcomplex

Given i and j in Fin (p + 1), this is the subcomplex of Δ[p] ⊗ Δ[1] obtained as the intersection of the subcomplexes generated by the ith and jth p + 1-dimensional non-degenerate simplices given by the enumeration prodStdSimplex₁.nonDegenerateEquiv.

Equations

• SSet.prodStdSimplex₁.intersectionNondeg i j = SSet.Subcomplex.ofSimplex ↑(SSet.prodStdSimplex₁.nonDegenerateEquiv i) ⊓ SSet.Subcomplex.ofSimplex ↑(SSet.prodStdSimplex₁.nonDegenerateEquiv j)

def SSet.prodStdSimplex₁.codimOneSimplex {p : ℕ} (j : Fin (p + 2)) : ↑((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p }) (stdSimplex.obj { len := 1 })).nonDegenerate p)

Given j : Fin (p + 2), this is the non-degenerate p-simplex of Δ[p] ⊗ Δ[1] which correspond to the stricly monotone map Fin (p + 1) → Fin (p + 1) × Fin 2 whose first projection is the identity, and whose second projection takes j-times the value 0.

Equations

• SSet.prodStdSimplex₁.codimOneSimplex j = ⟨(SSet.stdSimplex.objMk OrderHom.id, SSet.stdSimplex.objMk₁ j), ⋯⟩

@[simp]

theorem SSet.prodStdSimplex₁.codimOneSimplex_coe_fst {p : ℕ} (j : Fin (p + 2)) : (↑(codimOneSimplex j)).1 = stdSimplex.objMk OrderHom.id

@[simp]

theorem SSet.prodStdSimplex₁.codimOneSimplex_coe_snd {p : ℕ} (j : Fin (p + 2)) : (↑(codimOneSimplex j)).2 = stdSimplex.objMk₁ j

theorem SSet.prodStdSimplex₁.δ_castSucc_nonDegenerateEquiv {p : ℕ} (j : Fin (p + 1)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p }) (stdSimplex.obj { len := 1 })) j.castSucc)) ↑(nonDegenerateEquiv j) = ↑(codimOneSimplex j.castSucc)

theorem SSet.prodStdSimplex₁.δ_succ_nonDegenerateEquiv {p : ℕ} (j : Fin (p + 1)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p }) (stdSimplex.obj { len := 1 })) j.succ)) ↑(nonDegenerateEquiv j) = ↑(codimOneSimplex j.succ)

@[deprecated SSet.prodStdSimplex₁.nonDegenerateEquiv (since := "2026-08-13")]

def SSet.prodStdSimplex.nonDegenerateEquiv₁ {p : ℕ} : Fin (p + 1) ≃ ↑((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p }) (stdSimplex.obj { len := 1 })).nonDegenerate (p + 1))

Alias of SSet.prodStdSimplex₁.nonDegenerateEquiv.

---

This is an enumeration of the p + 1 nondegenerate dimension-(p + 1) simplices of Δ[p] ⊗ Δ[1]. It sends i : Fin (p + 1) to the nondegenerate simplex consisting of the vertices (0, 0) ≤ (1,0) ≤ ... ≤ (i, 0) ≤ (i, 1) ≤ ... ≤ (p, 1).

Equations

• @SSet.prodStdSimplex.nonDegenerateEquiv₁ = @SSet.prodStdSimplex₁.nonDegenerateEquiv

@[deprecated SSet.prodStdSimplex₁.nonDegenerateEquiv_fst (since := "2026-08-13")]

theorem SSet.prodStdSimplex.nonDegenerateEquiv₁_fst {p : ℕ} (i : Fin (p + 1)) : (↑(prodStdSimplex₁.nonDegenerateEquiv i)).1 = stdSimplex.objEquiv.symm (SimplexCategory.σ i)

Alias of SSet.prodStdSimplex₁.nonDegenerateEquiv_fst.

@[deprecated SSet.prodStdSimplex₁.nonDegenerateEquiv_snd (since := "2026-08-13")]

theorem SSet.prodStdSimplex.nonDegenerateEquiv₂_snd {p : ℕ} (i : Fin (p + 1)) : (↑(prodStdSimplex₁.nonDegenerateEquiv i)).2 = stdSimplex.objMk₁ i.castSucc.succ

Alias of SSet.prodStdSimplex₁.nonDegenerateEquiv_snd.