cls
plain-language theorem explainer
Specializes the abstract homology-class map to degree-1 singular cycles: a 1-cycle on a space W is sent to its class in H₁(W; ℤ). Anyone proving arc-complement acyclicity or Mayer–Vietoris injectivity at H₁ cites this packaging. The body is a one-line wrapper of the general classOf map on the singular chain complex of W.
Claim. For a topological space $W$ and a singular $1$-chain $z$ with $\partial z=0$, the value $\mathrm{cls}(W,z)$ is the homology class $[z]\in H_1(W;\mathbb{Z})$.
background
The ambient module builds singular homology of spaces in TopCat with ℤ coefficients, via the singular chain complex SC(W). Chain groups Cgrp(W,n) are the coproduct presentation ∐_σ ℤ over singular n-simplices; the boundary bnd(W,n) is the differential out of degree n+1. Homology groups Hgrp(W,n) are the homology objects of SC(W) in degree n.
Upstream, classOf packages the standard construction: a cycle z in degree n+1 (kernel of the differential) is sent to its class in the abstract homology object K.homology(n+1), via the short-complex homology iso of the chain complex. The present definition freezes that construction at n=0 on K=SC(W), so the input is a 1-cycle and the output lives in H₁(W).
Local setting is the arc-complement acyclicity development: one needs a named degree-1 class map to state vanishing, naturality under continuous maps, and Mayer–Vietoris injectivity elementwise on H₁ of intersections.
proof idea
One-line wrapper. Apply classOf to the singular chain complex SC(W) at index 0, with the given 1-cycle z and the hypothesis that bnd(W,0) z = 0. No extra algebra: the general short-complex homology iso already produces the element of Hgrp(W,1).
why it matters
Gives the concrete degree-1 class map used throughout ArcComplementAcyclic. Immediate consumers: cls_eq_zero_iff (class vanishes iff the cycle bounds), cls_natural (homologyMap of the singular chain map sends cls to cls of the image cycle), and bounds_of_mv (elementwise MV injectivity at H₁(U∩V): if H₂(X)=0 and a 1-cycle of the intersection pushes forward to boundaries in U and in V, then it bounds in the intersection).
That MV injectivity is the algebraic engine for showing complements of arcs (and related 1-dimensional sets) have vanishing H₁ in the Recognition foundation layer. The definition itself carries no physics content; it is the typed handle that lets those vanishing and injectivity statements talk about [z] rather than raw cycles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.