map_map_eq_self
plain-language theorem explainer
If a vertex map between finite types has a left inverse, pushing a real standard-simplex point forward and then back recovers the original point. Cited when checking that singular-prism face maps compose to the constant-height inclusions. The proof is a three-step rewrite: compose the maps, identify the vertex composite with id, then apply the identity pushforward.
Claim. Let $A,B$ be finite types and $f:A\to B$, $g:B\to A$ with $g(f(k))=k$ for all $k\in A$. For every point $x$ of the standard simplex $\Delta_A$ over $\mathbb{R}$, the barycentric pushforwards satisfy $\Delta(g)(\Delta(f)(x))=x$.
background
The ambient module builds a singular prism: a continuous map that thickens an $n$-simplex into a product with the unit interval, with face maps inserting the bottom and top slices. Points of the standard simplex $\Delta_S$ are nonnegative real weightings on a finite vertex set $S$ that sum to one. A function on vertices induces a pushforward $\Delta(f)$ that reindexes those weights.
The present lemma is the elementary retraction identity for that pushforward: a left inverse on vertices yields a left inverse on simplex points. It is pure Mathlib simplex algebra; the Recognition-Science forcing chain (T0–T8), $J$-cost, and $\varphi$-ladder do not enter the statement.
Downstream face-composition theorems reduce their first-component equalities exactly to an instance of this identity, with $f$ and $g$ the standard succAbove/predAbove vertex maps on Fin.
proof idea
Term-mode rewrite chain. First apply the Mathlib identity that the pushforward of a composite is the composite of pushforwards, evaluated at $x$. Second, discharge $g\circ f=\mathrm{id}$ by function extensionality from the pointwise left-inverse hypothesis. Third, apply the Mathlib fact that the pushforward along the identity vertex map is the identity on $\Delta_A$. No case splits or induction.
why it matters
Local plumbing for the singular-prism calculus in Foundation.SingularPrism. It is invoked by prism_comp_face_top and prism_comp_face_bot, whose docs state the geometric content: prism composed with the top (resp. bottom) face equals the product of the identity map with the constant height-$1$ (resp. height-$0$) section.
Those identities certify that the prism really interpolates between the two end simplices, which is the combinatorial prerequisite for any singular-homology or homotopy argument built on this prism. The lemma itself is not a Recognition landmark (not T5–T8, not RCL); it is infrastructure that keeps the topological side of the foundation free of ad-hoc simplex reindexing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.