gen
plain-language theorem explainer
Canonical inclusion of a single singular n-simplex into the free abelian chain group C_n(X;Z). Anyone assembling singular chains, boundaries, or prism homotopies cites this generator map. The body is a one-line coproduct inclusion (Sigma.ι) picking the component labeled by the simplex.
Claim. For a topological space $X$, a degree $n\in\mathbb{N}$, and a singular $n$-simplex $a$ of $X$, there is a $\mathbb{Z}$-module morphism $\mathbb{Z}\to C_n(X;\mathbb{Z})$ sending $1$ to the basis element of the free abelian group on singular $n$-simplices that is labeled by $a$.
background
In this module the index set of degree-$n$ singular simplices is Idx X n: the set of continuous maps $\Delta^n\to X$, written as the $n$-simplices of the singular simplicial set of $X$. The degree-$n$ singular chain group Cgrp X n is the coproduct $\coprod_{\sigma\in\mathrm{Idx},X,n}\mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$, i.e. the free abelian group on those simplices.
Singular homology is built from these free groups together with face and prism operators. The present declaration supplies the standard basis inclusion: each simplex contributes a generator $1\cdot[a]$ inside that coproduct. Sibling abbreviations in the same file define the prism map $\Delta^{n+1}\to\Delta^n\times I$, face maps, and the associated continuous data used for homotopy invariance of singular homology.
The surrounding imports are Mathlib singular homology, module-category colimits, and topological homotopy equivalences, so the local setting is ordinary singular chain calculus rather than an RS-specific cost identity.
proof idea
One-line definitional wrapper. The chain group is the coproduct $\coprod_{\sigma}\mathbb{Z}$ in ModuleCat ℤ. The generator attached to simplex $a$ is exactly the coproduct inclusion of the $a$-th summand: Sigma.ι (fun _ => ModuleCat.of ℤ ℤ) a. No further lemmas are applied; the abbrev is that inclusion morphism.
why it matters
This generator is the atomic building block of the singular chain complex used throughout Foundation.SingularPrism. Face maps, prism operators, and the singular $(n+1)$-simplex associated to a homotopy $H:I\times X\to Y$ are all assembled by pushing these generators forward along continuous maps of simplices.
In the broader Recognition Science stack the prism calculus supports homotopy-invariant chain-level arguments that sit under the foundation layer (forcing chain T0–T8 lives elsewhere; this file is ordinary singular homology infrastructure). Downstream name collisions with other gen symbols (cosmology adjacency generators, Hamiltonian generators, SM generation counts) are unrelated; the real consumers are the prism/face constructions and any chain-map or homotopy-operator lemmas built on Cgrp.
No open RS conjecture is discharged here: the declaration is pure linear-algebraic scaffolding for singular chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.