ev1
plain-language theorem explainer
Evaluation-at-1 turns a ℤ-module morphism f : ℤ → M into the single element f(1) ∈ M, as a ℤ-linear map on Hom(ℤ, M). Singular-chain arguments cite it whenever free generators are packaged as maps out of ℤ. The definition is the standard Hom-evaluation; additivity and scalar compatibility are definitional.
Claim. For any $\mathbb{Z}$-module $M$, the map $\mathrm{ev}_1 : \mathrm{Hom}_{\mathbb{Z}}(\mathbb{Z}, M) \to M$ given by $f \mapsto f(1)$ is $\mathbb{Z}$-linear.
background
In the singular Mayer–Vietoris development, free $\mathbb{Z}$-modules on simplices are handled in ModuleCat (the category of modules). A generator of a free summand is often a morphism out of $\mathbb{Z}$ rather than an abstract basis vector; evaluating that morphism at $1 \in \mathbb{Z}$ recovers the image element in the target module $M$.
The surrounding module builds small spans of singular chains relative to an open cover $U \cup V = X$, subdivision operators, and the prism/homotopy operators that feed the Mayer–Vietoris exact sequence. Evaluation-at-1 is the bridge between “map out of $\mathbb{Z}$” language and ordinary membership statements in those submodules.
(The dependency graph’s hits on unrelated symbols named M are name collisions; here $M$ is only the target module parameter.)
proof idea
Definitional: toFun sends $f$ to $f(1)$. Both map_add' and map_smul' hold by rfl because addition and scalar multiplication of module morphisms are pointwise. No external lemmas are invoked.
why it matters
Local plumbing for the singular Mayer–Vietoris chain of this module. Downstream lemmas rewrite compositions with coproduct inclusions via ev1 (comp_unitOf, ev1_apply), and the small-span closure proofs for affine chains, subdivision, and the prism homotopy all reduce generator cases to statements of the form ev1 (toChain …) ∈ smallSpan (toChain_one_mem_smallSpan, sdOp_mem_smallSpan, tOp_mem_smallSpan, and the uniform smallness iterate). Those feed the cover-refinement argument that every singular chain becomes $U$–$V$-small after enough subdivisions—the algebraic input to Mayer–Vietoris for singular homology. It is infrastructure, not a Recognition forcing step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.