ptH_augH
plain-language theorem explainer
The degree-0 homology class of a point pairs against a clopen augmentation to the identity on ℤ when the point lies in the set, and to zero otherwise. Sphere-geometry arguments cite it to certify nonvanishing of point-difference classes. The proof unfolds the two maps, reduces via the chain-level pairing lemma, and case-splits on membership.
Claim. Let $X$ be a topological space, $x\in X$, and $A\subseteq X$ clopen. The composition of the degree-$0$ homology class of $x$ with the degree-$0$ homology augmentation against $A$ equals $\mathrm{id}_{\mathbb{Z}}$ if $x\in A$, and equals the zero morphism otherwise.
background
The module Foundation.SingularSphere builds singular homology of spaces in TopCat over $\mathbb{Z}$, with $H_0$ realized as homology of the singular chain complex. Two maps on $H_0$ are central here.
The point class ptH is induced by the chain map ptFrom that sends $1\in\mathbb{Z}$ (concentrated in degree 0) to the constant 0-simplex at $x$. The augmentation augH is induced by a chain map that evaluates degree-0 chains against a fixed clopen set $A$: it records the total coefficient of simplices whose image lands in $A$. Clopenness of $A$ makes that evaluation a well-defined chain map, so it descends to homology.
Upstream, ptFrom_augTo already computes the composition at the chain-map level: the constant simplex at $x$ augments to $1$ or $0$ according as $x\in A$. The present lemma is the homology-level packaging of that fact, postcomposed with the identification of $H_0(\mathbb{Z}[0])$ with $\mathbb{Z}$.
proof idea
Term-mode proof by unfolding ptH and augH, then reassociating so the middle composite is homologyMap of ptFrom ≫ augTo. That composite is rewritten by ptFrom_augTo, which is already an if-then-else on membership. Case split on $x\in A$: the true branch becomes homologyMap id, which is the identity, and Iso.inv_hom_id cancels the $H_0$ identification; the false branch becomes homologyMap 0, hence zero after composition. Algebraic identities used are id_comp, homologyMap_id, homologyMap_zero, zero_comp, and comp_zero.
why it matters
This is the basic evaluation pairing that turns geometric membership of points in clopen charts into morphisms of $\mathbb{Z}$-modules. Downstream, diffClass_pairing in SingularSphereGeometry applies it twice to the east-arc clopen on the circle: the two endpoints of a point-difference class land one in and one out of the arc, so the pairing collapses to $\mathrm{id}-0=\mathrm{id}$. That nonvanishing statement is the algebraic certificate that the difference class is a nontrivial $H_0$ cycle, which underpins the singular-sphere geometry used later in the foundation stack.
In the broader Recognition framework this sits in the topological scaffolding that supports discrete octave and sphere constructions (eight-tick period, $D=3$), not in the J-cost forcing chain itself. It is pure singular-homology bookkeeping, proved with no sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.