bnd
plain-language theorem explainer
Singular boundary ∂_{n+1}: C_{n+1}(X;ℤ)→C_n(X;ℤ) on the coproduct presentation of the chain groups. Cited wherever cycles, boundaries, or H₁-vanishing are written in this foundation layer (arc-complement acyclicity and its bisection lemmas). One-line abbreviation extracting the differential of the Mathlib singular chain complex at degrees (n+1,n).
Claim. For a topological space $X$ and $n\in\mathbb{N}$, the map $\partial_{n+1}^{X}:C_{n+1}(X;\mathbb{Z})\to C_n(X;\mathbb{Z})$ is the degree-$(n+1)$ differential of the singular chain complex of $X$. Here each $C_k(X;\mathbb{Z})$ is the free $\mathbb{Z}$-module on the singular $k$-simplices of $X$, presented as the coproduct $\coprod_{\sigma}\mathbb{Z}$ over those simplices.
background
This module equips spaces in TopCat with integer singular chains so later geometric arguments (arc complements in spheres, Mayer-Vietoris bisections) can name cycles and boundaries at a fixed Lean type.
The degree-$n$ chain group is the coproduct $\coprod_{\sigma\in\mathrm{Idx}(X,n)}\mathbb{Z}$ over the index of singular $n$-simplices. The singular chain complex is Mathlib's singularChainComplexFunctor evaluated at $X$, a chain complex of $\mathbb{Z}$-modules indexed by $\mathbb{N}$.
The boundary abbreviation names the differential of that complex between consecutive degrees, keeping domain and codomain in the coproduct presentation rather than an opaque internal type.
proof idea
One-line wrapper: the boundary out of degree $n+1$ is defined to be the differential component (SC X).d (n+1) n of the singular chain complex of $X$. No extra obligations; the chain-complex structure already supplies the module morphisms and $d^{2}=0$.
why it matters
Workhorse boundary arrow for the arc-complement acyclicity development (Hatcher 2B.1, arc case). Downstream, the bisection invariant records that a reference 1-cycle does not bound in the complement of an arc segment; the bisection step and nested bad-interval sequence ask whether pushforwards equal a boundary image under this map. Functoriality and half-arguments (bounds_map, bounds_of_halves) package existence of a preimage under the same arrow.
The parent theorem asserts every embedded arc in $S^{D}$ has $H_{1}$-acyclic complement in every dimension $D$. In the Recognition foundation layer this is the topological side of linking and vanishing used when dimension and connectivity constraints are formalized (including the forced $D=3$ spatial dimensions from forcing-chain step T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.