Zsingle_d_one_zero
plain-language theorem explainer
In the chain complex with ℤ concentrated in degree 0, the differential from degree 1 to degree 0 is the zero map. Singular-homology arguments that compare an augmented complex to this single complex cite the fact routinely. The proof is a short term application of the Mathlib vanishing lemma for off-support degrees of a single complex, using 1 ≠ 0.
Claim. Let $Z_\bullet$ be the chain complex of $\mathbb{Z}$-modules that is $\mathbb{Z}$ in degree $0$ and $0$ elsewhere. Then the differential $d_1\colon (Z_\bullet)_1\to (Z_\bullet)_0$ equals the zero morphism.
background
The ambient module builds singular chain complexes and their homology for topological spaces, with an eye toward spheres and path-connected spaces. The abbreviation in play is the single complex: $\mathbb{Z}$ placed as a chain complex concentrated in degree $0$ (via Mathlib's ChainComplex.single₀), written here as the complex $Z_\bullet$.
Differentials of a single complex vanish off the support degree. Concretely, the object in degree $1$ is the zero module of $\mathbf{Mod}_{\mathbb{Z}}$, so any outgoing differential from that degree is forced to be zero. The complex shape is the standard downward shape on $\mathbb{N}$.
Upstream, the only arithmetic input needed is $1\neq 0$ in $\mathbb{N}$, which discharges the off-support hypothesis of Mathlib's vanishing lemma for single-complex objects.
proof idea
Term-mode one-liner. Apply Mathlib's HomologicalComplex.isZero_single_obj_X to the downward complex shape on $\mathbb{N}$, support degree $0$, coefficient object $\mathbb{Z}$, and query degree $1$, with witness $1\neq 0$. That yields that the degree-$1$ object is zero as a module. Then IsZero.eq_of_src concludes that any morphism out of that object (in particular $d_1$) equals zero.
why it matters
The lemma clears a routine differential identity needed when comparing the augmented singular complex of a space to the single complex $Z_\bullet$. Its sole recorded consumer is isIso_homologyMap_augTo: for a path-connected space $X$, the augmentation induces an isomorphism $H_0(X)\cong\mathbb{Z}$ on homology.
That $H_0$ computation is foundational scaffolding inside Foundation.SingularSphere, which develops singular homology of spheres and related spaces used by the Recognition forcing chain (spatial dimension and connectivity facts feeding T8-style dimension arguments). It does not itself force $\phi$, the eight-tick octave, or any physical constant; it is pure homological algebra supporting those later geometric claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.