gen_d
plain-language theorem explainer
The boundary of a generator simplex equals the alternating sum of the generators of its faces. Anyone computing singular boundaries on the coproduct presentation of chain groups cites this identity. The proof unfolds the alternating-face differential and reduces each summand to a face-index map on generators.
Claim. For a topological space $X$, degree $n\in\mathbb{N}$, and singular $(n+1)$-simplex $a$, the composite of the generator map of $a$ with the singular boundary $C_{n+1}(X)\to C_n(X)$ equals $\sum_{k=0}^{n+1}(-1)^k$ times the generator of the $k$-th face of $a$.
background
Singular chains are presented as coproducts of $\mathbb{Z}$ indexed by singular simplices. Idx X n is the set of singular $n$-simplices of $X$ (maps $\Delta^n\to X$). The generator attached to a simplex $a$ is the coproduct inclusion of that summand into the degree-$n$ chain group. The boundary bnd X n is the differential of the alternating-face-map complex of the singular simplicial set of $X$.
This module builds prism operators and chain homotopies for continuous homotopies, so boundaries must act explicitly on generators. The classical formula $\partial\sigma=\sum_k(-1)^k\sigma\circ\delta_k$ is exactly what is needed before any prism or Mayer–Vietoris computation can leave the generators.
proof idea
Rewrite the left-hand side as the generator composed with the alternating-face differential of the singular complex. Expand that differential via AlternatingFaceMapComplex.obj_d_eq, push the composite through the finite sum (Preadditive.comp_sum), and treat each summand separately. For fixed face index $k$, pull the scalar $(-1)^k$ out (Preadditive.comp_zsmul) and identify the remaining arrow as the coproduct map induced by the face operator $\delta_k$. The identity Sigma.ι_comp_map' plus Category.id_comp finishes each summand.
why it matters
This is the workhorse boundary-on-generators lemma for the whole singular-homology stack in the Foundation layer. Downstream it feeds the prism chain-homotopy identities in positive degree and degree zero (prism_chain_homotopy_succ, prism_chain_homotopy_zero), which in turn underwrite that homotopy equivalences induce isomorphisms on singular homology. It is also used for path-simplex boundaries on spheres (gen_pathSimplex_bnd), partial augmentations killing boundaries, Mayer–Vietoris intertwining of small and singular boundaries, and subdivision commutation with boundary.
In the Recognition framework this is pure algebraic-topology scaffolding: it does not invoke J-cost, $\phi$, or the forcing chain, but it supplies the chain-level control needed wherever singular homology appears as a topological invariant of recognition spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.