sum_coordAt_smul_unitOf
plain-language theorem explainer
Every element of the coproduct ∐_κ ℤ equals the finite sum of its coordinates times the corresponding unit generators. Anyone reconstructing free chains from supports in the singular Mayer–Vietoris complex cites this. The proof transports the standard DirectSum support expansion across the coprodIsoDirectSum isomorphism and pulls scalars through the inverse.
Claim. For every $z$ in the coproduct $\coprod_{\kappa}\mathbb{Z}$, one has $z=\sum_{i\in\mathrm{supp}(z)}c_i(z)\,u_i$, where $c_i(z)$ is the $i$-th coordinate of $z$ (via the direct-sum presentation) and $u_i$ is the canonical generator at index $i$.
background
The module SingularMayerVietoris builds the algebraic scaffolding for a Mayer–Vietoris sequence in singular chains. Free abelian groups appear as coproducts $\coprod_\kappa\mathbb{Z}$ in ModuleCat, indexed by a type $\kappa$ of generators (simplices or small-support labels).
Coordinates and support are read through the Mathlib isomorphism ModuleCat.coprodIsoDirectSum: coordAt i z is the $i$-th component of the image of $z$, and suppOf z is the finite support of that direct-sum element. The generators unitOf i are the images of the standard basis vectors under the inverse isomorphism.
Upstream, mapSmul records elementwise $\mathbb{Z}$-linearity of ModuleCat morphisms (stated on underlying maps to avoid instance noise). The reconstruction identity is the free-module fact that every finitely supported family is the sum of its values times basis vectors.
proof idea
Unfold suppOf and coordAt, and set $e$ to be coprodIsoDirectSum. Recover $z$ as $e^{-1}(e(z))$. Expand $e(z)$ by DirectSum.sum_support_of, rewriting each summand via lof_eq_of. Push the sum through $e^{-1}$ with map_sum. For each index, factor the coefficient out of lof by map_smul and mul_one, then apply mapSmul and identify the image of the unit with unitOf i via lof_coprodIsoDirectSum_inv_apply. The resulting equality is the claim.
why it matters
This is the bookkeeping lemma that lets one rebuild a chain from its nonzero coordinates. Downstream, mv_middle_exact (the heart of Mayer–Vietoris exactness: a cancelling pair of chains on $U$ and $V$ comes from a chain on $U\cap V$) and exists_chain_lift (compact-support lifting across nested complements) both sum over supports and scale generators; both invoke this identity.
In the Recognition foundation stack the lemma is pure homological algebra: it underwrites exactness of the small-complex Mayer–Vietoris sequence used later for acyclicity and covering arguments, not a forcing-chain step (T0–T8) itself. It closes the free-module presentation gap so those exactness proofs stay sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.