SSC_d
plain-language theorem explainer
The differential of the small-chains subcomplex C^{U,V}_*(X) in degree n+1 → n is exactly the small boundary map sBnd. Anyone building chain maps into or out of the small-chains complex cites this to unpack the differential. The proof is a one-line application of the constructor identity for ChainComplex.of.
Claim. For every $n \in \mathbb{N}$, the differential $d_{n+1}$ of the small-chains subcomplex $C^{U,V}_*(X)$ equals the small boundary map $\partial^{U,V}_n : C^{U,V}_{n+1}(X) \to C^{U,V}_n(X)$.
background
This module builds the singular Mayer–Vietoris sequence for an open cover ${U,V}$ of a space $X$. Stage 1 isolates the small-chains subcomplex $C^{U,V}_*(X)$: integer chains generated by singular simplices whose image lies entirely in $U$ or entirely in $V$.
The object groups are the free modules sCgrp U V n on those small simplices. The boundary sBnd U V n is the usual alternating sum of faces; faces of small simplices remain small by the face-stability lemma Small.δ. The complex itself is assembled by ChainComplex.of from those groups, the family sBnd, and the identity sBnd ∘ sBnd = 0.
Once the complex exists, downstream chain maps need a concrete name for its differential. That is what this lemma supplies.
proof idea
One-line term proof. SSC is defined as ChainComplex.of (sCgrp U V) (sBnd U V) (sBnd_comp_sBnd U V), so the differential of the resulting complex is definitionally sBnd. The lemma is just the library identity ChainComplex.of_d applied to those four arguments.
why it matters
Without an explicit differential, no chain-map commutativity square can be stated. The inclusions smallU : C_*(U) → C^{U,V}_*(X) and smallV : C_*(V) → C^{U,V}_*(X) both rewrite with SSC_d in their comm' fields, as does the joint inclusion smallι and the subsequent isomorphism-on-homology statement smallι_isIso_homologyMap.
Those maps are the left half of the Mayer–Vietoris short exact sequence of chain complexes. In the Recognition foundation stack this is pure singular-homology scaffolding: it underwrites the topological forcing arguments that later pin dimension and the eight-tick octave, but the lemma itself is ordinary algebraic topology, not a physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.