closedSingularOneCycle
plain-language theorem explainer
A closed singular 1-simplex on S¹ (equal face endpoints) is packaged as an actual degree-1 cycle in the integer singular chain complex of the circle. Anyone proving that zero-winding loops bound, or that closed edges are homologous to integer multiples of the fundamental cycle, cites this constructor. The body is a one-line liftCycles application of the generator-level boundary-vanishing lemma.
Claim. Given a singular $1$-simplex $s$ on $S^1$ whose two face maps agree ($\delta_0 s = \delta_1 s$), there is a morphism $\mathbb{Z} \to Z_1(S^1;\mathbb{Z})$ sending $1$ to the singular chain generator of $s$, which is a genuine $1$-cycle.
background
The module lifts path-level winding on the circle to singular simplices of TopCat.sphere 1 and proves that displacement kills boundaries, the chain-level fact needed for a homology invariant. A singular $1$-simplex is a continuous map $\Delta^1 \to S^1$ in the singular simplicial set; its two faces $\delta_0,\delta_1$ are the endpoint $0$-simplices. When those faces coincide the simplex is a closed edge (a loop at the chain level).
The ambient complex is the Mathlib singular chain complex of $S^1$ with integer coefficients, whose degree-$1$ homology is the strict T8 target $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Upstream, the generator-level lemma states that a singular $1$-simplex with equal endpoints has vanishing boundary in that complex: the coproduct summand inclusion of $s$ composed with $d_{1,0}$ is zero. Cycles are then obtained by the standard liftCycles construction into the kernel of the differential.
proof idea
One-line definitional wrapper. Apply sphereOneSingularIntChainComplex.liftCycles to the coproduct generator inclusion of $s$ into $C_1$, with the zero map on the complementary summand (discharged by simp), using singularOneSimplexChain_boundary_zero_of_faces_eq s hfaces as the proof that the differential vanishes. The result is a morphism $\mathbb{Z}\to Z_1$ whose image is the cycle class of that closed edge.
why it matters
This is the canonical cycle object for every closed singular edge. Downstream consumers use it as the left-hand side of bounding and generation statements: cone fillings prove the cycle bounds (closedSingularOneCycle_bounds_of_cone_simplex, _of_cone_map, _of_closed_cone_map, _of_continuous_coneCirclePoint, _of_free_boundary); prism and free-chain identities prove it is homologous to an integer multiple of the fundamental cycle (closedSingularOneCycle_boundary_generate_of_freePrismToFundamental, _of_rawPrismToFundamental, _of_zero_winding_coneCirclePoint).
Together with the winding homomorphism (left inverse to the fundamental class via pathWinding_fundamentalLoop), these feed the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs simplicial prism/subdivision operators that Mathlib singular homology does not yet supply; this definition is the cycle-side handle those arguments act on. In the Recognition forcing chain it sits under the T8 dimensional/topological identification of the circle's first homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.