kerMap_coe
plain-language theorem explainer
Coercing the induced kernel map on cycles back to the ambient chain module recovers the middle component of a short-complex morphism. Anyone simplifying concrete Mayer–Vietoris diagrams will cite this simp rule. The proof is pure definitional equality from LinearMap.restrict.
Claim. Let $\psi:S\to T$ be a morphism of short complexes of $\mathbb{Z}$-modules and let $x$ lie in $\ker(S.g)$. Writing $\mathrm{kerMap}(\psi)$ for the restriction of $\psi$'s middle component to kernels, the underlying element of $\mathrm{kerMap}(\psi)(x)$ in $T.X_2$ equals $\psi_{\tau_2}(x)$ in $S.X_2$.
background
The module builds a concrete singular Mayer–Vietoris sequence for Recognition Science chain complexes. Short complexes $S,T$ carry differentials $g$ on the middle term $X_2$; cycles are the kernels $\mathrm{LinearMap.ker},S.g.hom$ and $\mathrm{LinearMap.ker},T.g.hom$.
A morphism $\psi:S\to T$ supplies component maps, written $\tau_2$ on the middle degree. The sibling definition kerMap is the induced map on concrete cycles: it restricts $\psi.\tau_2.hom$ to those kernels, using the lemma that $\tau_2$ sends $\ker S.g$ into $\ker T.g$.
This coercion identity is the bookkeeping step that lets later exactness arguments treat the restricted map as ordinary application of $\tau_2$ after forgetting the subtype.
proof idea
One-line rfl. By definition kerMap ψ is LinearMap.restrict ψ.τ₂.hom (τ₂_maps_ker ψ), and the coercion out of a restricted linear map is definitionally the underlying map applied to the coerced domain element. No lemmas are invoked beyond that definitional unfolding.
why it matters
Sits in the Foundation singular Mayer–Vietoris layer that underpins homology exactness for the Recognition chain complexes (imports: SingularPrism, SingularPair, SingularSubdivision). The induced cycle map is the concrete stand-in for the map on $H_1$ that feeds the MV connecting homomorphism.
No downstream uses are recorded yet; the lemma is infrastructure for simp-normalization when assembling the long exact sequence. It does not itself touch T0–T8, RCL, or the phi ladder, but keeps the algebraic topology side of the foundation machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.