cons_comp_succAbove_zero
plain-language theorem explainer
Prepending a base point b to an (n+1)-tuple w and then composing with the face map that skips vertex 0 recovers w exactly. Algebraic topologists working the cone operator on abstract chains cite this when expanding the 0-face term of ∂(b·c). The proof is a one-line funext plus the standard Fin.succAbove/cons simplification lemmas.
Claim. For any base value $b\in\alpha$ and any map $w:\mathrm{Fin}(n+1)\to\alpha$, the composite $(\mathrm{cons}\,b\,w)\circ\mathrm{succAbove}(0)$ equals $w$. Equivalently, the $0$-th face of the cone on $w$ with apex $b$ is the base tuple $w$ itself.
background
The module builds an abstract chain complex $AC,\alpha,n$ of free $\mathbb{Z}$-modules on $(n+1)$-tuples valued in a type $\alpha$, together with a cone operator $b\cdot(-)$ that adjoins a fixed apex $b$ and a boundary $abnd$. Faces of cones are realized combinatorially by prepending the apex via $\mathrm{Fin.cons}$ and then applying the vertex-skipping maps $\mathrm{Fin.succAbove},j$.
Upstream, $\mathrm{SingularPrism.face}$ realizes the topological face inclusion $\Delta^n\to\Delta^{n+1}$ by the same $\mathrm{succAbove}$ vertex map, and the circle-winding face operator is the singular analogue $F\circ\mathrm{faceMap},i$. The present lemma is the pure Fin-level identity that makes the $0$-face of a cone equal the base, which is the combinatorial content of the classical cone formula $\partial(b\cdot c)=c-b\cdot(\partial c)$.
Local notation: $\mathrm{asimplex},w$ is the generator for tuple $w$, $\mathrm{acone},b$ is the linear cone map, and $\mathrm{abnd}$ is the alternating face-sum boundary.
proof idea
Term-mode proof by function extensionality on the domain $\mathrm{Fin}(n+1)$. After $\mathrm{funext},k$, a single $\mathrm{simp}$ closes the goal using $\mathrm{Function.comp_apply}$, the identity $\mathrm{Fin.zero_succAbove}$ (skipping $0$ sends $k$ to $k+1$), and $\mathrm{Fin.cons_succ}$ (cons then looking at a successor index recovers the original tuple entry). No induction or case split is required.
why it matters
The lemma is the $0$-face half of the cone calculus used to prove the two cone identities in this module. Downstream, $\mathrm{abnd_comp_acone}$ states $\partial(b\cdot c)=c-b\cdot(\partial c)$ in positive degree, and $\mathrm{abnd_comp_acone_zero}$ states the degree-$0$ form $\partial(b\cdot c)=c-\varepsilon(c)\cdot[b]$. Both proofs expand the face sum of a cone and invoke this identity on the $j=0$ term so that the base appears with coefficient $+1$.
In the Recognition foundation layer these cone identities supply the algebraic homotopy that contracts the abstract singular complex, which is the chain-level input to the forcing and subdivision arguments that sit under the eight-tick and dimension-forcing steps. Without the Fin identity the boundary expansion does not cancel cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.