coneSingularTwoChainOfPathFamily
plain-language theorem explainer
Packages a finite family of continuous paths on the circle into one singular 2-chain by summing the individual cone simplices. Homology and prism arguments cite it as the multi-edge cone chain whose boundary must telescope. The body is a free-module sum of the single-path cone constructors.
Claim. For $k\in\mathbb{N}$ and a family $\gamma:\mathrm{Fin}\,k\to C(I,S^1)$ of continuous paths on the circle, form the singular $2$-chain $\sum_i [C(\gamma_i)]$ in the free $\mathbb{Z}$-module on singular $2$-simplices of $S^1$, where $C(\gamma_i)$ is the cone of $\gamma_i$ onto its initial point.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact behind a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$.
SphereOne is the carrier of TopCat.sphere 1. A singular $2$-simplex is a continuous map $\Delta^2\to S^1$. The free chain group singularTwoChainFree is the free $\mathbb{Z}$-module on those simplices.
The single-path brick coneSingularTwoSimplexOfPath cones an arbitrary unit-interval path $\gamma$ to its initial point, yielding one singular $2$-simplex. The present definition sums those bricks over a finite indexed family, producing the multi-edge cone chain used by prism and cyclic-family arguments.
proof idea
Definitional one-liner: sum, over $i:\mathrm{Fin},k$, the free-module generators of the single-path cones coneSingularTwoSimplexOfPath (γ i). No further lemmas; the sum is taken in singularTwoChainFree.
why it matters
Supplies the algebraic multi-edge cone whose boundary is computed by singularTwoBoundaryFree_coneSingularTwoChainOfPathFamily: terminal-return sides minus constant apex sides plus base path edges. That identity is the target whose side terms must telescope in the multi-edge prism.
It also feeds OrientedCyclicFamilyTerm, the concrete oriented cyclic family of singular $1$-edges used when assembling closed walks. In the module narrative this is scaffolding toward the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (every $1$-cycle homologous to an integer multiple of the fundamental cycle), which needs simplicial prisms beyond Mathlib's current singular homology API. The kills-boundaries half already uses the single $2$-simplex telescoping; this family cone is the finite-sum extension of that brick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.