uIdx
plain-language theorem explainer
Maps each singular n-simplex on the open set U to the corresponding small simplex in the (U,V)-subdivision complex by pushing it into X and recording that its image is small. Algebraic topologists building the Mayer–Vietoris chain maps cite it as the index-level inclusion of U-simplices into the small complex. The definition is a subtype pair: pushforward of the simplex together with the smallness witness.
Claim. For open sets $U,V \subseteq X$ and $n \in \mathbb{N}$, send each singular $n$-simplex $a$ on $U$ to the small-simplex index $\mathrm{uIdx}(a) = (\iota_*(a),\,\text{proof that }\iota_*(a)\text{ is }(U,V)\text{-small})$, where $\iota_*$ is the pushforward along $U \hookrightarrow X$.
background
This module builds a singular Mayer–Vietoris sequence for a cover $X = U \cup V$ by working with the free chain groups on small singular simplices: those whose image lies in $U$ or in $V$. The index type of the degree-$n$ small chain group is the subtype of ordinary singular $n$-simplex indices that satisfy the smallness predicate.
The pushforward along the subspace inclusion $U \hookrightarrow X$ takes a simplex valued in $U$ to an ordinary simplex of $X$. Upstream, that push is defined by applying the singular simplicial set functor to the continuous inclusion. Smallness of the pushed simplex is a separate lemma used here as a witness.
Locally one needs both the $U$-side and $V$-side index maps so that the two inclusions of ordinary chain groups into the small complex can be written as coproduct descriptions on generators.
proof idea
One-line subtype constructor. Apply the subspace pushforward to the $U$-simplex index, then pair it with the already-proved smallness fact for that pushforward. No further rewriting: the resulting pair inhabits the small-index subtype by definition.
why it matters
This is the generator-level bridge from $C_n(U)$ into the small complex $C_n^{U,V}$. Downstream, the chain map from $U$ is the coproduct description that sends each generator to the small generator at this index; unit and composition lemmas reduce to that description. Injectivity of the index map is immediate from injectivity of the pushforward on indices.
The middle exactness lemma of Mayer–Vietoris (a cancelling pair of $U$- and $V$-chains comes from a chain on $U \cap V$) uses these inclusions, so the index map is part of the scaffolding that makes the MV short exact sequence of chain complexes available in the Recognition foundation stack. It is pure singular-homology infrastructure rather than a T0–T8 forcing step, but it supports later geometric arguments that need relative homology of covers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.