augFun
plain-language theorem explainer
Partial augmentation on singular 0-chains: each 0-simplex contributes coefficient 1 if its underlying point lies in a fixed set A, else 0. Algebraic topologists cite it when building the augmentation chain map to ℤ and when proving that clopen partial augmentations kill boundaries. Defined by coproduct descent with a pointwise indicator on generators.
Claim. For a topological space $X$ and a subset $A \subseteq X$, the partial augmentation is the $\mathbb{Z}$-linear map $\varepsilon_A \colon C_0(X;\mathbb{Z}) \to \mathbb{Z}$ sending each singular $0$-simplex $\sigma$ to $1$ if the underlying point of $\sigma$ lies in $A$, and to $0$ otherwise.
background
In this module the degree-$n$ singular chain group $C_n(X;\mathbb{Z})$ is the coproduct of one copy of $\mathbb{Z}$ over each singular $n$-simplex of $X$. A singular $0$-simplex is determined by its image point; pointOf extracts that point via evaluation at the unique vertex of the standard $0$-simplex.
Classical singular homology uses the full augmentation $\varepsilon \colon C_0(X) \to \mathbb{Z}$ that sums all coefficients. Here one needs a partial version relative to an arbitrary subset $A$: only generators whose points land in $A$ contribute. That map is the building block for the chain-map augmentation into the complex concentrated in degree $0$, and for the path-connectedness argument that every $0$-cycle is homologous to a multiple of a basepoint.
The surrounding development sits in the singular-sphere / Mayer–Vietoris layer of the foundation stack (prisms, pairs, subdivisions), where clopen decompositions and connectivity feed homology computations used later in the Recognition forcing chain.
proof idea
Definition by universal property of the coproduct: on the summand indexed by a $0$-simplex $s$, send the generator to the identity endomorphism of $\mathbb{Z}$ if pointOf s lies in $A$, and to the zero map otherwise. Classical choice is opened only to decide membership. No further lemmas are invoked at the definition site; downstream lemmas such as the generator evaluation and the boundary-vanishing statement unpack this case split.
why it matters
This is the degree-$0$ component of the partial augmentation chain map. Downstream, augTo packages it (when $A$ is clopen) as a morphism of complexes into $\mathbb{Z}$ concentrated in degree $0$; bnd_augFun proves it annihilates boundaries, so the map descends to homology; augFun_genUnit and augTo_f_zero give the elementwise and componentwise forms used in computations.
It also appears in exists_bnd_of_pathConnected: in a path-connected space every $0$-chain is homologous to its total augmentation times a fixed basepoint, which is the standard generator of $H_0$. That connectivity fact is the algebraic-topology input behind sphere and pair calculations in the singular foundation layer. Within Recognition Science those calculations support the geometric side of the forcing chain (eight-tick octave, $D=3$) rather than the $J$-cost or mass-ladder arithmetic directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.