biprod_decomp
plain-language theorem explainer
Any element of a binary biproduct $A\boxplus B$ in $\mathbf{Mod}_{\mathbb{Z}}$ equals the sum of the two canonical injections applied to its two projections. Homological algebraists building Mayer–Vietoris for singular chains cite it for elementwise biproduct calculus. The proof evaluates the biproduct total identity at $z$ and unpacks addition and composition in $\mathbf{ModuleCat}$.
Claim. Let $A,B$ be objects of $\mathbf{ModuleCat}_{\mathbb{Z}}$ and let $z\in A\boxplus B$. Then $z=\iota_A(\pi_A(z))+\iota_B(\pi_B(z))$, where $\iota_A:A\to A\boxplus B$, $\iota_B:B\to A\boxplus B$ are the biproduct injections and $\pi_A:A\boxplus B\to A$, $\pi_B:A\boxplus B\to B$ are the projections.
background
The ambient setting is singular chain complexes over $\mathbb{Z}$ in the Foundation Mayer–Vietoris development. Binary biproducts $A\boxplus B$ in an abelian category (here $\mathbf{ModuleCat}_{\mathbb{Z}}$) come with injections $\mathrm{inl},\mathrm{inr}$ and projections $\mathrm{fst},\mathrm{snd}$ satisfying the usual biproduct identities.
Mathlib supplies biprod.total: the endomorphism $\mathrm{fst}\gg\mathrm{inl}+\mathrm{snd}\gg\mathrm{inr}$ equals the identity on $A\boxplus B$. Working elementwise requires that addition of morphisms and composition act pointwise on underlying modules. The local helper addApp records $(f+g)(x)=f(x)+g(x)$ for morphisms in $\mathbf{ModuleCat}$.
This lemma is the element-level unpacking of that total identity, so later arguments can rewrite a biproduct element as the sum of its two pure components without leaving the category of modules.
proof idea
Start from biprod.total, which equates $\mathrm{id}_{A\boxplus B}$ with $\mathrm{fst}\gg\mathrm{inl}+\mathrm{snd}\gg\mathrm{inr}$. Apply congruence of evaluation at the given element $z$ to both sides.
On the composite-sum side, addApp turns the sum of morphisms into a sum of values, and two uses of ModuleCat.comp_apply push the compositions through to $\mathrm{inl}(\mathrm{fst},z)+\mathrm{inr}(\mathrm{snd},z)$. On the identity side, ModuleCat.id_apply recovers $z$.
A short simp substitutes both rewrites into the congruence, and symmetry yields the stated decomposition.
why it matters
Elementwise biproduct control is infrastructure for the singular Mayer–Vietoris sequence in this module. Immediately downstream, biprod_elem_ext uses the decomposition twice to conclude $z=w$ from equal projections, and descApp uses it to give the pointwise formula for biprod.desc.
Those lemmas let chain-level maps out of (and equalities inside) biproducts of singular chain groups be checked on components. That is the algebraic step needed when gluing relative singular complexes along a cover, before any Recognition-specific forcing (T0–T8) enters. The lemma itself is pure categorical linear algebra; its place in the RS mirror is as a proved foundation brick under the singular MV development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.