augTo
plain-language theorem explainer
Augmentation of the singular chain complex of a space X against a clopen subset A, realized as a chain map into ℤ placed in degree 0. Algebraic topologists cite it to pass from chains to H₀ and to count connected components via clopen sets. The construction is the standard mkHomToSingle packaging of the degree-0 partial augmentation, using that clopenness kills boundaries.
Claim. For a topological space $X$ and a clopen set $A \subseteq X$, there is a chain map from the singular chain complex $S_*(X;\mathbb{Z})$ to the complex with $\mathbb{Z}$ concentrated in degree $0$, induced by the partial augmentation that sends a $0$-simplex to $1$ if its image point lies in $A$ and to $0$ otherwise.
background
The module works in singular homology with integer coefficients on TopCat. The singular chain complex $S_*(X;\mathbb{Z})$ is the standard functorial complex whose degree-$n$ term is free on continuous maps $\Delta^n \to X$. The target complex is $\mathbb{Z}$ concentrated in degree $0$ (single complex), so a chain map into it is determined by a degree-$0$ map that annihilates boundaries.
The degree-$0$ map is the partial augmentation against $A$: on a generator (a $0$-simplex, i.e. a point of $X$) it returns $1$ if the point lies in $A$ and $0$ otherwise. The key upstream fact is that when $A$ is clopen this map kills the image of the boundary $S_1 \to S_0$. Clopenness supplies the topological control needed so that the two faces of a $1$-simplex contribute equally whenever the path crosses the cut, hence the composite vanishes.
Local setting is the singular-sphere foundation layer: chain-level tools that later identify $H_0$ of path-connected spaces and support sphere and Mayer–Vietoris arguments used in the dimensional forcing chain.
proof idea
One-line packaging via HomologicalComplex.mkHomToSingle. Feed the partial augmentation in degree $0$, then discharge the single compatibility obligation: the composite of the degree-$1$ differential with the partial augmentation is zero. That obligation is exactly the upstream lemma that the partial augmentation against a clopen set kills boundaries; after reducing the degree index by omega, the proof is that lemma applied to the given clopen hypothesis.
why it matters
This is the chain-level bridge from singular chains to integer-valued $H_0$ data against clopen cuts. Downstream it feeds the degree-$0$ homology augmentation, the elementwise identification of the degree-$0$ component, the pairing of point classes against the augmentation, naturality under continuous maps, and the theorem that on a path-connected space the augmentation induces $H_0(X) \cong \mathbb{Z}$.
In the Recognition foundation stack, controlled $H_0$ and sphere homology sit under the geometric side of the forcing chain (eight-tick octave, $D=3$). A clean augmentation-to-$\mathbb{Z}$ map is the standard algebraic input for those connectivity and dimension arguments; without it the later isomorphisms on $H_0$ cannot even be stated as chain maps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.