fundamentalCycle_boundary_generates
plain-language theorem explainer
Every integer singular 1-cycle on the circle is a singular 2-boundary plus an integer multiple of the once-around fundamental cycle, stated inside the cycle object of Mathlib's singular chain complex. Algebraic topologists closing H₁(S¹;ℤ) ≅ ℤ cite this as the concrete chain-level generation hypothesis. It is a Prop definition packaging the remaining geometric filling work (subdivision or prism), not a proved theorem.
Claim. Every degree-$1$ cycle $z$ in the singular chain complex of $S^1$ with coefficients in $\mathbb{Z}$ admits an integer $n$ and a singular $2$-chain $b$ such that $z$ equals the image of $b$ under the degree-$2$ boundary-to-cycles map plus $n$ times the lifted fundamental cycle.
background
The module lifts path-level winding on $S^1$ to singular simplices. Displacement of a singular $1$-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval; the key identity is that alternating face displacements of every singular $2$-simplex vanish (winding kills boundaries), by convexity of $\Delta^2$ and homotopy invariance of path displacement.
The ambient complex is Mathlib's singular chain complex of TopCat.sphere 1 with integer coefficients. Its degree-$1$ homology is the stated strict target for the circle computation. The fundamental cycle is the once-around singular $1$-chain, lifted into the cycle object via its zero-boundary proof.
Winding already supplies a left inverse to the fundamental class (split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Surjectivity needs every $1$-cycle homologous to an integer multiple of that generator; Mathlib does not yet ship the prism or subdivision operator that would finish the filling.
proof idea
No proof: the declaration is a bare Prop abbreviation. Its body quantifies over degree-$1$ cycles of the sphere singular complex and asserts existence of an integer coefficient $n$ and a degree-$2$ chain $b$ witnessing the displayed equality in the cycle module (boundary image plus the image of $n$ under the fundamental-cycle map). Downstream lemmas treat this Prop as a hypothesis and discharge it from weaker geometric assumptions (zero-winding filling, directed-cycle terms, oriented cyclic families, or finite closed-generator spanning).
why it matters
This is the remaining geometric obligation for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Feeding it into the one-step wrapper that kills the $2$-boundary under homology projection yields cycle-class generation; that in turn yields the final Mathlib integer comparison isomorphism for circle $H_1$.
Several reduction theorems target exactly this Prop: from integral winding plus zero-winding bounds; from spanning by a closed singular one-cycle list plus zero-winding filling; and from boundary generation of directed-cycle terms or oriented cyclic families. The module doc records that the split-injective half is already in hand via winding of the fundamental loop, so closing this Prop finishes the isomorphism.
In the Recognition stack the degree-$1$ homology of this complex is flagged as the final strict T8 target on the circle side. The open work is constructive: build the $2$-chain witness by subdivision, prism, or singular filling of the zero-winding remainder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.