gen_prismOp
plain-language theorem explainer
On a singular n-simplex generator, the prism operator equals the explicit signed sum of prism simplices. Algebraic topologists cite it when reducing chain-homotopy identities to generators. The proof is the coproduct universal property: the operator was defined by extending that signed sum, so evaluation on a summand is immediate.
Claim. Let $X,Y$ be topological spaces, $H\colon I\times X\to Y$ continuous, and let $\mathrm{prisms}$ be a family of continuous prism-decomposition maps $\Delta^{n+1}\to\Delta^n\times I$. For every singular $n$-simplex $s$ of $X$, the prism operator applied to the generator of $s$ equals the signed sum $\sum_i (-1)^i[\mathrm{prismSimplex}_i(s)]$ in $C_{n+1}(Y)$.
background
Singular chain groups here are free $\mathbb{Z}$-modules on continuous maps $\Delta^n\to X$. The index type of degree-$n$ generators is the set of singular $n$-simplices. The generator map sends each simplex to its basis element in the coproduct $\coprod_\sigma\mathbb{Z}$.
A homotopy $H\colon I\times X\to Y$ induces a prism operator $P\colon C_n(X)\to C_{n+1}(Y)$. On a generator one subdivides the prism $\Delta^n\times I$ into $n+1$ singular $(n+1)$-simplices and takes the alternating sum; that generator-level map is the signed prism sum. The full operator is the unique $\mathbb{Z}$-linear extension of that sum via the coproduct universal property.
The module builds Hatcher's prism argument for homotopy invariance of singular homology in Lean, using Mathlib singular sets and chain complexes.
proof idea
One-line term proof by the coproduct (Sigma) description map. The prism operator is defined as the unique morphism out of the free chain group whose component on each generator is the signed prism sum. Applying the inclusion of a generator and composing is therefore definitionally that component, which is exactly the generator-level prism sum. No combinatorial face identities are needed at this step.
why it matters
This is the generator-evaluation lemma for the prism operator. Downstream, the degree-zero chain-homotopy identity rewrites the composite of generator inclusion with the prism operator via this equality, then expands the one-term Fin sum. The positive-degree identity uses the same reduction under Sigma.hom_ext when checking $\partial P+P\partial=(F_1)\sharp-(F_0)\sharp$ on generators.
Those identities feed the theorem that a homotopy equivalence induces an isomorphism on singular homology with $\mathbb{Z}$ coefficients. In the Recognition foundation stack this is topological scaffolding: singular homology must be homotopy-invariant before higher geometric claims that quote homology can sit on a solid base. It is classical algebraic topology, not a T0–T8 forcing step, but it closes a proved link in the SingularPrism development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.