freeInduction
plain-language theorem explainer
Any property of integer chains in the free coproduct module ∐_κ ℤ that holds on the standard generators, vanishes at zero, and is closed under addition and integer scaling holds for every chain. Algebraic topologists building singular Mayer–Vietoris and support-tracking lemmas cite it as the free-module induction principle. The proof reduces membership to the top span of the generators and applies submodule span induction.
Claim. Let $M = \coprod_{\kappa} \mathbb{Z}$ be the free $\mathbb{Z}$-module on an index set $\kappa$, with standard generators $e_i$. If $P \subseteq M$ contains every $e_i$ and $0$, and is closed under addition and integer scalar multiplication, then $P = M$: every $z \in M$ satisfies $P(z)$.
background
In the singular chain complex, the degree-$n$ chain group is the free abelian group on singular $n$-simplices. Here that group is realized as the categorical coproduct $\coprod_{\kappa} \mathrm{ModuleCat}(\mathbb{Z},\mathbb{Z})$ of copies of $\mathbb{Z}$, one per simplex index in $\kappa$. The maps $\mathrm{unitOf}, i$ pick out the standard basis vectors.
The ambient module is the Elements section of SingularMayerVietoris, which builds the algebraic toolkit for a singular Mayer–Vietoris sequence: small spans relative to an open cover, support tracking, and the short exact sequence of chain groups. Upstream, the lemma that the range of $\mathrm{unitOf}$ spans the whole coproduct as a $\mathbb{Z}$-submodule is already proved (span_unitOf_eq_top: "The generating elements span the free module $\coprod_\kappa \mathbb{Z}$").
Once the generators span, any submodule-style inductive argument on free modules becomes available. That is the local role of this induction principle.
proof idea
First rewrite the target element $z$ into the $\mathbb{Z}$-span of the range of $\mathrm{unitOf}$, using the already-proved identity that this span equals the top submodule. Then apply Mathlib's Submodule.span_induction to that membership witness, feeding in the four closure hypotheses: the property on generators (via a short rintro on the range), vanishing at zero, additivity, and integer homogeneity. No further singular-topology input is needed; the argument is pure free-module algebra.
why it matters
Almost every later support or coordinate argument in SingularMayerVietoris inducts on chains via this lemma. Downstream it discharges: coordinate transport along injective index maps (coordAt_map_eq, coordAt_map_notMem); membership of inclusions in the small span (sInc_mem_smallSpan); uniform smallness after iterated subdivision (exists_sdOpIter_mem_smallSpan); and surjectivity of the Mayer–Vietoris degree map (mvSESdeg_epi). Outside the module it also feeds the path-connected sphere lemma that every $0$-chain is homologous to a multiple of a base point (exists_bnd_of_pathConnected).
In the Recognition foundation stack this is Stage-2 algebraic scaffolding for singular homology, not a forcing-chain step (T0–T8). It does not touch J-cost, $\varphi$, or the eight-tick octave; it simply makes free-chain induction a one-liner so the Mayer–Vietoris and sphere arguments stay readable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.