coe_succAbove
plain-language theorem explainer
When embedding an n-simplex vertex index into dimension n+1 by skipping a fixed slot p, the underlying natural number is i if i < p and i+1 otherwise. Prism and sphere face lemmas cite this to reduce Fin-index bookkeeping to ordinary ℕ comparisons. Proof is a two-branch case split on i < p, rewriting with the matching Fin.succAbove clauses and simplifying.
Claim. For $n\in\mathbb{N}$, $p\in\mathrm{Fin}(n+1)$ and $i\in\mathrm{Fin}\,n$, the coercion of $\mathrm{succAbove}(p,i)$ to $\mathbb{N}$ equals $i$ if $i<p$ and equals $i+1$ otherwise.
background
The module builds continuous prism maps on standard simplices, the geometric ingredient of the prism operator $P$ in singular homology. Faces of an $(n+1)$-simplex are induced by the order-preserving embeddings $\mathrm{succAbove},p:\mathrm{Fin},n\to\mathrm{Fin}(n+1)$, which insert a gap at coordinate $p$ (skipping that vertex index).
Working with those maps pointwise requires knowing the underlying natural number of $\mathrm{succAbove},p,i$. That value is the identity below the gap and a unit shift above it. The local arithmetic of $\le$ and $<$ on the coerced indices is the only comparison data needed; the proof routes those comparisons through the standard Fin order characterizations.
Sibling lemmas (coe_predAbove, face, prism) package the dual gap-insertion and the continuous maps built from them.
proof idea
Case-split on the proposition $(i:\mathbb{N})<(p:\mathbb{N})$.
- If true, rewrite with
Fin.succAbove_of_castSucc_lt, discharging the order hypothesis bysimpaagainstFin.lt_def, thensimpwith the true branch of theif. - If false, rewrite with
Fin.succAbove_of_le_castSucc, discharging vianot_lt.mpandFin.le_def, thensimpwith the false branch.
No further induction or arithmetic is required; the two library clauses for succAbove already match the piecewise definition.
why it matters
This is pure index plumbing, but every prism–face identity in the module depends on it. Downstream it is used by prism_comp_face_top and prism_comp_face_bot (top and bottom of the prism equal the constant-height sections), by prism_comp_face_cancel (adjacent prism maps agree on the shared face, the cancelling terms of $\partial P$), and by the high/low face commutation lemmas prism_comp_face_of_gt and prism_comp_face_of_le that match $(i,j)$ terms of $\partial P$ against $P\partial$.
Outside the prism file it feeds coord_face_v0 in SingularSphere and abnd_comp_abnd in SingularSubdivision, so the same coercion fact underwrites sphere-coordinate and barycentric-subdivision calculations. In the Recognition foundation stack these identities are the concrete simplicial algebra behind continuous homotopies; they do not themselves invoke the forcing chain (T0–T8) or the J-cost, but they sit in the singular-homology layer that later supports topological arguments in that stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.