sUnit
plain-language theorem explainer
Canonical generator of the free ℤ-module on small singular n-simplices for a two-set cover (U,V). Algebraic topologists cite it when relating the small-chain complex to ordinary singular chains via inclusion. The body is a one-line specialization of the generic coproduct unit map to the small-simplex index type.
Claim. Fix sets $U,V \subseteq X$ and $n \in \mathbb{N}$. For each small singular $n$-simplex $t$ (an ordinary singular $n$-simplex whose image lies in $U$ or in $V$), write $sUnit(U,V,n,t)$ for the standard basis element of the free $\mathbb{Z}$-module on those small simplices corresponding to the index $t$.
background
This module builds the singular Mayer–Vietoris apparatus for a cover by two sets $U,V \subseteq X$. Ordinary singular chains are the free $\mathbb{Z}$-module on all continuous maps $\Delta^n \to X$. The small chain group restricts the generators to those simplices whose image lies entirely in $U$ or entirely in $V$ (the predicate Small).
The index type of degree-$n$ small chains is the subtype of ordinary singular $n$-simplices satisfying that smallness condition. The small chain group itself is the coproduct $\coprod \mathbb{Z}$ over that index type, i.e. the free $\mathbb{Z}$-module on small simplices. The generic construction unitOf sends an index $i$ to the image of $1 \in \mathbb{Z}$ under the coproduct inclusion at $i$.
sUnit is exactly that generator, specialized to the small-simplex index.
proof idea
One-line wrapper: apply the generic free-module generator unitOf with index type equal to the small-simplex indices SIdx U V n, evaluated at the given small simplex $t$. No further rewriting or lemmas.
why it matters
This generator is the atomic object that the small-to-ordinary inclusion acts on. Downstream, sInc_sUnit identifies the image of sUnit t with the ordinary singular generator of the underlying simplex; sInc_mem_smallSpan then shows every small chain lands in the span of small ordinary generators; and exists_sInc_eq recovers a small-chain preimage for every element of that span.
In the Recognition Science foundation stack this is pure singular-homology scaffolding: it supports the Mayer–Vietoris exact sequence used to control topological invariants of recognition complexes, not a physics claim by itself. It does not touch the forcing chain (T0–T8), the J-cost, or the phi ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.