ClosedSingularOneCycleTerm
plain-language theorem explainer
Packages one closed singular 1-simplex on S¹ together with an integer coefficient as a single summand in a closed-generator decomposition of a singular 1-cycle. Anyone building integer 1-cycles from loops on the circle for the winding homomorphism cites this carrier. Pure structure definition: simplex, endpoint-face equality, and coeff.
Claim. A closed singular one-cycle term is a triple $(\sigma,\,\delta_0\sigma=\delta_1\sigma,\,c)$ where $\sigma$ is a singular $1$-simplex on $S^1$ (a continuous map $\Delta^1\to S^1$), the two face maps of $\sigma$ agree (so $\sigma$ is a closed loop), and $c\in\mathbb{Z}$ is an integer coefficient.
background
The ambient module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact needed for a homology invariant. A singular $1$-simplex here is an object of the singular simplicial set of TopCat.sphere 1, i.e. a continuous map from the standard $1$-simplex $\Delta^1$ into $S^1$.
The two face operators $\delta_0,\delta_1$ extract the endpoints of that simplex. Equality of faces means the path is closed: start and end coincide on $S^1$. Integer coefficients live in the free $\mathbb{Z}$-module underlying the singular chain complex sphereOneSingularIntChainComplex.
Module goal (from the header): combine this packaging with simplexDisplacement and the kills-boundaries identity to get a winding map on $1$-cycles that is a left inverse to the fundamental class, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
No proof: this is a structure (data carrier). Three fields only: the singular $1$-simplex, a propositional equality of its two faces, and an integer coefficient in ModuleCat.of ℤ ℤ. The companion projection ClosedSingularOneCycleTerm.cycle turns one such term into an actual $1$-cycle by applying closedSingularOneCycle to the simplex and face equality, then scaling by the coefficient via ModuleCat.Hom.hom.
why it matters
Sits in the Foundation circle-winding chain that aims at the classical isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ without axioms or project-local circle replacements. The module already has the kills-boundaries identity (simplexDisplacement_boundary) and the generator evaluation (pathWinding_fundamentalLoop sends the once-around loop to $1$). Finite sums of these closed terms are the concrete cycles on which that winding homomorphism is evaluated.
No downstream consumers are wired yet in the graph (used_by empty). The open half of the story remains generation: every $1$-cycle homologous to an integer multiple of the fundamental cycle needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. This structure is the bookkeeping atom for the closed-generator side of that comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.