prism_comp_face_of_gt
plain-language theorem explainer
When a face index sits strictly above a prism index, the prism map composed with that high face factors through the one-dimension-lower prism via face×id. Anyone building the singular prism chain homotopy cites this to match ∂P terms against P∂. The proof is pointwise ContinuousMap.ext: Fin arithmetic on the simplex factor and a filtered sum identity on the interval factor, both discharged by omega.
Claim. Let $i\in\mathrm{Fin}(n+1)$ and $j\in\mathrm{Fin}(n+2)$ satisfy $i^{\uparrow}<j$, where $i^{\uparrow}$ is the cast-successor embedding into $\mathrm{Fin}(n+2)$. Write $P_k$ for the topological prism map at slot $k$ and $d^{\ell}$ for the corresponding face map of the standard simplex. Then $P_{i^{\uparrow}}\circ d^{j+1}=(d^j\times\mathrm{id}_I)\circ P_i$ as continuous maps on the product of the standard simplex with the unit interval.
background
Module Foundation.SingularPrism builds the classical prism operator that witnesses homotopy invariance of singular homology with $\mathbb{Z}$ coefficients. A prism map $P_i$ sends an $n$-simplex times the unit interval $I$ into an $(n+1)$-simplex by inserting a coordinate slot at index $i$; its second (interval) component is the filtered sum prismSndFun. Face maps $d^j$ are the standard affine inclusions of the boundary of the standard simplex, implemented via Fin.succAbove / Fin.predAbove on barycentric coordinates.
The chain-homotopy identity $\partial P+P\partial=F_1^{\sharp}-F_0^{\sharp}$ expands into many face–prism composites. Those with face index strictly above the prism index must cancel against the prism applied one dimension down; that is exactly the relation proved here. The dual low-face case is handled by a sibling lemma.
Upstream Fin arithmetic (lt_def, coe_succAbove, coe_predAbove) supplies the concrete inequalities used in the case splits; composition is ordinary continuous-map composition on the product space.
proof idea
Reduce both sides by ContinuousMap.ext and split the product with Prod.ext.
On the simplex factor, the claim is equality of two composites of stdSimplex.map along predAbove and succAbove. Apply the naturality lemma map_map_eq_map_map and check the underlying Fin functions pointwise: after unfolding coe_predAbove / coe_succAbove and the cast/succ value formulas, every branch of the split_ifs is an inequality discharged by omega (using the hypothesis $i^{\uparrow}<j$).
On the interval factor, rewrite with prismSndFun_map_succAbove, expand prismSndFun as a filtered sum, and apply Finset.sum_congr. The filter predicate again reduces to Fin inequalities settled by omega. The second component of the product is then a pure Subtype.ext of that equality.
why it matters
This is one of the face-commutation bricks inside Stage 3 of the singular prism construction. Downstream, prism_chain_homotopy_succ assembles all such identities into the chain-level relation $\partial\circ P+P\circ\partial=(F_1){\sharp}-(F_0){\sharp}$ on positive-degree singular chains. That identity is the engine behind isIso_homology_map_of_homotopyEquiv: the map on singular homology induced by a homotopy equivalence is an isomorphism.
In the Recognition Science foundation stack this is classical algebraic-topology scaffolding, not a forcing-chain step (T0–T8). It underwrites homotopy invariance of the singular complex that later interfaces with the discrete eight-tick and recognition-composition layers. Without the high-face commutation, the prism operator would fail to be a chain homotopy and the homology isomorphism would not go through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.