coneCircleMapOfContinuous_face_one
plain-language theorem explainer
The middle face of the continuous cone over a path γ on S¹ is the constant singular edge at the apex γ(0). Anyone computing the free singular boundary of a cone 2-simplex cites this identity. The proof is pointwise extensionality plus the already-proved face restriction of the cone point map.
Claim. Let $\gamma : I \to S^1$ be continuous. If the pointwise cone $x \mapsto \mathrm{coneCirclePoint}(\gamma,x)$ on the standard $2$-simplex is continuous, then the face $\delta_1$ of the packaged singular $2$-simplex equals the constant singular $1$-simplex at $\gamma(0)$.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that 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$. That identity, with the generator evaluation, gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The cone construction builds a candidate singular $2$-simplex over a path $\gamma$ by lifting angles, forming a linear cone in the cover, and projecting back via the trigonometric covering. coneCirclePoint is that pointwise map; coneCircleMapOfContinuous packages it as a TwoSimplex once continuity at the apex is supplied. Faces of a $2$-simplex are compositions with the standard face maps of $\Delta^2$; face index $1$ is the side opposite the middle vertex.
Upstream, coneCirclePoint_faceMap_one already shows the pointwise restriction along $\delta_1$ is constantly $\gamma(0)$, via the lifted-angle face identity and the fact that the path lift recovers $\gamma$ at time $0$.
proof idea
Term-mode proof by pointwise equality of continuous maps. Extend both sides over a point $x$ of $\Delta^1$, unfold the constant singular edge, and apply coneCirclePoint_faceMap_one at $x$. No new analytic work: continuity of the cone is an assumption used only to form the packaged $2$-simplex, and the face identity is inherited from the pointwise cone.
why it matters
Needed to evaluate free singular $2$-boundaries of cones. Downstream, singularTwoBoundaryFree_freeMk_coneCircleMap states that the boundary of the cone over an arbitrary singular edge is terminal-return side minus constant apex side plus the original edge; the constant-apex term is exactly this face. The path-parametric sibling singularTwoBoundaryFree_freeMk_coneSingularTwoSimplexOfPath uses the same identity as the primitive finite-prism brick.
In the module narrative, the zero-winding loop theorem is the special case where terminal-return equals the constant apex side, so the alternating boundary collapses. That feeds the chain-level "winding kills boundaries" story and the left-inverse half of the integer comparison $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. It does not touch the generation/surjectivity half, which still needs a simplicial prism or subdivision operator absent from Mathlib singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.