exists_classOf
plain-language theorem explainer
Every abstract homology class in degree n+1 is the class of some genuine cycle. Used by anyone extracting concrete nonbounding cycles from nonvanishing homology (notably the arc-complement argument). Proof lifts h through the short-complex homology iso, then uses surjectivity of the quotient-by-boundaries map and cancels the iso pair.
Claim. Let $K$ be a chain complex. For every $n \in \mathbb{N}$ and every homology class $h \in H_{n+1}(K)$, there exist a chain $z \in K_{n+1}$ with $dz = 0$ such that the homology class of $z$ equals $h$.
background
The module works in the homological algebra of chain complexes of modules (Mathlib HomologicalComplex / ShortComplex), preparing the arc-complement acyclicity and linking-vanishing facts imported from LinkingVanishingHighDim.
classOf sends a degree-$(n+1)$ cycle $z$ (i.e. $d z = 0$) to its class in the abstract object $K.\mathrm{homology}(n+1)$. Internally it quotients by boundaries in the honest-index short complex $K_{n+2}\to K_{n+1}\to K_n$, then transports along the inverse of the canonical short-complex isomorphism scIso (from K.sc(n+1) to that honest triple).
inv_hom_apply is the elementary cancellation $e^{-1}(e(x))=x$ for a module isomorphism $e$. Together these make abstract homology elements interchangeable with cycle-mod-boundary data.
proof idea
Term-mode existence proof. Apply Submodule.mkQ_surjective to the image of $h$ under the composite of homologyMap (scIso n).hom with the left-homology iso of the honest short complex; this yields a cycle representative $\langle z, hz\rangle$ in the quotient by boundaries.
Refine the existential with that $z$ and $hz$. Unfold classOf, rewrite the quotient equality just obtained, then cancel the remaining iso pair by two applications of inv_hom_apply (once on the short-complex homology iso, once on homologyMapIso (scIso n)). The result is exactly $h$.
why it matters
Representability is the bridge from abstract nonvanishing of homology to concrete geometric cycles. Downstream, exists_nonbounding cites it: a nonvanishing $H_1(W)$ produces a cycle $z$ in degree 1 with $dz=0$ that is not a boundary. That lemma is the working engine for arc-complement arguments in this foundation layer (nonbounding 1-cycles obstruct acyclicity and control linking).
In the broader Recognition stack this sits under the topological forcing material that feeds dimensional and octave constraints (T7 eight-tick period, T8 $D=3$), where one needs homology classes to be realized by actual chains rather than formal symbols. The lemma itself is pure homological algebra; its value is that the later geometric claims can quote cycles, not just classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.