descApp
plain-language theorem explainer
Elementwise evaluation of the biproduct descent map: on A ⊕ B, desc(u,v) sends z to u(fst z) + v(snd z). Algebraic topologists building singular Mayer–Vietoris exactness cite it when chasing cycles through the SES of chain groups. The proof decomposes z via the biproduct total identity, then applies the universal properties of inl/inr.
Claim. For $\mathbb{Z}$-modules $A,B,M$ and morphisms $u:A\to M$, $v:B\to M$, every $z\in A\oplus B$ satisfies $\mathrm{desc}(u,v)(z)=u(\pi_A z)+v(\pi_B z)$, where $\pi_A,\pi_B$ are the biproduct projections.
background
The module SingularMayerVietoris assembles the singular-chain Mayer–Vietoris short exact sequence for a cover $X=U\cup V$, working in ModuleCat ℤ. Binary biproducts $A\boxplus B$ supply the direct-sum chain groups $C_n(U)\oplus C_n(V)$ that appear in that SES.
The biproduct descent map $\mathrm{desc}(u,v):A\boxplus B\to M$ is the unique morphism induced by a pair of maps into a common target. Its dual, lift, packages a pair of maps out of a common source. Elementwise control of these maps is needed before exactness can be checked on underlying abelian groups.
Upstream, biprod_decomp records the standard splitting $z=\iota_A(\pi_A z)+\iota_B(\pi_B z)$. The present lemma is the companion evaluation formula for descent.
proof idea
Two short calculations: $\mathrm{desc}\circ\iota_A=u$ and $\mathrm{desc}\circ\iota_B=v$, rewritten via ModuleCat.comp_apply and the biproduct identities inl_desc / inr_desc. Rewrite the left-hand side by biprod_decomp, push the morphism through the sum with map_add, and substitute the two calculations.
why it matters
Feeds directly into mvSESdeg_exact, which proves degreewise exactness of the Mayer–Vietoris short complex on singular chains. That exactness is the algebraic engine behind the long exact Mayer–Vietoris sequence used later in the foundation stack for covering arguments and gluing of recognition data on open sets.
Within Recognition Science this sits in the Foundation layer (homology infrastructure), not in the T0–T8 forcing chain itself. It is pure categorical algebra that keeps the singular-chain SES honest before any physics constants or $\varphi$-ladder statements appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.