coneCircleMapOfContinuous_face_zero
plain-language theorem explainer
The δ₀ face of the continuous cone over a path γ : I → S¹ equals the terminal-return side of that cone. Anyone building free boundaries of singular 2-simplex cones cites this before cancelling side terms in a prism. The proof is pointwise extensionality plus the already-proved face-map identity for the pointwise cone.
Claim. Let $\gamma : I \to S^1$ be continuous, and assume the pointwise cone of $\gamma$ on the standard $2$-simplex is continuous. Then the $\delta_0$ face of the resulting singular $2$-simplex equals the terminal-return side of the cone over $\gamma$.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices of $\mathrm{TopCat.sphere},1$, and proves the chain-level fact that simplex displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$.
The cone over a path $\gamma$ is built by lifting angles through the circle cover, forming a pointwise map on the standard $2$-simplex, and packaging it as a singular $2$-simplex once continuity at the apex is supplied. Faces of a singular $2$-simplex are precomposition with the standard face maps of $\Delta^2$. The terminal-return side is the concrete singular $1$-simplex whose values are the projected linear interpolants of the lifted endpoint angles of $\gamma$.
Upstream, the pointwise identity already states that restricting the cone along the $0$-th face map recovers that terminal-return side.
proof idea
One-line term proof: extend equality of continuous maps by evaluating at an arbitrary point of the standard $1$-simplex, then apply the pointwise face restriction already proved for the cone. Continuity packaging drops out after the face is taken, so no further analytic work appears.
why it matters
Supplies the open-edge $\delta_0$ face formula used by the free-boundary shell theorems for cones: the boundary of the cone over an edge (or path) is terminal-return side minus constant apex side plus the original edge. Those shells are the finite-prism bricks toward the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The split-injective half already follows from the kills-boundaries identity together with the fact that winding sends the once-around generator to $1$. The doc-comment flags this lemma as the face formula needed before side terms cancel in a multi-edge prism. Pure singular-homology infrastructure in the foundation layer, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.