exists_preimage_of_isColimit_cokernel_eq_zero
plain-language theorem explainer
Element-level exactness for a cokernel cofork in ModuleCat: if p is the cokernel projection of f and p kills x in N, then x lies in the image of f. Homological algebraists and anyone reducing vanishing homology classes to boundaries will cite it. The proof compares p to the concrete quotient map N → N/im(f) via the colimit universal property, then unpacks membership in the range.
Claim. Let $R$ be a ring and $M,N,Q$ objects of $\mathbf{Mod}_R$. Let $f:M\to N$ and $p:N\to Q$ with $p\circ f=0$. If the cofork of $p$ is a colimit (so $p$ is a cokernel of $f$), and if $p(x)=0$ for some $x\in N$, then there exists $m\in M$ such that $f(m)=x$.
background
In the category of modules over a ring $R$, the cokernel of a map $f:M\to N$ may be presented either as the concrete quotient $N/\mathrm{im}(f)$ or, abstractly, as a colimit of the cokernel cofork of a parallel pair. The theorem equates the two presentations at the level of elements: vanishing under an abstract cokernel projection is the same as lying in the image of $f$.
The ambient module is Foundation.CircleWindingChain, which lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries. That identity, together with the once-around generator mapping to $1$, yields the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Element-level exactness is the bridge from "homology class zero" to "the cycle is a boundary" inside that argument.
No Recognition-Science-specific cost functional or forcing step is used here; the lemma is pure categorical homological algebra over ModuleCat.
proof idea
Build, via the colimit descriptor of the given cofork, a comparison map $\mathrm{desc}:Q\to N/\mathrm{im}(f)$ into the concrete cokernel. The colimit face identity says $p\circ\mathrm{desc}$ equals the canonical quotient projection $N\twoheadrightarrow N/\mathrm{im}(f)$.
Apply both sides to $x$. Since $p(x)=0$, the composite sends $x$ to $0$, so the quotient class of $x$ vanishes. By the usual criterion, $x\in\mathrm{im}(f)$. Unpack the range membership to obtain a preimage $m\in M$ with $f(m)=x$.
The argument is a short tactic script: one desc, one face identity, a quotient-zero rewrite, and LinearMap.mem_range.
why it matters
Downstream, cycle_eq_boundary_of_homologyπ_eq_zero applies this lemma to turn a vanishing homology class of a $1$-cycle into an explicit preimage under the boundary map. That step is required for the chain-level winding invariant on singular simplices of $S^1$ to detect homology rather than mere cycles.
In the module narrative, the winding homomorphism on $1$-cycles is already a left inverse to the fundamental class (split-injectivity of $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$). Surjectivity of the comparison map still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply; this lemma closes only the exactness half of the boundary-recognition step, not the generation half.
It is scaffolding-free pure algebra inside the Foundation layer: no axioms, no sorry, and no project-local replacement of $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.