singularEdgeListChain_ofFn
plain-language theorem explainer
For any finite family of singular 1-simplices on S¹ indexed by Fin k, the free C₁ chain built from List.ofFn of that family equals the sum of the free generators of each simplex. Homology and winding arguments that package cyclic edge lists cite this equality. The proof is induction on k, matching the recursive list chain against Fin.sum_univ_succ.
Claim. Let $e:\mathrm{Fin}\,k\to\{\text{singular }1\text{-simplices on }S^1\}$. Then the free singular $1$-chain associated to the list $\mathrm{List.ofFn}\,e$ equals $\sum_{i}\iota(e_i)$, where $\iota$ sends each simplex to its free generator in $C_1^{\mathrm{free}}(S^1)$.
background
This module lifts path-level winding and displacement on the circle to singular simplices of $\mathrm{TopCat.sphere},1$, and proves that displacement kills boundaries of singular $2$-simplices. That identity, with the once-around generator mapping to $1$, supplies the split-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 $S^1$ in degree $1$. The free $1$-chain on a finite list of such simplices is defined recursively: empty list maps to $0$; cons adds the free generator of the head to the chain of the tail. ModuleCat.freeMk is that free-generator inclusion.
The theorem converts the list presentation into an ordinary finite sum over Fin k, which is the form used when packaging cyclic families of edges into concrete cycle terms.
proof idea
Induction on $k$. Base $k=0$: both sides are zero by the empty-list clause of the list-chain definition and the empty Fin-sum, discharged by simp.
Successor step: rewrite List.ofFn via List.ofFn_succ, unfold the recursive list-chain definition, apply the inductive hypothesis to the tail family $i\mapsto e(i.succ)$, then rewrite the Fin-sum by Fin.sum_univ_succ. The head free generator plus the tail sum matches the successor Fin-sum.
why it matters
Downstream, cyclicSingularEdgeListTerm_of_cyclicFamily builds a concrete cyclic edge-list term from a Fin-indexed cyclic family by setting edges := List.ofFn e and coefficient $1$. This theorem identifies that list chain with the free sum of generators, so the certified cycle object's raw free-chain image is exactly the expected edge sum.
The same conversion feeds the oriented cyclic family engine (OrientedCyclicFamilyTerm): finite sign-oriented closed walks in singular $1$-simplices need list and sum presentations to agree when extracting winding or comparing to the fundamental class.
In the module's program this is bookkeeping on the way to a winding homomorphism on $1$-cycles left-inverse to the fundamental class (split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Surjectivity still needs a simplicial prism or subdivision operator not yet in Mathlib singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.