cls_natural
plain-language theorem explainer
Naturality of the degree-1 singular homology class: for a continuous map f and a 1-cycle z, the induced H1 map sends [z] to the class of the pushed cycle f#(z). Cited by anyone tracking Mayer-Vietoris injectivity on arc complements. Proof is a one-line specialization of the general class-of naturality lemma.
Claim. Let $A,B$ be topological spaces and $f:A\to B$ continuous. If $z$ is a singular $1$-chain on $A$ with $\partial z=0$, then the induced map $H_1(A)\to H_1(B)$ sends the homology class $[z]$ to the class of the image cycle $f_\#(z)$ (which is again a cycle).
background
The module works with singular chain complexes of topological spaces in TopCat, written via a coproduct presentation of the chain groups. The boundary out of degree $n+1$ is abbreviated bnd; a $1$-cycle is a degree-$1$ chain $z$ with $\partial z=0$. The degree-$1$ homology class of such a cycle is packaged as cls, which is just the general classOf construction on the singular complex at $n=0$.
Continuous maps induce chain maps on singular complexes. Upstream, chainMap_cycle records that pushforwards of cycles remain cycles: if $\partial z=0$ then $\partial(f_# z)=0$. The general naturality statement classOf_natural says homology classes push forward along any chain map of complexes: $\mathrm{homologyMap}(\varphi)([z])=[\varphi(z)]$.
Local setting is the arc-complement acyclicity development, which needs functoriality of $H_1$ classes under inclusions of open sets in Mayer-Vietoris arguments.
proof idea
One-line term wrapper. Instantiate the general naturality lemma classOf_natural at the singular chain map induced by $f$, at degree index $n=0$, on the given $1$-cycle $z$ and its cycle hypothesis. The required cycle hypothesis on the image is supplied by chainMap_cycle. Unfolding cls as classOf on the singular complex makes the two sides match the specialized statement.
why it matters
Feeds the parent theorem bounds_of_mv (elementwise Mayer-Vietoris injectivity at $H_1(U\cap V)$): with $H_2(X)=0$, a $1$-cycle of the intersection whose pushforwards bound in $U$ and in $V$ must bound in the intersection. Naturality of classes is the bookkeeping step that lets one compare the class in $H_1(U\cap V)$ with its images under the two inclusions.
In the Recognition foundation stack this sits under arc-complement acyclicity, which supports vanishing and linking arguments used when forcing spatial structure (cf. the $D=3$ landmark in the T0-T8 chain). It is pure algebraic topology scaffolding, not a physics identity, but it is load-bearing for the topological half of the forcing development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.