gen_augFun
plain-language theorem explainer
Composing the generator inclusion of a singular 0-simplex s with the partial augmentation against A yields id on ℤ if the point of s lies in A, and 0 otherwise. Anyone computing H₀ via augmentation, or pairing point classes against clopen sets, cites this. The proof is the coproduct universal property (one-line Sigma.ι_desc).
Claim. Let $X$ be a topological space and $A \subseteq X$. For any singular $0$-simplex $s$ of $X$, the composite of the generator inclusion of $s$ into the degree-$0$ singular chain group with the partial augmentation against $A$ equals $\mathrm{id}_{\mathbb{Z}}$ if the underlying point of $s$ lies in $A$, and equals $0$ otherwise.
background
In the singular-chain setup of this module, the index type Idx X n is the set of singular $n$-simplices of $X$ (maps $\Delta^n \to X$). The degree-$n$ chain group is the coproduct $\coprod_{\sigma} \mathbb{Z}$ over those simplices. The generator map attached to a simplex $a$ is the canonical coproduct inclusion of the $\mathbb{Z}$ summand labelled by $a$.
The partial augmentation against a set $A$ is the chain map out of degree $0$ that sends the generator of a $0$-simplex to $1 \in \mathbb{Z}$ when the simplex's point lies in $A$, and to $0$ otherwise. A $0$-simplex is determined by its image point (pointOf).
The local setting is the singular-homology apparatus used to identify $H_0$ of path-connected spaces with $\mathbb{Z}$ via augmentation, and to pair point classes against clopen subsets.
proof idea
One-line term proof. The partial augmentation is defined as a coproduct descent (Sigma.desc) whose component on each $0$-simplex is the indicated if-then-else. The generator is the corresponding coproduct inclusion (Sigma.ι). Their composite is therefore exactly that component, by the defining equation Sigma.ι_desc.
why it matters
This is the evaluation rule that makes partial augmentation computable on generators. Downstream it feeds augFun_genUnit (same statement on unit chains), bnd_augFun (partial augmentation against a clopen set kills boundaries), ptFrom_augTo (pairing a point class against a clopen augmentation), and sChainMap_augTo (naturality of full augmentation under continuous maps).
Those lemmas assemble into isIso_homologyMap_augTo: for path-connected $X$, the augmentation induces $H_0(X) \cong \mathbb{Z}$. In the Recognition foundation stack this is the singular-homology side of connectedness and component counting, used when the geometric models (spheres, prisms, Mayer–Vietoris) need a clean $H_0$ identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.