classOf_natural
plain-language theorem explainer
Homology classes of cycles push forward along chain maps: the homology map of φ sends the class of a cycle z to the class of φ(z). Anyone tracking singular or abstract chain maps through H_{n+1} will cite this. The proof factors homology through short-complex isomorphisms and left-homology data, then chases the quotient class under the induced short-complex map.
Claim. Let $\varphi:K\to L$ be a morphism of chain complexes of $\mathbb{Z}$-modules (shape $\mathrm{down}\,\mathbb{N}$), let $z\in K_{n+1}$ be a cycle, and assume $\varphi(z)$ is a cycle in $L$. Then $H_{n+1}(\varphi)([z])=[\varphi_{n+1}(z)]$ in $H_{n+1}(L)$, where $[\cdot]$ denotes the homology class built from a cycle via the short-complex left-homology presentation.
background
The module develops tools for arc-complement acyclicity in the foundation layer: singular chain complexes of topological spaces, their homology, and how classes move under continuous maps. Inside ClassToolkit, a cycle $z\in K_{n+1}$ with $d z=0$ is packaged as a homology class by classOf, which routes through the short complex at degree $n+1$ and the module-category left-homology isomorphism to the quotient $\ker d/\mathrm{im},d$.
Chain complexes here live in ModuleCat ℤ with ComplexShape.down ℕ. The short-complex functor and the natural isomorphism natIsoSc' identify the standard short complex at $n+1$ with the three-term window $(n+2,n+1,n)$. A local iso scIso mediates between those presentations. Homology maps of complex morphisms are then short-complex homology maps of the induced maps on those windows.
The lemma is pure homological algebra: no Recognition-cost or ladder data enters. Name collisions in the dependency graph (cost $H$, bridge $K$, species down) are unrelated; the live inputs are classOf, short-complex homology maps, and the left-homology data maps.
proof idea
Define $\psi$ as the image of $\varphi$ under the primed short-complex functor on the window $(n+2,n+1,n)$, and $e$ as natIsoSc' on that window. Naturality of $e$ plus hom_inv_id yields a commuting triangle relating the ordinary short-complex functor map of $\varphi$ to $(\mathrm{scIso},K).\mathrm{hom}\gg\psi\gg(\mathrm{scIso},L).\mathrm{inv}$.
Hence homologyMap φ equals the short-complex homology map of that composite. Unfold classOf and apply hom_inv_apply on the homology iso of scIso K to land on the inverse homology iso applied to the submodule quotient class of $\langle z,hz\rangle$. The left-homology map data of $\psi$ then sends that quotient class to the quotient class of $\langle\varphi(z),hz'\rangle$ (via homologyMap_eq and kerMap). A short calc composes the three short-complex homology maps and closes by definition of classOf on $L$.
why it matters
This is the abstract naturality engine for homology classes in the arc-complement development. Downstream, cls_natural specialises it to singular 1-chains: for $f:A\to B$ continuous, $H_1(sChainMap f)$ sends $\mathrm{cls}_A(z)$ to $\mathrm{cls}B(f\sharp z)$, proved as the one-line instance classOf_natural (sChainMap f) 0 ....
In the broader Recognition foundation, arc-complement acyclicity and linking-vanishing arguments (imported from LinkingVanishingHighDim) need classes to move cleanly under induced chain maps when comparing spaces and their complements. Without naturality, degree-1 cycle classes could not be transported along continuous maps while staying inside the same short-complex presentation.
The lemma sits below the topological wrappers (cycles, bounding, classes of 1-chains) and does not itself touch T5–T8, RCL, or the φ-ladder; it is infrastructure those geometric claims rely on when they speak in homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.