prism
plain-language theorem explainer
The i-th prism map is the continuous affine map Δ^{n+1} → Δ^n × I that sends the first i+1 vertices of the domain to the bottom face (height 0) and the remaining vertices to the top face (height 1). Its second coordinate is the sum of barycentric weights strictly above index i. Anyone assembling singular prism operators, cone fillings, or circle H₁ generators cites this map. The definition only packages the face map with the already-proved continuous height function.
Claim. For each index $i \in \{0,\ldots,n\}$ there is a continuous map $\mathrm{prism}_i:\Delta^{n+1}\to\Delta^n\times I$ given on barycentric coordinates by $x\mapsto\bigl(\mathrm{face}_i(x),\,t_i(x)\bigr)$, where $t_i(x)=\sum_{k>i}x_k\in I=[0,1]$ and $\mathrm{face}_i$ is the affine map induced by the predecessor-above operator on vertices. On vertices it sends $e_0,\ldots,e_{n+1}$ to $v_0,\ldots,v_i,w_i,\ldots,w_n$ with $v_j=(e_j,0)$ and $w_j=(e_j,1)$.
background
Singular prism operators are the standard geometric device that turns a homotopy of singular simplices into a chain homotopy. The domain is the standard simplex $\Delta^{n+1}\subset\mathbb{R}^{n+2}$ (barycentric coordinates summing to 1); the codomain is the product of $\Delta^n$ with the unit interval $I=[0,1]$.
The second coordinate of the map is the height function that sums all barycentric coordinates strictly above the chosen index $i$. Nonnegativity and the bound $\le 1$ put that height in $I$; continuity of the finite sum is elementary. The first coordinate is the standard face map of the simplex category induced by the predecessor-above embedding of vertex sets.
The local module builds these continuous prism maps (and their faces) as the geometric substrate for later singular-chain arguments about winding on the circle.
proof idea
Definition, not a proof. The underlying function is the product of two pieces: the continuous simplex face map stdSimplex.map along the predecessor-above vertex map, and the subtype package of the height function (the sum of barycentric coordinates above $i$) together with the membership lemma that places that sum in $I$. Continuity of the product is the product of stdSimplex.continuous_map with the subtype-marked continuity of the height function.
why it matters
This is the geometric atom used throughout the circle-winding chain. Downstream theorems that close Mathlib's computation of $H_1(S^1;\mathbb{Z})$ invoke it as the raw prism filling: oriented cyclic families admit explicit prism fillings; zero-winding closed singular 1-cycles bound via cone/prism constructions; directed-cycle generation reduces to prism boundaries. Without a continuous prism map $\Delta^{n+1}\to\Delta^n\times I$, those generation and bounding statements have no geometric carrier.
In the Recognition foundation layer the map is pure algebraic topology infrastructure: it does not itself encode J-cost, $\varphi$, or the forcing chain, but it supplies the singular-homology toolkit those later arguments rely on when they identify winding with integer homology classes on the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.