augFun_genUnit
plain-language theorem explainer
On a generator 0-chain attached to a singular 0-simplex s, the set-relative augmentation returns 1 if the underlying point of s lies in A and 0 otherwise. Anyone reducing 0-homology or writing Mayer–Vietoris style arguments on singular chains will cite this evaluation rule. The proof unfolds the generator, rewrites through the composite that defines the augmentation, and splits on membership of the point in A.
Claim. Let $X$ be a topological space, $A \subseteq X$, and $s$ a singular $0$-simplex of $X$. Writing $c_s$ for the generator $0$-chain attached to $s$ and $\varepsilon_A$ for the set-relative augmentation on $0$-chains, one has $\varepsilon_A(c_s) = 1$ if the point of $s$ lies in $A$, and $\varepsilon_A(c_s) = 0$ otherwise.
background
The ambient module is singular chain homology with integer coefficients on a topological space $X$ (as a TopCat object). The index type Idx X n is the set of singular $n$-simplices of $X$; the degree-$n$ chain group is the free $\mathbb{Z}$-module on that index set.
The generator attached to a simplex $s$ is the basis element of coefficient $1$ at $s$ (written genUnit). For $n=0$, a singular $0$-simplex is just a point of $X$, recovered by pointOf. The set-relative augmentation augFun X A is the $\mathbb{Z}$-linear functional on $0$-chains that sums the coefficients of those generators whose underlying points lie in $A \subseteq X$.
Upstream, genUnit_eq identifies the unit generator with the general scaled generator at coefficient $1$, and gen_augFun records how the augmentation acts after composition with the generator map. The zero-morphism evaluation lemma zeroApp handles the complementary case.
proof idea
Term-mode rewrite followed by a two-branch case split. First replace the unit generator by the scaled generator at $1$ via genUnit_eq, then push the evaluation through the module-category composition using ModuleCat.comp_apply and the composite identity gen_augFun. Case on whether pointOf s lies in $A$: if yes, both if branches fire positively and the identity morphism applies; if no, both fire negatively and zeroApp collapses the zero morphism to $0$.
why it matters
This is the generator-level evaluation rule for the $0$-augmentation used throughout the singular-sphere development. Its sole recorded consumer is exists_bnd_of_pathConnected: in a path-connected space every $0$-chain is homologous to its total augmentation times a fixed base-point generator. That lemma is the standard H_0 identification needed before any sphere or Mayer–Vietoris computation can reduce degree-zero classes to integers.
In the Recognition Science foundation stack this sits under the singular-homology toolkit (prism operators, pair exact sequences, Mayer–Vietoris) that supports geometric forcing arguments. It does not itself touch the T0–T8 chain, the J-cost, or the eight-tick octave; it is pure algebraic topology scaffolding those later geometric claims rely on when they quote H_0 or connectedness of simplices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.