augH
plain-language theorem explainer
Degree-0 singular homology augmentation: a map H_0(X;ℤ) → ℤ induced by counting 0-chains against a fixed clopen subset A ⊂ X. Algebraic topologists cite it to identify H_0 of path-connected spaces with ℤ and to split Mayer–Vietoris in degree 0. Defined by pushing the chain-level clopen augmentation to homology and composing with the standard H_0(ℤ[0]) ≅ ℤ.
Claim. For a topological space $X$ and a clopen set $A \subseteq X$, there is a morphism of $\mathbb{Z}$-modules $\varepsilon_{X,A} : H_0(X;\mathbb{Z}) \to \mathbb{Z}$ obtained by applying $H_0$ to the chain-level augmentation against $A$ and identifying $H_0(\mathbb{Z}[0])$ with $\mathbb{Z}$.
background
In this module, singular homology $H_n(X;\mathbb{Z})$ is the homology of the singular chain complex $SC(X)$ with integer coefficients. Degree 0 records path-components up to oriented counting of points.
The chain-level map augTo sends a 0-chain to the integer sum of coefficients of those singular 0-simplices whose image lands in a fixed clopen set $A$. Because $A$ is clopen, the boundary of a 1-chain has total $A$-mass zero, so the map descends to a chain map into the complex $\mathbb{Z}$ concentrated in degree 0. The canonical isomorphism $H_0(\mathbb{Z}[0]) \cong \mathbb{Z}$ then converts that chain map into a homology morphism $H_0(X) \to \mathbb{Z}$.
The local setting is the singular-homology toolkit used to compute $H_*(S^n)$ via Mayer–Vietoris and prism subdivisions, feeding later Recognition geometry on the circle and sphere.
proof idea
Pure definitional composition, not a proof. Form the homology map in degree 0 of the chain map that augments against the clopen set $A$, then post-compose with the forward arrow of the standard isomorphism identifying $H_0$ of the degree-0 single complex on $\mathbb{Z}$ with the module $\mathbb{Z}$ itself. No tactics; the body is one composite morphism.
why it matters
This is the working $H_0 \to \mathbb{Z}$ map used throughout the singular-sphere development. Downstream, path-connectedness makes the universal-set instance an isomorphism, yielding $H_0(X) \cong \mathbb{Z}$ (Stage A/B). The same map is natural in $X$, pairs point classes to the indicator of membership in $A$, and supplies the splitting that proves the Mayer–Vietoris pair map is mono in degree 0 when $U \cap V$ is path-connected.
In the geometry layer it witnesses that the point-difference class on the circle is nonzero by pairing to $1$ against an east-arc clopen, which is the algebraic step toward $H_1(S^1) \neq 0$. Within Recognition Science this sits in the foundation that underwrites the eight-tick octave and $D=3$ forcing chain: singular homology of spheres is the topological backbone those later uniqueness arguments rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.