singularZeroChainFree
plain-language theorem explainer
The free ℤ-module on singular 0-simplices of the circle S¹, serving as an explicit model of C₀(S¹;ℤ). Anyone working the free-boundary or cycle-lifting arguments in the circle winding chain cites it as the codomain of the explicit 1-boundary. The body is a one-line abbreviation: free ℤ-module on the type of actual singular 0-simplices.
Claim. Write $C_0^{\mathrm{free}}(S^1;\mathbb{Z})$ for the free $\mathbb{Z}$-module on the set of singular $0$-simplices of the topological circle $S^1$ (i.e., continuous maps $\Delta^0\to S^1$). As an object of the category of $\mathbb{Z}$-modules this is $\mathrm{Free}_{\mathbb{Z}}(\mathrm{Sing}_0(S^1))$.
background
The module CircleWindingChain lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact needed for a homology invariant. Singular $0$-simplices are points of $S^1$ in the singular simplicial set: continuous maps $\Delta^0\to S^1$, written here as the type of $0$-simplices of $\mathrm{Sing}(S^1)$.
Working with Mathlib's raw singular chain groups is awkward for finite-support cancellation. The standard move is to replace $C_0(S^1;\mathbb{Z})$ by the free module on those $0$-simplices, so a chain is a finite integer combination of points and the boundary of a directed edge is literally terminal minus initial.
Upstream, SingularZeroSimplex is exactly that type of singular $0$-simplices of TopCat.sphere 1. The free-module functor then produces the object used as explicit $C_0$ throughout the free-boundary calculus.
proof idea
One-line definitional abbreviation: apply the free $\mathbb{Z}$-module functor in ModuleCat to the type of singular $0$-simplices of $S^1$. No proof obligations; the body is (ModuleCat.free ℤ).obj SingularZeroSimplex.
why it matters
This object is the explicit free $C_0$ that makes boundary telescoping computable. Downstream, singularOneBoundaryFree is the map $C_1^{\mathrm{free}}\to C_0^{\mathrm{free}}$ sending each directed edge to terminal minus initial. Cyclic free-boundary vanishing theorems (cyclicEdgeFamily_freeBoundary_zero, cyclicOrientedFamily_freeBoundary_zero) prove that closed edge-walks are cycles in this module, which is what lifts a closed walk to a degree-$1$ cycle.
The isomorphism singularZeroChainFreeIso identifies Mathlib's raw $C_0(S^1;\mathbb{Z})$ with this free module, so free-module boundary computations transport back to the singular chain complex. Together with the module's winding-kills-boundaries identity and the fundamental-loop normalization, this supports the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation/surjectivity half still needs a prism or subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.