prismSimplex
plain-language theorem explainer
Builds the singular (n+1)-simplex obtained by feeding an n-simplex through a continuous homotopy along a chosen prism map Δ^{n+1} → Δ^n × I. Algebraic topologists cite it as the generator-level brick of the prism operator. The body is pure ContinuousMap composition, then reindexed by the singular-set equivalence.
Claim. Given a continuous homotopy $H: I \times X \to Y$, a continuous prism map $\mathrm{pr}: \Delta^{n+1} \to \Delta^n \times I$, and a singular $n$-simplex $\sigma: \Delta^n \to X$, form the singular $(n+1)$-simplex of $Y$ by $t \mapsto H(\pi_2(\mathrm{pr}\, t),\, \sigma(\pi_1(\mathrm{pr}\, t)))$.
background
The module develops the classical prism operator that turns a continuous homotopy of spaces into a chain homotopy of singular chains, in the style of Hatcher §2.1. Singular $n$-simplices of a space $X$ are packaged as the index type Idx X n: the degree-$n$ objects of the singular simplicial set of $X$. The free $\mathbb{Z}$-module on that index set is the singular chain group.
A prism decomposition supplies continuous maps $\mathrm{pr}: \Delta^{n+1} \to \Delta^n \times I$ that cut the product of an $n$-simplex with the unit interval into $(n+1)$-simplices. Given a homotopy $H: I \times X \to Y$ and a singular simplex $\sigma$ of $X$, one must push $\sigma$ forward along $H$ after pairing with the $I$-coordinate of $\mathrm{pr}$. That single pushed simplex is exactly what this definition records.
Sibling maps (prism, face, prismSndFun) handle the geometric faces and the second-factor projection; this declaration is the pure generator-level pushforward.
proof idea
Definition by composition, not a proof. Read the singular $n$-simplex $s$ as a continuous map $\Delta^n \to X$ via the singular-set equivalence, form the product map with $\mathrm{id}_I$, precompose the prism map $\mathrm{pr}$, swap factors so the pair lands in $I \times X$, postcompose the homotopy $H$, and transport the resulting continuous map $\Delta^{n+1} \to Y$ back to an index in Idx Y (n+1). No lemmas are invoked beyond ContinuousMap composition and the singular-set equivalence.
why it matters
This is the atomic generator map underneath the prism operator. Downstream, Pgen forms the signed sum $\sum_i (-1)^i [\mathrm{prismSimplex}, i]$ over a full prism decomposition; that operator is exactly the $P$ appearing in the chain-homotopy identities
$\partial P + P\partial = (F_1)\sharp - (F_0)\sharp$
proved in positive degree by prism_chain_homotopy_succ and in degree zero by prism_chain_homotopy_zero.
The alternating double-sum bookkeeping that collapses faces-of-prisms against prisms-of-faces is isolated in prism_sum_cancellation (Hatcher's Theorem 2.10 in abstract form). Within Recognition Science this sits in the Foundation layer: singular homology is infrastructure for later topological arguments, not itself a forcing-chain step (T0–T8). It closes the classical bridge from continuous homotopy of spaces to algebraic chain homotopy of singular chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.