singleDegreeOneIntComplex
plain-language theorem explainer
Defines the chain complex of ℤ-modules that is ℤ in degree 1 and zero elsewhere (downward ℕ-grading). It is the algebraic skeleton of the finite circle model used to compute H₁(S¹; ℤ) ≅ ℤ. Anyone transporting a cellular or singular model of the circle cites this object as the reduced target. The body is a one-line Mathlib single-complex constructor applied to ModuleCat.of ℤ ℤ.
Claim. Let $C_\bullet$ be the homological complex of $\mathbb{Z}$-modules, graded by $\mathbb{N}$ with differentials lowering degree, that is concentrated in degree $1$ with $C_1 \cong \mathbb{Z}$ and $C_n = 0$ for $n \neq 1$. This is the single-supported integer complex in degree $1$.
background
The module CircleH1Computation is a local Mathlib-style workbench aimed at the classical isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Per the module doc, it does not yet replace TopCat.sphere 1 and does not feed the strict T8 dimensional bridge until a genuine equivalence to Mathlib singular homology is proved.
The first algebraic atom is a chain complex of objects in ModuleCat ℤ with shape ComplexShape.down ℕ (differentials lower degree). Mathlib's HomologicalComplex.single builds the complex that is a given module in one degree and zero elsewhere. Instantiating that constructor at degree 1 with the free rank-one module ModuleCat.of ℤ ℤ yields the reduced model whose degree-1 homology is visibly ℤ.
This object is the algebraic core of the finite circle chain model before any topological transport to the geometric circle is supplied.
proof idea
Definitional one-liner. Apply Mathlib's HomologicalComplex.single functor for the category ModuleCat ℤ and shape ComplexShape.down ℕ at degree 1, then evaluate on the object ModuleCat.of ℤ ℤ. No lemmas or tactics; the abbrev is pure constructor application.
why it matters
This is the reduced target against which every finite circle chain model is compared. Downstream transport lemmas (homologyOneIsoIntOfIsoSingleDegreeOneIntComplex, the degree-local and global quasi-iso variants, and their Nonempty proposition-facing forms) all state: if a complex $K$ is isomorphic or quasi-isomorphic to this single-supported complex, then $H_1(K)\cong\mathbb{Z}$. The reduced cellular circle chain model is also built relative to it.
In the Recognition framework the computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is a missing Mathlib-facing atom on the path toward the eight-tick octave and the T8 forcing of $D=3$. The module doc is explicit that this workbench does not yet close that bridge: topological identification with singular homology of TopCat.sphere 1 remains open. The definition therefore anchors the algebraic half of that unfinished step without claiming the geometric half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.