coneCirclePoint_faceMap_two
plain-language theorem explainer
On the base face δ₂ of Δ², the pointwise S¹-cone of a path γ recovers the singular 1-simplex built from γ. Anyone packaging a continuous cone 2-simplex whose base edge is the original path cites this. The proof unfolds both sides, rewrites via the angle-level face identity, and projects the path lift through the circle cover.
Claim. For every continuous path $\gamma:I\to S^1$ and every $x\in\Delta^1$, the pointwise cone of $\gamma$ at $\delta_2(x)\in\Delta^2$ equals the singular $1$-simplex associated to $\gamma$ evaluated at $x$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact behind the split injection $\mathbb{Z}\hookrightarrow H_1(S^1;\mathbb{Z})$.
SphereOne is the carrier of TopCat.sphere 1. A path $\gamma:I\to S^1$ has a real lift pathLift γ under the trigonometric covering trigCirclePoint, with pathLift_lifts stating $\mathrm{trig}\circ\mathrm{pathLift},\gamma=\gamma$. The singular $1$-simplex oneSimplexOfPath γ reparameterizes $\Delta^1$ to $I$ via the standard homeomorphism and composes with $\gamma$.
faceMap i is the affine topological face map $\Delta^1\to\Delta^2$ induced by the coface $\delta_i$. The pointwise cone coneCirclePoint γ sends $x\in\Delta^2$ to trigCirclePoint of a lifted cone angle built from $\gamma$; it is not yet a continuous map. The upstream angle identity coneLiftAngle_faceMap_two says that on $\delta_2$ the lifted cone angle equals the path lift of $\gamma$.
proof idea
Term-mode, three steps. Unfold coneCirclePoint and oneSimplexOfPath so both sides are trigCirclePoint applied to an angle. Rewrite the cone angle on the $\delta_2$ face by coneLiftAngle_faceMap_two, which replaces it by pathLift γ at the unit-interval reparameterization of $x$. Finish with congrFun (pathLift_lifts γ) at that point: the covering projection of the path lift is $\gamma$ itself, matching the unfolded right-hand side.
why it matters
This is the pointwise base-face identity needed to promote the cone to a singular $2$-simplex whose $\delta_2$ face is exactly the path simplex. The sole downstream consumer is coneCircleMapOfContinuous_face_two_path, which under a continuity hypothesis packages coneCirclePoint as a continuous map and concludes face (cone) 2 = oneSimplexOfPath γ by ext and this lemma.
In the module narrative that identity is part of the cone/prism toolkit supporting the kills-boundaries theorem simplexDisplacement_boundary (alternating face sum of displacement vanishes on every singular $2$-simplex). Together with the generator evaluation on the fundamental loop, that yields the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Continuity of the cone at the apex remains the open packaging step; this face restriction is independent of that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.