SSC_X
plain-language theorem explainer
The degree-n object of the small-chains subcomplex equals the free ℤ-module on small singular n-simplices in U or V. Anyone rewriting against the Stage-1 Mayer–Vietoris chain complex cites this as a simp fact. The proof is pure definitional equality from ChainComplex.of.
Claim. For every $n \in \mathbb{N}$, the degree-$n$ term of the small-chains complex $C^{U,V}_*(X)$ equals the free $\mathbb{Z}$-module on singular $n$-simplices landing in $U$ or in $V$.
background
In the singular Mayer–Vietoris setup one works with an open cover ${U,V}$ of a space $X$ and restricts attention to singular simplices whose image lies entirely in $U$ or entirely in $V$. The degree-$n$ small chain group is the free $\mathbb{Z}$-module on those simplices, presented as a coproduct of copies of $\mathbb{Z}$.
Stage 1 packages those groups into a chain complex $C^{U,V}_*(X)$ by feeding the small chain groups and the restricted boundary maps into Mathlib's ChainComplex.of. The present lemma simply exposes the object-level component of that construction: the complex's degree-$n$ object is definitionally the small chain group already defined.
Local notation: $U,V$ are the two open sets of the cover; the small-simplex index type selects generators; the boundary on small chains is the restriction of the ordinary singular boundary.
proof idea
One-line definitional proof. The small-chains complex is built as ChainComplex.of applied to the family of small chain groups and the small boundary maps. By the API of ChainComplex.of, the degree-$n$ object is definitionally that family at $n$, so rfl closes the goal. Marked @[simp] for automatic rewriting.
why it matters
Stage 1 of the singular Mayer–Vietoris development needs a clean identification between the abstract chain-complex object and the concrete small chain groups, so later exactness and comparison maps can rewrite without unfolding ChainComplex.of. This simp lemma is that identification.
No downstream consumers are recorded yet in the graph; it is infrastructure for the Mayer–Vietoris long exact sequence on singular homology, which sits in the Foundation layer beneath the Recognition forcing chain rather than inside T0–T8 itself. It does not touch J-cost, phi, or the eight-tick octave; it is pure homological scaffolding for the geometric side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.