SOb
plain-language theorem explainer
For a topological space X, SOb X is the simplicial object in ℤ-modules whose degree-n term is the free abelian group on singular n-simplices of X. Singular-homology and prism-operator arguments cite it as the free simplicial module feeding the alternating-face chain complex. The body is a pure composition: free-module functor whiskered onto the singular simplicial set of X.
Claim. For a topological space $X$, write $\mathrm{SOb}(X)$ for the simplicial object in $\mathbb{Z}$-modules obtained by applying the free $\mathbb{Z}$-module functor degreewise to the singular simplicial set of $X$. Equivalently, in each degree $n$ one has the free abelian group on continuous maps $\Delta^n\to X$.
background
Singular homology of a space $X$ is built in two steps: first form the singular simplicial set (continuous maps from standard simplices into $X$), then take free abelian groups degreewise and pass to the alternating-face chain complex. The present abbreviation packages that free-module step as a simplicial object in the category of $\mathbb{Z}$-modules.
The ambient module SingularPrism develops prism operators and face identities for singular chains, importing Mathlib's singular homology, module-category, and homotopy infrastructure. Sibling definitions supply the geometric prism map, face inclusions, and the continuous second-coordinate projection on the prism.
Downstream, the singular chain complex of $X$ is identified with the alternating-face complex of this simplicial module, so every boundary computation is phrased on $\mathrm{SOb}(X)$.
proof idea
Definitional one-liner. Start from the singular simplicial set of $X$, apply the constant free $\mathbb{Z}$-module functor via simplicial whiskering, and land in simplicial objects of $\mathrm{Module}_{\mathbb{Z}}$. No lemmas are invoked; the body is pure functor composition.
why it matters
This abbreviation is the typed carrier for singular chains inside the prism calculus. The equality SC_eq states that the singular chain complex of $X$ is definitionally the alternating-face complex of $\mathrm{SOb}(X)$. The generator-boundary lemma gen_d rewrites the differential on a basis simplex as the alternating sum of faces by unfolding that identification and applying the standard formula for the alternating-face differential.
In the Recognition Science foundation layer, singular chains and prism homotopies support topological identities used when relating discrete recognition structure to continuum topology. The declaration itself is pure algebraic topology scaffolding: it does not encode a forcing-chain step (T0–T8), the Recognition Composition Law, or a physical constant, but it supplies the chain-level language those continuum comparisons sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.