coneSingularTwoSimplexOfPath
plain-language theorem explainer
Packages a continuous path on the circle into the singular 2-simplex given by the geometric cone to the path's initial point. Anyone building prism or cone chains for the winding homology invariant on S¹ cites this brick. The body is a one-line composition: continuous cone map, then transport into Mathlib's singular simplicial set.
Claim. Given a continuous path $\gamma:I\to S^1$, return the singular $2$-simplex on $S^1$ obtained by coning $\gamma$ to its initial point $\gamma(0)$.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$, and proves that displacement vanishes on boundaries. That vanishing, together with the once-around generator mapping to $1$, gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation half needs prism/subdivision operators; this definition is a primitive brick for those cones.
A singular $2$-simplex here is an element of the degree-$2$ object of Mathlib's singular simplicial set of $\mathrm{TopCat.sphere},1$. Upstream, the pointwise cone $\Delta^2\to S^1$ is already known continuous (continuous_coneCirclePoint: non-apex by coordinates, apex by squeeze). That continuity is packaged as a concrete continuous $2$-simplex map, then transported by the standard equivalence into the singular simplicial set.
proof idea
Pure definitional packaging, not a proof. Apply the continuous cone constructor to $\gamma$ with the already-proved continuity of the pointwise cone, then pass the resulting continuous map $\Delta^2\to S^1$ through the equivalence that turns concrete continuous simplices into singular simplices in Mathlib's simplicial set. No new analytic or algebraic work occurs here.
why it matters
This is the atomic cone brick for the path-parametric boundary shell. Downstream, the free generator on this simplex has boundary equal to the terminal-return edge minus the constant apex edge plus the original path as a singular $1$-edge. Finite sums of these cones give the family cone chain used as a prism operator on path families.
In the module narrative, the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs exactly such simplicial prisms; Mathlib does not yet supply a general subdivision operator, so these explicit cones close that gap for the circle. The construction sits in the Foundation layer that makes winding a homology invariant, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.