singularEdgeListChain
plain-language theorem explainer
Maps a finite list of singular 1-simplices on S¹ to the free singular 1-chain that is their unweighted sum (each edge coefficient 1). Anyone building explicit cycle representatives from edge lists cites this constructor. The body is a recursive free-module sum: empty list to zero, cons to free generator plus the remainder.
Claim. Given a finite list of singular $1$-simplices on $S^1$, form the free $\mathbb{Z}$-chain equal to the sum of the corresponding free generators, each with coefficient $1$. The empty list maps to the zero chain.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$ and proves that displacement kills boundaries, yielding the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$. The free singular $1$-chain module is the free $\mathbb{Z}$-module on those simplices. Free generators are the standard basis elements of that module.
Downstream, a cyclic edge-list term packages a list of such simplices, a global integer coefficient, and a certified cycle whose free-chain image equals that coefficient times the listed edge sum. This definition supplies that listed edge sum before the global scalar is applied.
proof idea
Definition by recursion on the list. The empty list is the zero free chain. On a cons cell, take the free generator of the head simplex and add the recursively computed chain of the tail. No lemmas are invoked; it is pure free-module arithmetic.
why it matters
Concrete cycle bookkeeping for the circle winding chain. Parent consumers include the cyclic edge-list term structure (whose chain_eq equates a certified cycle's free image to a coefficient times this list-chain) and the list-of-terms free-chain sum that aggregates several such pieces.
Together with simplex displacement and the kills-boundaries identity, these edge-list chains support explicit representatives for the winding homomorphism on $1$-cycles, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity (generation by the fundamental loop) remains open and needs a simplicial prism/subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.