genUnit
plain-language theorem explainer
Canonical basis element of the free singular n-chain group attached to one singular n-simplex. Anyone writing Mayer–Vietoris, barycentric subdivision, or small-chain arguments in this development cites it as the unit generator. The body is a one-line specialization of the free-module unit map to the simplex index set.
Claim. For a space $X$, degree $n\in\mathbb{N}$, and singular $n$-simplex $s$ of $X$, the associated generator is the image of $1\in\mathbb{Z}$ under the canonical inclusion of the $s$-summand into the free $\mathbb{Z}$-module $C_n(X;\mathbb{Z})=\bigoplus_{\sigma}\mathbb{Z}$ of singular $n$-chains.
background
Singular chains here are the free $\mathbb{Z}$-module on the set of continuous maps $\Delta^n\to X$. That index set is written as the degree-$n$ object of the singular simplicial set of $X$; the chain group is the coproduct $\coprod_{\sigma}\mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$.
The upstream unit map builds, for any index type $\kappa$, the standard generator of the $\kappa$-summand: the image of $1\in\mathbb{Z}$ under the coproduct inclusion at that index. The present definition simply instantiates that construction at $\kappa=$ singular $n$-simplices of $X$.
The ambient module is the Mayer–Vietoris / subdivision layer of the foundation stack: open covers, small simplices (image in $U$ or $V$), and the submodule they span inside ordinary singular chains.
proof idea
Pure definitional wrapper. Apply the free-module unit constructor at the index equal to the given singular simplex; no further rewriting or induction.
why it matters
This generator is the atom from which the small-chain submodule is spanned: that submodule is defined as the $\mathbb{Z}$-span of all such units on simplices that are small relative to an open cover $(U,V)$. Downstream lemmas identify the small-group inclusion on a small unit with this generator, place the generator in the small span when the simplex is small, and run free induction on chains by reducing to the unit case.
That unit case is exactly how uniform smallness is proved: every chain admits a subdivision iterate landing in the small span, by inducting on free generators and subdividing each simplex. Sphere-side results also evaluate the augmentation and boundary on this generator. In the broader Recognition foundation this is ordinary singular homology scaffolding (not a T0–T8 forcing step), needed so later geometric or topological arguments can quote a clean Mayer–Vietoris sequence over $\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.