prism_comp_face_cancel
plain-language theorem explainer
Adjacent prism maps agree on their shared face: prism_i composed with face_{i+1} equals prism_{i+1} composed with the same face. This supplies the interior cancellation in ∂P for the prism chain homotopy of singular homology. Anyone proving homotopy invariance of singular homology via prisms cites it. The proof is pointwise ContinuousMap extensionality, reducing both simplex and height coordinates to Fin arithmetic on predAbove/succAbove.
Claim. For each index $i \in \{0,\ldots,n\}$, the adjacent prism maps agree after composition with their shared face: $\mathrm{prism}_{i}\circ\mathrm{face}_{i+1}=\mathrm{prism}_{i+1}\circ\mathrm{face}_{i+1}$ as continuous maps on the standard simplex (product of a simplex map with a height coordinate in the unit interval).
background
Module Foundation.SingularPrism builds the prism operator that turns a continuous homotopy $F:X\times I\to Y$ into a chain homotopy on singular chains. A prism map sends an $n$-simplex in $X$ to an $(n+1)$-chain in $Y$ by sweeping the simplex along the homotopy parameter; combinatorially it is assembled from face insertions succAbove/predAbove on Fin and a height function prismSndFun (the second, unit-interval coordinate of the prism).
The boundary of a prism expands as an alternating sum of face composites. Adjacent terms share a common face index; those composites must cancel pairwise so that only the two endpoint chain maps $F_0$ and $F_1$ survive. The present identity is exactly that pairwise agreement: $\mathrm{prism},i\circ\mathrm{face}(i+1)=\mathrm{prism}(i+1)\circ\mathrm{face}(i+1)$.
Local supporting facts include the coercion lemmas for predAbove/succAbove and the interaction of prismSndFun with succAbove (used to compare height sums after face insertion).
proof idea
Term-style proof via ContinuousMap.ext, then Prod.ext on the prism codomain (simplex factor × unit-interval factor).
On the simplex factor: both sides are stdSimplex.map composites of predAbove with the same succAbove. Apply a map-map commutation lemma and check the underlying Fin functions pointwise: after unfolding coe_predAbove, coe_succAbove, and the castSucc/succ value formulas, a split_ifs; omega case split on the cut index closes the equality.
On the height factor: rewrite both sides by the lemma that pushes prismSndFun through succAbove, then compare the filtered Finset sums that define the height. Filter membership reduces again to Fin.lt_def plus the same succAbove coercions; another split_ifs; omega finishes it.
why it matters
This is the algebraic cancellation step inside the prism boundary. Downstream, prism_chain_homotopy_succ quotes it while proving the positive-degree chain-homotopy identity $\partial\circ P+P\circ\partial=(F_1)\sharp-(F_0)\sharp$. That identity is the engine behind isIso_homology_map_of_homotopyEquiv: the singular-homology map induced by a homotopy equivalence is an isomorphism.
In the Recognition foundation stack, homotopy invariance of singular homology is part of the topological toolkit that underwrites geometric constructions (circle windings, singular chains on configuration spaces) rather than a direct T0–T8 forcing step. Closing the prism calculus cleanly keeps those later geometric arguments free of ad-hoc chain-level bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.