bnd_augFun
plain-language theorem explainer
Partial augmentation against a clopen subset annihilates degree-0 singular boundaries: composing the boundary map with that augmentation yields zero. Anyone assembling a chain map from singular chains of X into ℤ concentrated in degree 0 cites this. The argument expands the boundary via the two face maps, then cancels endpoint contributions using clopen membership agreement on 1-simplex faces.
Claim. Let $X$ be a topological space and $A \subseteq X$ clopen. Write $\partial_0$ for the degree-$0$ singular boundary and $\varepsilon_A$ for the partial augmentation that sends a $0$-simplex to $1$ if its image point lies in $A$ and to $0$ otherwise. Then $\varepsilon_A \circ \partial_0 = 0$.
background
The module works in the singular chain complex of a space $X$ (as a TopCat object), with free $\mathbb{Z}$-modules on singular simplices and the usual alternating face boundary. Degree $0$ chains are formal sums of points of $X$; the boundary $\partial_0$ lands there from degree $1$.
Partial augmentation against a set $A$ evaluates a $0$-chain by counting (with coefficients) only those generators whose underlying point lies in $A$. The full classical augmentation is the special case $A = X$. Here $A$ is required to be clopen so that continuous images of connected simplices cannot split membership between $A$ and its complement.
Upstream, the boundary on generators is the signed sum of face maps (gen_d), and the generator-level evaluation of the partial augmentation is the pointwise indicator of $A$ (gen_augFun). A companion fact records that the two $0$-faces of any $1$-simplex agree on membership in a clopen set.
proof idea
Extensionality on the coproduct of free modules reduces to a single $1$-simplex $\sigma$. Rewrite $\partial_0(\sigma)$ via the face formula as $\delta_0\sigma - \delta_1\sigma$ (the two terms of Fin 2 with signs $(+1),(-1)$). Push the partial augmentation through the sum and scalar multiplications, then apply the generator-level evaluation twice.
Case on whether the image point of $\delta_0\sigma$ lies in $A$. Clopenness gives the two faces the same membership status. If both are in, the contributions are $+1$ and $-1$, which cancel. If both are out, both contributions are zero. Either way the composite vanishes on $\sigma$.
why it matters
This is the exact chain-map identity needed to promote the degree-$0$ partial augmentation into a morphism of homological complexes. Downstream, augTo packages it as a map from the singular complex of $X$ into $\mathbb{Z}$ concentrated in degree $0$, with this lemma discharging the sole nontrivial degree check (that the map kills boundaries into degree $1$).
In the SingularSphere development the construction supplies a homological probe of clopen decompositions: the induced map on $H_0$ counts components meeting $A$. That is the algebraic input for comparing singular homology of spheres and related spaces against discrete recognition data in the Foundation layer, without yet invoking the forcing chain (T5–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.