Pgen
plain-language theorem explainer
On a single singular n-simplex, the prism operator is the alternating sum of the (n+1)-simplices obtained by composing a cylinder map H:I×X→Y with a chosen prism decomposition of the standard simplex. Homotopy-invariance arguments for singular homology cite this generator formula before extending by linearity. The definition is exactly that signed sum of chain-group generators.
Claim. Let $X,Y$ be topological spaces, $H:I\times X\to Y$ continuous, and let $\mathrm{prisms}_i:\Delta^{n+1}\to\Delta^n\times I$ for $i=0,\ldots,n$ be continuous prism maps. For a singular $n$-simplex $s$ of $X$, the generator-level prism operator is the $\mathbb{Z}$-linear map $\mathbb{Z}\to C_{n+1}(Y;\mathbb{Z})$ sending $1$ to $\sum_{i=0}^{n}(-1)^i[\sigma_i]$, where $\sigma_i$ is the singular $(n+1)$-simplex of $Y$ built from $H$, $\mathrm{prisms}_i$, and $s$.
background
Singular chain groups here are the free $\mathbb{Z}$-modules on singular simplices: $\mathrm{Idx},X,n$ is the set of continuous maps $\Delta^n\to X$, and $C_n(X;\mathbb{Z})$ is the coproduct of a copy of $\mathbb{Z}$ over that index set. The generator map attaches the basis element of a given simplex.
The classical prism construction fills the cylinder $\Delta^n\times I$ by $n+1$ singular $(n+1)$-simplices. A family of maps $\mathrm{prisms}_i:\Delta^{n+1}\to\Delta^n\times I$ supplies that decomposition; composing with $H$ and the simplex $s$ produces singular simplices of $Y$.
This module builds the prism operator inside Lean’s singular-homology API so that continuous homotopies induce chain homotopies, the standard route to homotopy invariance of singular homology.
proof idea
Pure definition, not a proved identity. The body is the finite sum over $i\in\mathrm{Fin}(n+1)$ of $(-1)^i$ times the generator in $C_{n+1}(Y)$ of the singular simplex obtained by feeding $H$, the $i$-th prism map, and the input simplex $s$ into the prism-simplex constructor. No lemmas are applied; the expression is the classical alternating prism sum written in the ModuleCat language of the ambient chain groups.
why it matters
This is the generator clause of the prism operator. The full operator prismOp is the coproduct extension $\Sigma.\mathrm{desc}$ of this map, and gen_prismOp records that generators are sent exactly to this signed sum.
Downstream, the chain-homotopy identities in positive degree and in degree zero (prism_chain_homotopy_succ, prism_chain_homotopy_zero) expand prismOp on generators via this definition, then verify $\partial P+P\partial=(F_1)\sharp-(F_0)\sharp$. That is the algebraic engine of homotopy invariance for singular homology in the Recognition foundation stack.
Within RS this sits in the topological scaffolding that supports continuum limits and geometric forcing arguments; it is classical AT infrastructure rather than a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.