coordAt
plain-language theorem explainer
Extracts the integer coefficient at a fixed basis index from an element of the free ℤ-module on a discrete index set κ, via the coproduct-to-direct-sum isomorphism. Algebraic topologists working the singular Mayer–Vietoris sequence cite it whenever they need support or coefficient tracking on free chain groups. The body is a one-line projection through ModuleCat.coprodIsoDirectSum.
Claim. For an index $i\in\kappa$ and an element $z$ of the coproduct $\coprod_{\kappa}\mathbb{Z}$ (as an object of $\mathbf{Mod}_{\mathbb{Z}}$), $\mathrm{coordAt}(i,z)\in\mathbb{Z}$ is the $i$-th coordinate of $z$ under the canonical isomorphism of that coproduct with the direct sum $\bigoplus_{\kappa}\mathbb{Z}$.
background
In the singular Mayer–Vietoris development, free chain groups on a discrete index set of simplices are realized as coproducts $\coprod_{\kappa}\mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$. Mathlib supplies a canonical isomorphism of that coproduct with the direct-sum object whose underlying type is a finitely supported function $\kappa\to\mathbb{Z}$.
The coordinate map is the composite of that isomorphism with evaluation at a chosen index. It is the standard way to read off the integer multiplicity of a generator inside a free chain. Sibling infrastructure in the same module (unit generators, support predicates, inclusion/retraction maps for small subcomplexes) all speak in this language.
The ambient module is the Foundation singular-homology stack: prism operators, singular pairs, and barycentric subdivision feed the same free-module presentation, so coefficient extraction is shared across those constructions.
proof idea
One-line definitional wrapper. Apply the forward map of ModuleCat.coprodIsoDirectSum (the coproduct $\to$ direct-sum isomorphism for the constant family of $\mathbb{Z}$-modules indexed by $\kappa$), then evaluate the resulting direct-sum element at the index $i$. No further lemmas are invoked in the body; additivity, scalar homogeneity, and values on unit generators are proved separately by unfolding this definition and using DFinsupp arithmetic.
why it matters
Coefficient extraction is the primitive that turns free-chain identities into integer equations. Downstream lemmas coordAt_add, coordAt_smul, coordAt_zero, and coordAt_unitOf establish that it is a $\mathbb{Z}$-linear dual basis functional. The tracking lemmas coordAt_map_eq and coordAt_map_notMem control how coordinates move under injective reindexings of generators, which is exactly what support-preserving chain maps require.
Outside the module, exists_chain_lift in ArcComplementAcyclic uses coordinates (via support) to lift a chain whose geometric support avoids a closed set $T$ back to the complement of $T$. That lifting is part of the acyclicity argument for arc complements, which sits in the Foundation layer that underwrites the topological side of the Recognition forcing chain (local contractibility and excision inputs to the eight-tick and dimension steps).
As a bare definition it closes no open conjecture, but every support or multiplicity argument in the singular MV package routes through it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.