ev1_apply
plain-language theorem explainer
Unfolding lemma: the linear evaluation map on morphisms out of ℤ returns the image of the unit 1. Anyone simplifying free singular generators under chain maps or inclusions cites it. The proof is pure definitional equality (rfl).
Claim. For any $\mathbb{Z}$-module $M$ and any morphism $f:\mathbb{Z}\to M$ in $\mathbf{Mod}_{\mathbb{Z}}$, the evaluation map $\mathrm{ev}_1$ satisfies $\mathrm{ev}_1(f)=f(1)$.
background
In the singular Mayer–Vietoris setup, free chain groups are biproducts $\coprod_\kappa \mathbb{Z}$ of copies of $\mathbb{Z}$, one per singular simplex index. Morphisms out of a single copy $\mathbb{Z}$ are determined by where they send $1$.
The upstream definition $\mathrm{ev}_1$ packages that determination as a $\mathbb{Z}$-linear map $(\mathbb{Z}\to M)\to M$ with $\mathrm{toFun},f:=f(1)$. Generating elements of the free biproduct (the units attached to each index) are built so that composing an inclusion of a summand with a map $\varphi$ and then evaluating at $1$ recovers $\varphi$ on that generator.
The ambient module is ordinary singular chain algebra over $\mathbb{Z}$ in $\mathbf{ModuleCat}$, not yet the long exact sequence; this lemma is bookkeeping for those generators.
proof idea
Term-mode one-liner: rfl. By definition of $\mathrm{ev}_1$, its underlying function is $f\mapsto f(1)$, so the stated equality is definitional and needs no further lemmas.
why it matters
Local glue for generator calculus in singular Mayer–Vietoris. Downstream, comp_unitOf rewrites $\varphi(\mathrm{unitOf},i)$ as $\mathrm{ev}_1$ of the composite of the summand inclusion with $\varphi$; the inclusions $u\mathrm{Inc}$, $v\mathrm{Inc}$ and the singular chain map then use that rewrite plus this simp lemma to prove they send generators to generators (uInc_unitOf, vInc_unitOf, chainMap_unitOf).
Those elementwise identities are what make the MV short complex of free singular chains well-defined on the standard basis before passing to homology. No Recognition forcing step (T0–T8) is involved; this is pure foundational homological algebra supporting the singular side of the RS stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.