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].
noncomputable def
SSet.prodStdSimplex.nonDegenerateEquiv₁
{p : ℕ}
:
Fin (p + 1) ≃ ↑((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p))
(stdSimplex.obj (SimplexCategory.mk 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).
Instances For
@[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