ptFrom_augTo
plain-language theorem explainer
Composing the degree-0 point chain map at x with the clopen augmentation of A yields the identity on ℤ[0] when x lies in A, and the zero map otherwise. Homology-level point/augmentation pairings cite this lemma. The proof reduces to the degree-0 component via from_single_hom_ext and splits on membership of x in A.
Claim. Let $X$ be a topological space, $x\in X$, and $A\subseteq X$ clopen. The composition of the chain map sending $1\in\mathbb{Z}[0]$ to the constant $0$-simplex at $x$ with the clopen augmentation of $A$ equals $\mathrm{id}_{\mathbb{Z}[0]}$ if $x\in A$, and the zero chain map otherwise.
background
The module works in singular chain complexes of topological spaces (as TopCat), with Zsingle the complex that is $\mathbb{Z}$ concentrated in degree $0$. The point map sends the generator of that complex to the constant $0$-simplex at a chosen basepoint $x$. The augmentation against a clopen set $A$ is the chain map to Zsingle induced by the degree-$0$ functional that sums coefficients of simplices whose image point lies in $A$ (and vanishes in positive degrees by the clopen boundary identity).
Clopenness of $A$ is required so the functional is a chain map: the boundary of a $1$-simplex contributes only when endpoints straddle $A$, which cannot happen for continuous paths into a clopen set. Upstream, augTo packages that functional as a morphism of complexes; the local lemmas augTo_f_zero, gen_augFun, and pointOf_constSimplex identify its degree-$0$ component on constant simplices with the characteristic value of membership in $A$.
proof idea
Apply HomologicalComplex.from_single_hom_ext to reduce equality of maps out of a single complex to equality of the degree-$0$ components. Rewrite the composite component via comp_f, ptFrom_f_zero, augTo_f_zero, gen_augFun, and pointOf_constSimplex, obtaining the characteristic if x ∈ A then 1 else 0 on the generator. Case-split on membership: if $x\in A$, both sides become the identity component; if not, both sides become zero. Each branch closes by rfl.
why it matters
This is the chain-level pairing of a point class against a clopen augmentation. The sole downstream consumer is ptH_augH, which lifts the same identity-or-zero statement to homology by naturality of homologyMap and this composite identity. In the SingularSphere development that statement is the computational engine for reading off $H_0$ against characteristic classes of clopen pieces, the algebraic input needed when the sphere and prism subdivisions feed Mayer–Vietoris and connectivity arguments in the foundation layer.
Within Recognition Science this sits in the topological scaffolding beneath the forcing chain rather than at a numbered T-step: it supplies the integer-valued test of whether a distinguished point lies in a recognized clopen region, the discrete precursor to later ladder and octave bookkeeping. No open scaffold remains; the lemma is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.