coneCirclePoint_side_faces_eq_of_winding_zero
plain-language theorem explainer
Zero winding of a continuous path on the circle forces the two side faces of its pointwise cone to agree at every point of the standard 1-simplex. Anyone assembling the singular cone that witnesses null-homology of zero-winding 1-cycles will cite this. The proof is a one-line composition of the lift-endpoint identity with the lift-level side-face equality.
Claim. Let $\gamma:I\to S^1$ be continuous with winding number zero, and let $x$ be any point of the standard $1$-simplex $\Delta^1$. Then the pointwise cone of $\gamma$ takes the same value on the $0$-th and $1$-st faces of $x$: $\mathrm{cone}(\gamma)(\delta_0 x)=\mathrm{cone}(\gamma)(\delta_1 x)$.
background
The module lifts the path-level winding invariant of the circle to singular simplices on $S^1$ and proves that winding kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity, together with the fact that the fundamental loop has winding one, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Here the circle is the carrier of Mathlib's TopCat.sphere 1. Path winding is displacement divided by $2\pi$. The pointwise cone sends a point of the standard $2$-simplex to the image, under the trigonometric covering map, of a lifted cone angle built from a canonical real lift of $\gamma$. Face maps $\delta_i:\Delta^1\to\Delta^2$ are the affine maps induced by the cofaces of the simplex category.
Upstream, zero winding already forces the canonical lift endpoints to coincide. Separately, equal lift endpoints already force the two side faces of the pointwise cone to agree. The present statement simply specialises the second fact to the zero-winding case.
proof idea
One-line term proof. Apply the lift-level side-face equality (side faces of the pointwise cone agree once lift endpoints agree) to the path $\gamma$, feeding it the endpoint identity obtained from zero winding, and evaluate at the given point $x$ of $\Delta^1$. No further rewriting or case analysis is required.
why it matters
This is the zero-winding specialisation needed before packaging the pointwise cone as a continuous singular $2$-simplex. Downstream it is consumed by the continuous-map version: if the pointwise zero-winding cone is continuous, then its two side faces agree as singular $1$-simplices. That face equation is the geometric content of "a zero-winding $1$-simplex bounds," which feeds the chain-level kills-boundaries identity and therefore the left-inverse half of the comparison $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. Continuity of the cone at the apex remains the remaining analytic obligation isolated by the module; the present lemma is independent of that obligation and holds pointwise regardless.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.