prism_comp_face_of_le
plain-language theorem explainer
When j ≤ i, the prism map at i+1 composed with face j equals the product face j × id_I composed with the prism at i. Anyone assembling the prism chain homotopy for singular homology cites this low-face commutation. The proof is pointwise ContinuousMap.ext: Fin case splits on succAbove/predAbove for the simplex factor, and a filtered sum identity for the interval coordinate.
Claim. Let $i \in \mathrm{Fin}(n+1)$ and $j \in \mathrm{Fin}(n+2)$ satisfy $j \le i^{\uparrow}$. Then $\mathrm{prism}(i+1) \circ \mathrm{face}(j^{\uparrow}) = (\mathrm{face}(j) \times \mathrm{id}_I) \circ \mathrm{prism}(i)$, as continuous maps from the standard $n$-simplex into $Y \times I$.
background
The module builds prism operators for singular chain homotopies. A prism map sends an $n$-simplex in $X$ to an $(n+1)$-simplex in $Y \times I$ by inserting a coordinate along the unit interval $I$, using face and degeneracy combinatorics on $\mathrm{Fin}$ indices together with a second-coordinate weight prismSndFun (the sum of barycentric coordinates above a cut).
Face maps $\mathrm{face},j$ are the standard inclusions of codimension-one faces of the standard simplex. The low-face regime is $j \le i$ (equivalently $j < i+1$ in the boundary bookkeeping). The companion high-face lemma treats $j > i$.
These identities are the combinatorial engine behind matching terms of $\partial P$ against $P\partial$ in the prism chain-homotopy formula, so that $\partial P + P\partial$ collapses to the difference of the endpoint chain maps.
proof idea
Reduce the Fin inequality to a natural-number comparison. Apply ContinuousMap.ext and split the product with Prod.ext.
On the simplex factor: rewrite both sides as successive stdSimplex.map applications and invoke the general commutation lemma map_map_eq_map_map, checking pointwise on Fin that predAbove (i+1) after succAbove (j↑) equals succAbove j after predAbove i. The equality is Fin.ext plus split_ifs; omega on the coe formulas for predAbove/succAbove.
On the interval factor: reduce via prismSndFun_map_succAbove to a filtered Finset sum, then Finset.filter_congr with the same split_ifs; omega comparison of index inequalities.
why it matters
This is one of the two face-commutation legs (low faces) needed to prove the prism chain-homotopy identity in positive degree, prism_chain_homotopy_succ: $\partial\circ P + P\circ\partial = (F_1)\sharp - (F_0)\sharp$. That identity is the algebraic content of homotopy invariance for singular chains.
Downstream it supports isIso_homology_map_of_homotopyEquiv: the singular-homology map induced by a homotopy equivalence is an isomorphism. In the Recognition foundation stack this supplies the topological invariance layer under singular homology, so later geometric and forcing constructions can treat homology as a homotopy-invariant invariant rather than a raw singular-complex artifact.
The doc-comment ties the identity directly to matching $(i,j)$ terms of $\partial P$ with $j < i+1$ against $P\partial$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.