coneCirclePoint_faceMap_two_of_oneSimplex
plain-language theorem explainer
On the base face of the standard 2-simplex, the pointwise circle cone built from a singular edge recovers that edge exactly after projection to S¹. Algebraic topologists proving the winding-kills-boundaries identity for H₁(S¹) cite this face restriction. The argument reduces the cone angle on δ₂ to the path lift, applies the covering-map lift identity, and finishes by the standard Δ¹ ≃ I reparameterization.
Claim. For every singular $1$-simplex $f:\Delta^1\to S^1$ and every point $x\in\Delta^1$, the pointwise cone map associated to the path reparameterization of $f$, evaluated on the image of $x$ under the base-face inclusion $\delta_2:\Delta^1\hookrightarrow\Delta^2$, equals $f(x)$.
background
The 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 makes winding a homology invariant: for every singular $2$-simplex the alternating face sum of displacements vanishes. Together with evaluation on the once-around generator, that yields the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is a continuous map $f:\Delta^1\to S^1$. Reparameterizing $\Delta^1$ through the standard homeomorphism to the unit interval produces a path. The covering lift of that path is a continuous real-valued angle function; the trigonometric parametrization sends angles back to $S^1$, and the lift identity records that the composition recovers the original path.
The pointwise cone on $\Delta^2$ is the trigonometric image of a lifted cone angle built from the path. The base face $\delta_2$ is the face opposite vertex $2$, parameterized by the standard face map $\mathrm{Fin},2\to\mathrm{Fin},3$.
proof idea
Unfold the cone point to the trigonometric image of the lifted cone angle. Rewrite that angle on the base face by the sibling identity that identifies the cone angle on $\delta_2$ with the path lift of the reparameterized edge at the matching unit-interval point. A congruence from the covering lift identity then replaces the trigonometric image of the path lift by the path itself. Unfold the path reparameterization and simplify with the interval-to-simplex map to obtain $f(x)$.
why it matters
This is the pointwise engine behind the continuous-cone face theorem: if the zero-winding cone is continuous, its base face equals the original singular edge. That face identity lets the cone be treated as a genuine singular $2$-simplex whose boundary involves the given $1$-simplex, feeding the chain-level winding invariant and the kills-boundaries telescoping on $\Delta^2$.
In the Recognition foundation stack this supports the winding homomorphism on $1$-cycles as a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Continuity of the cone at the apex remains an explicit frontier noted on the cone definition; the present lemma is independent of that continuity and holds purely pointwise. The generation/surjectivity half still needs a simplicial prism or subdivision operator not yet in Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.