coordAt_zero
plain-language theorem explainer
The zero element of the free ℤ-module on an index set κ has vanishing coordinate at every index. Coordinate-tracking lemmas in the singular Mayer–Vietoris setup cite this as the base case for free induction on chains. The proof unfolds the coproduct-to-direct-sum presentation, uses that the iso sends zero to zero, and reads off the DFinsupp zero-at-index fact.
Claim. For every index $i\in\kappa$, the $i$-th coordinate of the zero element of $\coprod_{\kappa}\mathbb{Z}$ (equivalently $\bigoplus_{\kappa}\mathbb{Z}$ via the standard iso) is $0$.
background
The module SingularMayerVietoris builds the algebraic half of a singular Mayer–Vietoris sequence: free ℤ-chain groups on open sets $U$, $V$, and $U\cap V$, with inclusion-induced maps, and exactness at the middle term.
Chains are presented as objects of the coproduct $\coprod_{\kappa}\mathrm{ModuleCat}(\mathbb{Z})$ in the module category. The helper coordAt extracts the integer coefficient at a chosen basis index by transporting along ModuleCat.coprodIsoDirectSum and evaluating the resulting finitely supported function: it is “the coordinate of an element of $\coprod_\kappa\mathbb{Z}$ at an index, through the direct-sum presentation.”
This lemma records the trivial but necessary fact that the zero chain has all coordinates zero, so later inductions on free generators can treat the zero case in one line.
proof idea
Term-mode, three steps. Unfold coordAt to expose the composite of the coproduct-to-direct-sum homomorphism with evaluation at $i$. Rewrite by map_zero so the image of zero under that homomorphism is the zero DFinsupp. Finish with DFinsupp.zero_apply i, which states that the zero finitely supported function evaluates to $0$ at every index.
why it matters
Local bookkeeping for the free ℤ-module presentation used throughout singular Mayer–Vietoris. Downstream, coordAt_map_eq and coordAt_map_notMem track coordinates through basis-index maps (injective image preserves the source coordinate; indices outside the image get coordinate zero); both rely on the zero case when inducting on chains. Those feed mv_middle_exact, “the heart of the Mayer–Vietoris exactness: a pair of chains on $U$ and $V$ whose images in the small complex cancel comes from a chain on $U\cap V$.”
In the Recognition foundation stack this is pure algebraic topology scaffolding (singular chains, subdivision, prism operators), not a physics forcing step. It closes a tiny gap so the middle exactness argument can reason coefficientwise without special-casing zero by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.