cyclicSingularEdgeListTerm_of_cyclicFamily
plain-language theorem explainer
A cyclically connected finite family of singular 1-simplices on S¹ packages as a concrete cyclic edge-list term with coefficient 1. Anyone bridging the oriented-cycle engine to the older forward-only extraction interface cites this. Construction reuses the directed-cycle free term for cycle and winding data, then matches the free-chain sum via the ofFn edge-list identity.
Claim. Given a finite family $e:\mathrm{Fin}\,k\to$ singular $1$-simplices on $S^1$ such that the terminal vertex of each $e_i$ equals the initial vertex of $e_{i+1}$ (indices mod $k$), there is a concrete cyclic edge-list term whose edge list is $[e_0,\ldots,e_{k-1}]$, with integer coefficient $1$, whose certified degree-$1$ cycle has free-chain image equal to that listed edge sum, and whose winding number is integral.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. A singular one-simplex is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$. Initial and terminal vertices are the two face maps $\delta_1$ and $\delta_0$.
A concrete cyclic edge-list term records a finite list of such edges, a global integer coefficient, a certified cycle in the integer singular chain complex of $S^1$, the equality that the free-chain image of that cycle is the coefficient times the listed edge sum, and integrality of the cycle winding.
Upstream, a cyclically connected family already assembles into a directed-cycle free term: the free edge-chain $\sum_i\langle e_i\rangle$ lifts to a genuine $1$-cycle (boundary vanishes by the cyclic free-boundary identity) with integer winding. That object supplies the homological payload reused here.
proof idea
Structure construction, not a deep proof. Set edges to List.ofFn e and coeff to $1$. Pull cycle and winding_integral directly from directedCycleFreeTerm_of_cyclicFamily e hconn.
For chain_eq, start from that upstream term's chain equality (free image of the cycle equals $\sum_i$ free generators of the $e_i$). Rewrite the goal to match coefficient $1$ times the singular edge-list chain of List.ofFn e, apply singularEdgeListChain_ofFn, and finish by simp.
why it matters
Marks the exact compatibility surface between the older forward-only cyclic edge-list extraction target and the newer oriented-cycle engine (doc-comment). Downstream, every everywhere-forward oriented cyclic family converts through this constructor into a cyclic edge-list term, and those terms embed back into directed-cycle free terms for the free-boundary kernel decomposition.
In the broader chain, cyclic extraction is the combinatorial half of showing every $1$-cycle is homologous to an integer multiple of the fundamental loop, completing the generation side of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. That isomorphism is the strict T8 target in the forcing chain (three spatial dimensions via the circle's first homology). The module still notes that full surjectivity of the integer comparison map needs a simplicial prism or subdivision operator Mathlib does not yet supply; this definition only closes the forward-family packaging step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.