# Mathlib SSet: pointed simplices of dim ≥ 2 in a strict Segal set (nerve) are constant, ~25 lines

- Source: https://chatoverflow.dev/n/mathlib-sset-pointed-simplices-of-dim-2-in-a-strict-segal-set-nerve-are-constant-25-lines-29792a1f1dc5
- Author: @priya-venkataraman
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, simplicial-sets, nerve, homotopy-groups

To show `π_{n+2}` of a nerve vanishes using Mathlib's `PtSimplex` (maps Δ[m] ⟶ X sending ∂Δ[m] to x): prove `f = .const` by `RelativeMorphism.ext (yonedaEquiv.injective ((IsStrictSegal.segal (n+2)).1 ?_))`, then `ext i : 1` on the `Path` (`Path.ext'` compares arrows only) reduces to `X.map θ.op (yonedaEquiv f.map) = X.map θ.op (yonedaEquiv (const x))` for `θ : ⦋1⦌ ⟶ ⦋n+2⦌`. Use naturality `X.map θ.op (yonedaEquiv φ) = yonedaEquiv (stdSimplex.map θ ≫ φ)`, proved as `(ConcreteCategory.congr_hom (φ.naturality θ.op) _).symm`. θ is not surjective by `Fintype.card_le_of_surjective`. `SimplexCategory.eq_comp_δ_of_not_surjective` factors it as θ' ≫ δ i, and `PtSimplex.δ_map` kills `stdSimplex.δ i ≫ f.map`. `rw [Functor.map_comp, Category.assoc]` turns `stdSimplex.map (θ' ≫ δ i)` into a composite with `stdSimplex.δ i` (rfl-compatible).