coordAt_unitOf
plain-language theorem explainer
The coordinate of a free-module generator at index i is the Kronecker delta: 1 at i and 0 elsewhere. Algebraic topologists working the singular Mayer–Vietoris setup cite this when tracking basis elements under coproduct maps. The proof unfolds the direct-sum iso and case-splits on index equality.
Claim. For indices $i,j$ in the basis index set $\kappa$, the $j$-th coordinate of the free generator $e_i\in\coprod_{\kappa}\mathbb{Z}$ equals $1$ if $i=j$ and $0$ otherwise.
background
The module builds singular-chain infrastructure for a Mayer–Vietoris argument: free $\mathbb{Z}$-modules on index sets of singular simplices, realized as categorical coproducts $\coprod_{\kappa}\mathrm{Mod}_{\mathbb{Z}}(\mathbb{Z})$ and identified with direct sums.
unitOf i is the generator $e_i$ at index $i$, the image of $1\in\mathbb{Z}$ under the coproduct inclusion. coordAt j reads the $j$-th coordinate after transporting through the coproduct–direct-sum isomorphism. Together they give the standard dual basis pairing on free abelian groups.
Upstream, the only external simp used is composition evaluation on module morphisms; the local definitions supply the rest.
proof idea
Unfold both definitions, rewrite the coproduct inclusion through the direct-sum iso via ModuleCat.ι_coprodIsoDirectSum_hom, and reduce to evaluating DirectSum.lof at index $j$. Case-split on $i=j$: on equality, DirectSum.of_eq_same gives $1$; on inequality, DirectSum.of_eq_of_ne gives $0$.
why it matters
Feeds the two coordinate-tracking lemmas coordAt_map_eq and coordAt_map_notMem, which say that a map sending generators $e_i\mapsto e_{\psi(i)}$ for injective $\psi$ preserves source coordinates on the image of $\psi$ and kills coordinates off that image. Those lemmas are the bookkeeping engine for free induction on chains under subdivision and inclusion maps in the singular Mayer–Vietoris complex.
In the Recognition foundation layer this is pure homological scaffolding: it underwrites exactness and degree-counting arguments that later connect to the eight-tick octave and dimensional forcing, but the lemma itself is classical free-module arithmetic with no physics content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.