prismHomotopy
plain-language theorem explainer
A continuous homotopy between maps F₀, F₁ : X → Y yields a chain homotopy between the induced singular chain maps. Algebraic topologists cite this as the prism construction behind homotopy invariance of singular homology (Hatcher 2.10). The definition packages the prism operator into Mathlib's Homotopy structure, verifying the chain-homotopy identity via the degree-zero and positive-degree prism lemmas.
Claim. Given continuous maps $F_0, F_1 : X \to Y$ and a homotopy $H$ from $F_0$ to $F_1$, there is a chain homotopy between the induced maps of singular chain complexes $C_*(X;\mathbb{Z}) \to C_*(Y;\mathbb{Z})$, built from the prism operator on simplices.
background
Singular homology is computed from the singular chain complex $C_*(X;\mathbb{Z})$, whose degree-$n$ group is free on continuous maps $\Delta^n \to X$. A continuous map $f : X \to Y$ induces a chain map by postcomposition; here those induced maps are written on the coproduct presentation of the chain groups.
A chain homotopy between two chain maps $f_\sharp$ and $g_\sharp$ is a degree-$+1$ family of maps $P$ satisfying $\partial P + P\partial = g_\sharp - f_\sharp$. The classical geometric source is the prism operator: subdivide $\Delta^n \times I$ into $(n+1)$-simplices via affine maps that send vertices of $\Delta^{n+1}$ to the bottom and top faces of the prism. The module builds those prism maps and the associated operator on chains.
Upstream, the identities $\partial P = (F_1)\sharp - (F_0)\sharp$ in degree $0$ and $\partial P + P\partial = (F_1)\sharp - (F_0)\sharp$ in positive degrees are already proved on generators. This definition assembles them into Mathlib's abstract Homotopy structure between the two singular chain maps.
proof idea
The construction fills Mathlib's Homotopy record. The only nonzero component of the homotopy is in bidegree $(i,i+1)$: the negative of the prism operator applied to the continuous homotopy, transported by eqToHom when the indices match; otherwise zero.
The zero field is immediate from the dif_neg branch. The comm field splits on degree. In degree $0$, rewrite the abstract dNext/prevD formulas, insert the prism operator via dif_pos, and reduce to the upstream identity prism_chain_homotopy_zero, finishing with abel. In degree $n+1$, the same pattern uses both diagonal components and reduces to prism_chain_homotopy_succ, again closing by abel.
why it matters
This is the bridge from geometric homotopies of spaces to algebraic homotopies of singular chain complexes. Downstream it is the ingredient in homotopic_maps_induce_same_homology (Hatcher, Theorem 2.10: homotopic maps induce the same map on $H_n(-;\mathbb{Z})$), in chainHomotopyEquiv (a homotopy equivalence of spaces induces a homotopy equivalence of singular chain complexes), and in isIso_homology_map_of_homotopyEquiv (the forward map of a homotopy equivalence is an isomorphism on singular homology).
In the Recognition Science foundation layer this supplies the standard singular-homology toolkit used when comparing topological models of the recognition complex. It does not itself invoke the forcing chain (T0–T8), the J-cost, or the phi-ladder; it is pure algebraic topology scaffolding that those geometric arguments can cite once spaces and maps are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.