span_unitOf_eq_top
plain-language theorem explainer
The canonical generators of the free ℤ-module ∐_κ ℤ span the whole module as a ℤ-submodule. Anyone proving statements about free singular chains by generation will cite this. The proof transports an arbitrary element through the coproduct–direct-sum isomorphism, expands it on its finite support, and rewrites each summand as an integer multiple of a generator.
Claim. Let $\kappa$ be the index type and let $\coprod_{\kappa}\mathbb{Z}$ be the coproduct of copies of $\mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$. Write $u_i$ for the canonical generator at index $i\in\kappa$. Then $\mathrm{span}_{\mathbb{Z}}\{u_i:i\in\kappa\}$ equals the whole module.
background
The module SingularMayerVietoris builds the algebraic scaffolding for a singular Mayer–Vietoris sequence: free chain modules on simplices, inclusions, retractions, and boundary maps. The free object in play is the coproduct $\coprod_{\kappa}\mathbb{Z}$ in the category of $\mathbb{Z}$-modules (realized via Mathlib's ModuleCat biproducts and direct sums).
The map unitOf sends each index $i\in\kappa$ to the corresponding standard basis element of that coproduct. Elementwise $\mathbb{Z}$-linearity of morphisms is packaged as mapSmul (stated through the underlying linear map to avoid instance noise on carriers). The ambient isomorphism ModuleCat.coprodIsoDirectSum identifies the categorical coproduct with the algebraic direct sum, so finite-support expansions become available.
Locally this is pure free-module algebra: no topology, no cost functional, and no Recognition Composition Law. It is the generation fact needed before one can induct on chains.
proof idea
Rewrite the goal via Submodule.eq_top_iff': every $z$ must lie in the span. Transport $z$ through the coproduct–direct-sum iso $e$, so $e^{-1}(e(z))=z$. Expand $e(z)$ as a finite sum of DirectSum.lof terms on its support. Push the sum back by $e^{-1}$, using map_sum and mapSmul, and identify each image of a unit direct-sum basis vector with unitOf i via lof_coprodIsoDirectSum_inv_apply. The resulting expression is a finite $\mathbb{Z}$-linear combination of generators, hence lies in the span by sum_mem and smul_mem.
why it matters
This lemma is the generation engine for freeInduction in the same module: to prove a property of all elements of $\coprod_{\kappa}\mathbb{Z}$ closed under $0$, $+$, and $\mathbb{Z}$-scaling, it is enough to check the generators unitOf i. The induction principle opens with membership of $z$ in the span, which is exactly this equality with $\top$.
In the broader Foundation stack, free singular modules feed the Mayer–Vietoris exact sequence used for singular homology comparisons (prism, pair, and subdivision imports). The result is ordinary free-module bookkeeping rather than a forcing-chain step (T0–T8), but without it the chain-level induction that closes exactness and naturality arguments does not start. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.