cons_comp_succAbove_succ
plain-language theorem explainer
Prepending a vertex and then taking the face that skips index j+1 equals prepending that vertex to the j-th face of the remaining simplex. Algebraic topologists cite it when assembling the cone boundary formula on augmented chains. The proof is pointwise on Fin, by cases on the zero and successor indices with the standard Fin face lemmas.
Claim. For any $b \in \alpha$, any $w : \mathrm{Fin}(n+1) \to \alpha$, and any $j \in \mathrm{Fin}(n+1)$, $$ (b \mathbin{::} w) \circ \delta^{j+1} = b \mathbin{::} (w \circ \delta^{j}), $$ where $\delta^{k} = \mathrm{succAbove}\,k$ is the order-preserving face embedding that skips index $k$, and $b \mathbin{::} w$ is the map sending $0$ to $b$ and $i+1$ to $w(i)$.
background
The module builds singular subdivision and cone operators on free abelian groups of abstract simplices. An abstract simplex is a map from a finite ordinal into a vertex set $\alpha$; the face operators are the standard embeddings $\mathrm{succAbove},j : \mathrm{Fin},n \to \mathrm{Fin}(n+1)$ that skip coordinate $j$. Prepending a vertex $b$ is $\mathrm{Fin.cons},b$, which builds the geometric cone with apex $b$.
Augmented chain groups $\mathrm{AC},\alpha,n$ and the boundary $\partial$ (written $\mathrm{abnd}$) and cone $\mathrm{acone},b$ maps live one layer up. The present identity is the combinatorial engine for how faces interact with that cone: the $(j+1)$-st face of a cone is the cone on the $j$-th face. A sibling lemma handles the $0$-th face separately.
The surrounding Stage 2 block targets the classical cone identity $\partial(b\cdot c)=c-b\cdot(\partial c)$ in positive degrees.
proof idea
Pointwise equality of functions $\mathrm{Fin}(n+1)\to\alpha$. Apply function extensionality, then induct on the argument $k$ via $\mathrm{Fin.cases}$.
- On $k=0$: reduce with $\mathrm{succ_succAbove_zero}$ and $\mathrm{cons_zero}$.
- On $k=\mathrm{succ},k'$: reduce with $\mathrm{succ_succAbove_succ}$ and $\mathrm{cons_succ}$.
Each branch is a one-line simp only against the Mathlib Fin API; no further lemmas from the monolith are required.
why it matters
Direct input to abnd_comp_acone, which states the cone identity in positive degrees: $\partial(b\cdot c)=c-b\cdot(\partial c)$ for $c:\mathrm{AC},\alpha,(n+1)$. That identity is the algebraic heart of the singular cone and subdivision package imported from Mathlib's singular homology API.
In the Recognition foundation stack this sits under SingularSubdivision / SingularPrism: it supplies the face-by-face bookkeeping needed so that cone and boundary commute in the free $\mathbb{Z}$-module of abstract simplices. It is pure Fin combinatorics, not a physics claim, but without it the chain-level cone formula does not typecheck. No forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked; the lemma is infrastructure for later geometric arguments that may feed those layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.