Zsingle
plain-language theorem explainer
The integers, viewed as a chain complex supported only in degree 0. Algebraic topologists cite it as the codomain of augmentation maps and the domain of point-class maps in singular homology. The body is a one-line Mathlib constructor: single₀ applied to ℤ as a ℤ-module.
Claim. Let $Z_{\bullet}$ be the chain complex of $\mathbb{Z}$-modules with $Z_0 \cong \mathbb{Z}$ and $Z_n = 0$ for all $n \neq 0$. Equivalently, $Z_{\bullet}$ is the image of $\mathbb{Z}$ under the degree-$0$ single-complex functor on chain complexes indexed by $\mathbb{N}$.
background
SingularSphere develops singular homology for topological spaces in the Recognition Foundation layer, using Mathlib's ChainComplex and ModuleCat over $\mathbb{Z}$. The singular chain complex $SC(X)$ of a space $X$ is free on singular simplices; its degree-$0$ homology is controlled by path-components via an augmentation to $\mathbb{Z}$.
A single complex (Mathlib ChainComplex.single₀) places an object in degree $0$ and zeros elsewhere, with vanishing differentials. Here the object is $\mathbb{Z}$ as a module over itself. Sibling abbreviations in the module (Hgrp, constSimplex, augFun, pointOf) build the free singular chains and the augmentation functional against clopen sets.
This object is the standard target for total-mass maps and the standard source for constant $0$-simplices at a base point.
proof idea
One-line definitional wrapper. Apply Mathlib's ChainComplex.single₀ at the category ModuleCat ℤ, then take the object functor on ModuleCat.of ℤ ℤ. No further lemmas or tactics; noncomputable only because the ambient category infrastructure is.
why it matters
This is the unit object for degree-$0$ singular homology arguments in the module. Downstream, augTo builds the augmentation chain map $SC(X) \to Z_{\bullet}$ against a clopen set; ptFrom sends $1 \in \mathbb{Z}$ to the constant $0$-simplex at a point; ptFrom_augTo evaluates the pairing (identity or zero according to membership). ZsingleH0Iso identifies $H_0(Z_{\bullet}) \cong \mathbb{Z}$, and Zsingle_d_one_zero records that the outgoing differential from degree $1$ vanishes.
Together these feed exists_bnd_of_pathConnected: in a path-connected space every $0$-chain is homologous to its total augmentation times a base point. That is the classical $H_0 \cong \mathbb{Z}$ step used when the Foundation layer compares singular spheres, prisms, and Mayer–Vietoris gluings. It is pure homological scaffolding, not a physics forcing step (T0–T8), but it underwrites later topological invariants the monolith attaches to recognition geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.