vertexCoeff
plain-language theorem explainer
Extracts the integer coefficient of a chosen singular 0-simplex from an explicit free 0-chain on S¹. Anyone working the free-module presentation of C₀(S¹;ℤ) or the incidence formula for ∂₁ cites this. The body is the underlying Finsupp evaluation map of the free ℤ-module.
Claim. For a free singular $0$-chain $z$ on $S^1$ (an element of the free $\mathbb{Z}$-module on singular $0$-simplices) and a singular $0$-simplex $v$, write $\mathrm{coeff}(z,v)\in\mathbb{Z}$ for the coefficient of $v$ in $z$.
background
The module develops the winding/displacement invariant on singular $1$-simplices of $\mathrm{TopCat.sphere},1$ and proves that displacement kills boundaries, the chain-level fact behind the split injection $\mathbb{Z}\hookrightarrow H_1(S^1;\mathbb{Z})$.
A singular $0$-simplex is a point of the singular simplicial set of $S^1$. The free $0$-chain group is the free $\mathbb{Z}$-module on those points (Mathlib ModuleCat.free), so every chain is a finitely supported integer combination of vertices. This definition is the coordinate projection onto one basis vector.
It sits under the free-module presentation used for the singular boundary $\partial_1:C_1\to C_0$ and the incidence-sum bookkeeping that identifies boundary coefficients with oriented endpoint counts.
proof idea
Definitional one-liner: apply the underlying function of the free-module element (z.toFun) at the vertex v. No lemmas; pure unpacking of ModuleCat.free / Finsupp coefficients.
why it matters
Local plumbing for the free $C_0$ presentation in the circle winding chain. Downstream, vertexBoundaryCoeff is defined as this coefficient of $\partial_1 c$, and theorems such as vertexBoundaryCoeff_freeMk and vertexBoundaryCoeff_eq_incidenceSum_holds reduce boundary coefficients to incidence sums over edge support. Those feed boundaryIncidenceSum_eq_zero_of_boundary_zero: free $1$-cycles have vanishing incidence at every vertex.
That bookkeeping supports the module's main goal: displacement as a homology invariant and the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via the once-around generator. It does not itself touch T0–T8 or the Recognition Composition Law; it is pure singular-chain infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.