sBnd
plain-language theorem explainer
Defines the boundary operator on the small singular chain groups relative to a pair of subsets U, V: on each generator it is the usual alternating sum of faces. Faces of small simplices remain small, so the map lands in the small n-chains. Anyone assembling the small-chain complex or the Mayer–Vietoris comparison cites this. The body is a coproduct descent that writes the classical formula on generators.
Claim. For subsets $U,V\subseteq X$ and $n\in\mathbb{N}$, the small boundary $\partial^{U,V}_n:C^{U,V}_{n+1}(X)\to C^{U,V}_n(X)$ is the $\mathbb{Z}$-linear map determined on the generator of a small singular $(n+1)$-simplex $\sigma$ by $\partial^{U,V}_n(\sigma)=\sum_{k=0}^{n+1}(-1)^k\,\sigma\circ\delta_k$, where each face $\sigma\circ\delta_k$ is again small.
background
In singular homology one often restricts to simplices that land in a prescribed open cover. Here a singular $n$-simplex of $X$ is small relative to $U,V$ when its image lies entirely in $U$ or entirely in $V$. The degree-$n$ small chain group $C^{U,V}_n(X)$ is the free $\mathbb{Z}$-module on those small simplices, realized as a coproduct of copies of $\mathbb{Z}$.
The generator map sends the unit of the copy indexed by a small simplex $t$ to the corresponding basis element. Faces of small simplices remain small (the range of a face sits inside the range of the original simplex), so the classical face operators restrict to the small indexing set.
The ambient module is the ordinary singular chain complex of $X$; the small groups sit inside it by the inclusion of generators. This module builds the small subcomplex used for Mayer–Vietoris comparisons.
proof idea
Definition by the universal property of the coproduct: Sigma.desc specifies a map out of $C^{U,V}_{n+1}$ by giving, for each small $(n+1)$-simplex $t$, a morphism $\mathbb{Z}\to C^{U,V}n$. That morphism is the integer linear combination $\sum{k:\mathrm{Fin}(n+2)}(-1)^k\cdot$ (generator of the $k$-th face of $t$). The face is packaged as a small index via Small.δ, so the target generator is well-typed. No further lemmas are invoked in the body.
why it matters
This is the differential of Stage 1 of the singular Mayer–Vietoris setup: the small-chains complex is assembled as ChainComplex.of on the small groups with this boundary and the identity $\partial\circ\partial=0$. Downstream, sBnd_comp_sBnd proves the square vanishes by transporting across the inclusion into ordinary singular chains and using $d\circ d=0$ there; sBnd_comp_sInc says the inclusion intertwines small and ordinary boundaries.
Those facts feed the injectivity and surjectivity inputs (small_inj, small_surj_succ) that compare small homology to singular homology when $U\cup V=X$ are open. In the Recognition Science foundation this is pure algebraic topology scaffolding: it supplies the chain-level language for cover arguments, not a forcing-chain step (T0–T8) or a physical constant identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.