circleH1ZIsoInt_of_orientedCyclicFamilies
plain-language theorem explainer
Assuming every oriented cyclic family of singular 1-simplices on the circle is homologous to an integer multiple of the fundamental cycle, the first singular homology of S¹ with integer coefficients is isomorphic to ℤ. Algebraic topologists closing the Mathlib H₁(S¹) computation cite this bridge step. The proof is a two-step term composition through the global boundary-generation theorem.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If every oriented cyclic family of singular $1$-simplices is homologous to an integer multiple of the fundamental cycle (plus a $2$-boundary), then there is an isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in Mathlib singular homology.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices of TopCat.sphere 1, and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes by telescoping inside the convex standard $2$-simplex.
Singular $0$- and $1$-simplices are the actual vertices and edges in Mathlib's singular simplicial set of the circle. The input hypothesis states that every concrete oriented closed walk (retained with its walk data) has free $1$-cycle equal to a $2$-boundary plus an integer multiple of the fundamental cycle.
Upstream, the target certificate is the strong Mathlib closure proposition that $H_1(S^1;\mathbb{Z})$ is isomorphic to $\mathbb{Z}$ as a $\mathbb{Z}$-module. The intermediate global generation statement asserts every singular $1$-cycle is homologous to an integer multiple of the fundamental cycle; the oriented-family hypothesis is the concrete local filling target that implies that global statement.
proof idea
One-line term proof. Feed the oriented-family hypothesis into the lemma that filling each concrete oriented cyclic family yields the global chain-level generation theorem. Pass that generation witness to the upstream closure lemma, which reduces generation of the fundamental cycle class to the final Mathlib isomorphism certificate Nonempty (H₁(S¹;ℤ) ≅ ℤ).
why it matters
Middle rung of the H₁(S¹;ℤ) ≅ ℤ closure ladder in this foundation module. Downstream, the raw-prism theorem reduces a prism-filling hypothesis on oriented cyclic families to the present oriented-family target, then invokes this result to obtain the Mathlib certificate.
The module already supplies the split-injective half: winding is a left inverse to the fundamental class, via the kills-boundaries identity and the fact that the once-around generator has winding one. Surjectivity (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs simplicial prism or subdivision data that Mathlib singular homology does not yet provide. Discharging oriented cyclic families closes that generation half and yields the integer comparison isomorphism, without axioms, sorry, or project-local S¹ replacements.
In the Recognition foundation layer this pins the topological circle's first homology as a Mathlib-facing fact, the geometric substrate on which discrete winding and octave structure sit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.