orientedCyclicFamilyTermListChain
plain-language theorem explainer
Converts a finite list of oriented cyclic families (closed walks of signed singular edges) into an explicit free singular 1-chain on S¹. Anyone proving that boundary-free free chains decompose into cycles, or that those cycles generate the fundamental class, cites this packaging map. The body is a one-line composition: map each family to a directed-cycle term, then sum via the directed-cycle list chain.
Claim. Given a finite list $t_s$ of oriented cyclic family terms (each a length-$k$ closed walk of oriented singular $1$-edges with matching terminals and initials under cyclic rotation), form the free singular $1$-chain obtained by converting every term to a directed-cycle free term and taking the corresponding free-chain sum in $\mathbb{Z}[\mathrm{Sing}_1(S^1)]$.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$ and proves that displacement kills boundaries of $2$-simplices. The free module singularOneChainFree is $\mathbb{Z}$ on actual singular $1$-simplices of $\mathrm{TopCat.sphere},1$.
An oriented cyclic family term is a concrete finite sign-oriented closed walk: a natural number $k$, a map from $\mathrm{Fin},k$ to oriented singular edges, and a connectivity hypothesis that each edge's terminal equals the next edge's initial under cyclic rotation. Each such family packages as a directed-cycle free term via the sibling conversion map.
Upstream, the directed-cycle list chain is the recursive free sum of those directed pieces (empty list to $0$, cons by adding the head chain). The present definition simply feeds the converted list into that sum, so oriented families become ordinary free $1$-chains.
proof idea
One-line definitional wrapper. Map the input list with the conversion OrientedCyclicFamilyTerm.toDirectedCycleFreeTerm (itself the packaging of the family's oriented edges and connectivity into a directed-cycle free term), then apply directedCycleFreeTermListChain, which recursively sums the free chains of those directed pieces. No extra algebraic work.
why it matters
This is the concrete chain-level packaging used by the decomposition and generation halves of the circle $H_1$ story in this module. Downstream, freeBoundaryKernel_decomposesIntoOrientedCyclicFamilies_holds states that every free $1$-chain with vanishing free boundary equals the chain of some list of oriented cyclic families; the equality is literally identity with this map. Downstream again, fundamentalCycle_boundary_generates_of_orientedCyclicFamilies reduces global generation (every $1$-cycle homologous to an integer multiple of the fundamental cycle) to filling each concrete oriented family, again by routing through this list chain.
Together with the module's kills-boundaries identity for simplex displacement and the fact that path winding sends the once-around generator to $1$, these steps supply the generation half of the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module notes that full surjectivity still needs a simplicial prism/subdivision operator Mathlib does not yet provide; this definition is the intermediate language in which that generation argument is stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.