Theorems · Definition · algebraic topology

SSet.Nonsingular.iso

{X : SSet} →
  [X.Nonsingular] →
    {n : ℕ} →
      (x : X.obj (Opposite.op { len := n })) →
        x ∈ X.nonDegenerate n → (SSet.stdSimplex.obj { len := n } ≅ (SSet.Subcomplex.ofSimplex x).toSSet)

If x : X _⦋n⦌ is a nondegenerate simplex of a nonsingular simplicial set, this is the isomorphism Δ[n] ≅ Subcomplex.ofSimplex x induced by x.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Cited by

2 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SSet.Nonsingular