classOf
plain-language theorem explainer
Given a cycle in degree n+1 of a chain complex of abelian groups, this returns its class in the abstract homology object H_{n+1}. Topologists and anyone proving acyclicity of arc complements cite it as the standard cycle-to-class map. The body is a pure transport: quotient by boundaries, then push across the short-complex isomorphism that aligns honest indices with the complex's built-in short complex.
Claim. Let $K$ be a chain complex of $\mathbb{Z}$-modules indexed by $\mathbb{N}$. For $n \in \mathbb{N}$ and a cycle $z \in K_{n+1}$ (so $d_{n+1}(z)=0$), the map sends $z$ to its homology class $[z] \in H_{n+1}(K)$.
background
The module develops tools for singular and group-valued chain homology of spaces, aimed at showing arc complements are acyclic in the degrees needed for linking-vanishing arguments. Homology of a complex $K$ is realized via Mathlib short complexes: at each degree one forms the three-term piece $K_{n+2} \to K_{n+1} \to K_n$, takes cycles modulo boundaries, and identifies that quotient with the abstract object $K.\mathrm{homology}(n+1)$.
The sibling isomorphism scIso is the canonical identification of the complex's built-in short complex at degree $n+1$ with the honest-index short complex $K_{n+2} \to K_{n+1} \to K_n$. Cycles enter as pairs $\langle z, dz=0\rangle$ in the cycle submodule; their classes live in the corresponding homology module of that short complex.
Upstream, the only structural ingredient is that short-complex isomorphism (plus Mathlib's left-homology data and quotient map). The name $K$ here is the chain complex, not the RS bridge constant $\varphi^{1/2}$.
proof idea
Definitional, not a proof. Form the submodule quotient class $\mathrm{Submodule.Quotient.mk},\langle z, hz\rangle$ of the cycle. Apply the inverse of the short complex's left-homology isomorphism to land in the honest short-complex homology. Then apply $\mathrm{homologyMap}$ of $(\mathrm{scIso},K,n)^{-1}$ to transport into the abstract homology object $K.\mathrm{homology}(n+1)$. No tactics; pure composition of the two inverse isomorphisms with the quotient constructor.
why it matters
This is the local cycle-to-class constructor for the arc-complement acyclicity development. Downstream it is the sole input to the vanishing criterion (class zero iff the cycle is a boundary), to representability (every homology element is some classOf), and to naturality of classes under chain maps. The degree-1 specialization cls is literally classOf at $n=0$ on the singular complex of a space, so every $H_1$ argument in the module routes through this definition.
In the broader Foundation layer it supports linking-vanishing in high dimension (the module import), which is topological scaffolding rather than a T0–T8 forcing step. It does not itself assert acyclicity; it only names the classes whose vanishing later theorems must establish.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.