augTo_f_zero
plain-language theorem explainer
The degree-0 component of the clopen augmentation chain map equals the partial augmentation on 0-chains: a simplex contributes 1 if its point lies in A and 0 otherwise. Singular-homology arguments that pair points or push chains against clopen sets cite this identification. The proof unfolds the mkHomToSingle construction and cancels the identity isomorphism.
Claim. Let $X$ be a topological space and $A \subseteq X$ a clopen subset. Write $\mathrm{aug}_A$ for the chain map from the singular chain complex of $X$ to $\mathbb{Z}$ concentrated in degree $0$ that augments against $A$. Then the degree-$0$ component of $\mathrm{aug}_A$ equals the partial augmentation homomorphism that sends a $0$-simplex to $1$ if its image point lies in $A$ and to $0$ otherwise.
background
The module builds singular-chain tools for Recognition Science continuum bridges: free abelian groups on singular simplices, boundaries, and chain maps into $\mathbb{Z}$ placed in a single degree. The partial augmentation $\mathrm{augFun}(X,A)$ is the degree-$0$ map that, on each generator simplex $s$, returns the identity on $\mathbb{Z}$ when the underlying point of $s$ lies in $A$ and zero otherwise.
When $A$ is clopen, that map extends to a genuine chain map $\mathrm{augTo}(X,A)$ into the complex with $\mathbb{Z}$ only in degree $0$, because the boundary of every $1$-simplex has total signed weight zero on $A$ (the boundary-vanishing lemma used inside the definition of $\mathrm{augTo}$). Homological-complex infrastructure packages such a map via $\mathrm{mkHomToSingle}$, so the degree-$0$ face is the original map composed with the canonical identification of the single complex's degree-$0$ object with $\mathbb{Z}$.
proof idea
Term-mode rewrite of the definition of $\mathrm{augTo}$: expand $\mathrm{mkHomToSingle}$, reduce the single-complex degree-$0$ object via $\mathrm{single}_0\mathrm{ObjXSelf}$, and cancel the inverse of the reflexivity isomorphism. What remains is composition on the right by the identity morphism, which is the identity by the standard $\mathrm{comp_id}$ law. No case analysis on $A$ or $X$ is required.
why it matters
This is the bookkeeping step that lets later lemmas treat the chain map and the concrete $0$-chain functional interchangeably. Downstream, $\mathrm{ptFrom_augTo}$ pairs the class of a point against a clopen augmentation and obtains $1$ or $0$ according to membership; $\mathrm{augTo_f_zero_apply}$ is the elementwise form used under concrete-category coercions; $\mathrm{sChainMap_augTo}$ shows naturality of universal augmentation under continuous maps; and path-connected homology reductions compare chains to total augmentation times a base point.
In the Foundation layer these identities support singular-sphere and Mayer–Vietoris arguments that connect discrete ledger structure to continuum topology, feeding the continuum-bridge side of the forcing chain rather than a named T0–T8 step directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.