Documentation

Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne

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].

source
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).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SSet.prodStdSimplex.nonDegenerateEquiv₁_fst {p : ℕ} (i : Fin (p + 1)) :
    (↑(nonDegenerateEquiv₁ i)).1 = stdSimplex.objEquiv.symm (SimplexCategory.σ i)
    source
    @[simp]
    theorem SSet.prodStdSimplex.nonDegenerateEquiv₁_snd {p : ℕ} (i : Fin (p + 1)) :
    (↑(nonDegenerateEquiv₁ i)).2 = stdSimplex.objMk₁ i.castSucc.succ