augTo_f_zero_apply
plain-language theorem explainer
Elementwise, the degree-0 component of the clopen augmentation chain map equals the partial augmentation on singular 0-chains. Algebraic topologists cite it when moving between HomologicalComplex morphisms and concrete ℤ-linear maps on chains. The proof is a one-line congrArg from the already-proved morphism equality at degree 0.
Claim. Let $X$ be a topological space, $A \subseteq X$ clopen, and $c$ a singular $0$-chain on $X$ with $\mathbb{Z}$ coefficients. Then the underlying map of the degree-$0$ component of the augmentation chain map $SC(X) \to \mathbb{Z}[0]$ sends $c$ to the same integer as the partial augmentation of $c$ against $A$.
background
In this module, singular chains $C_n(X;\mathbb{Z})$ are realized as the coproduct $\coprod_{\sigma} \mathbb{Z}$ over singular $n$-simplices (written Cgrp). The object $\mathbb{Z}[0]$ is the chain complex with $\mathbb{Z}$ concentrated in degree $0$.
The partial augmentation against a set $A$ is the $\mathbb{Z}$-linear map on $0$-chains that sends each generator $\sigma$ to $1$ if its image point lies in $A$ and to $0$ otherwise. When $A$ is clopen, this map extends to a chain map $SC(X) \to \mathbb{Z}[0]$ because the boundary of every $1$-simplex has augmentation zero (the two endpoints either both lie in $A$ or both lie outside).
The sibling lemma already identifies the degree-$0$ component of that chain map with the partial augmentation as morphisms in ModuleCat. The present statement only unwraps the concrete-category coercion so the equality can be applied to an individual chain.
proof idea
One-line term proof. Apply congrArg to the function that evaluates a module morphism at the fixed $0$-chain $c$, using the already-established morphism equality that the degree-$0$ face of the augmentation chain map equals the partial augmentation map. No new algebraic content; pure transport across the ConcreteCategory.hom coercion.
why it matters
Feeds the theorem that the augmentation induces an isomorphism $H_0(X) \cong \mathbb{Z}$ for path-connected $X$. That result applies the elementwise form when checking that the homology map is bijective on classes of $0$-cycles: one must evaluate the chain-map component on concrete chains, not merely equate morphisms.
In the Recognition foundation stack this sits inside the singular-homology toolkit (prisms, pairs, Mayer–Vietoris, sphere computations) used to control low-degree topology of configuration and recognition spaces. It does not itself touch the forcing chain T0–T8, but it is infrastructure for any later argument that needs $H_0 \cong \mathbb{Z}$ as an integer invariant of connected components.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.