fundamentalSphereOneSingularOneChain_boundary_zero
plain-language theorem explainer
The once-around fundamental singular 1-chain on S¹ has vanishing boundary, hence is a genuine 1-cycle in Mathlib's integer singular chain complex. Anyone assembling H₁(S¹; ℤ) ≅ ℤ from the geometric generator cites this atom. The proof expands the alternating-face differential to a signed two-term sum and cancels the faces via the equal-faces theorem.
Claim. Let $c$ be the degree-$1$ singular chain on $S^1$ given by the coproduct summand inclusion of the once-around singular $1$-simplex, and let $d_{1,0}$ be the differential of the integer singular chain complex of $S^1$. Then $c \circ d_{1,0} = 0$.
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It works with Mathlib's imported singular chain complex of TopCat.sphere 1 with integer coefficients, the exact chain-level object whose degree-$1$ homology is the eventual strict target.
The geometric generator is the once-around singular $1$-simplex in the singular simplicial set of $S^1$. Its two faces are equal (it is a loop); that equal-faces theorem is already proved upstream. The fundamental singular $1$-chain is the corresponding coproduct summand inclusion $\mathbb{Z}\to X_1$ of that simplex into the degree-$1$ term of the singular chain complex.
The differential of the singular chain complex is the alternating face map of the simplicial object. For a $1$-simplex the boundary is therefore the signed difference of the two face $0$-simplices.
proof idea
Unfold the chain, the singular chain complex functor, and the alternating-face differential, then rewrite via AlternatingFaceMapComplex.obj_d_eq. The degree-$1$ differential reduces to a two-term Fin-sum: $+\delta_0$ minus $\delta_1$ of the fundamental simplex, as morphisms out of the $\mathbb{Z}$ summand.
After simplifying the sigma-coproduct inclusions and identity compositions, the goal is exactly that signed difference of the two face inclusions is zero. Rewrite by the upstream equal-faces theorem fundamentalSphereOneSingularOneSimplex_faces_eq; the two identical summands cancel and simp finishes.
why it matters
This is the chain-level form of the equal-faces theorem and the first geometric cycle atom in the circle $H_1$ workbench. Downstream, fundamentalCycle lifts the chain into the cycles object of the singular complex precisely by feeding this zero-boundary proof into liftCycles. The same fact is reused when generating closed singular $1$-cycles from raw prism data in CircleWindingChain.
In the broader Recognition framework the computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is the algebraic core needed before any strict bridge to the eight-tick octave and T8 ($D=3$). The module itself states it does not yet feed the strict T8 bridge until a real equivalence to Mathlib's imported singular homology object is proved; this lemma closes the cycle step of that unfinished path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.