circleH1Z
plain-language theorem explainer
Pins the Mathlib object for first singular homology of the circle with integer coefficients: H₁(S¹; ℤ) as an object of ModuleCat ℤ. Anyone wiring the T8/S¹ cohomology handoff or the Mathlib backend contract cites this name instead of inlining the functor application. The body is a pure abbreviation of Mathlib's singularHomologyFunctor at degree 1 on TopCat.sphere 1.
Claim. Let $\mathrm{circleH1Z}$ denote the object of $\mathbf{Mod}_{\mathbb{Z}}$ given by the degree-$1$ singular homology of the topological $1$-sphere with coefficients in $\mathbb{Z}$, i.e. $H_1(S^1;\mathbb{Z})$ as produced by Mathlib's singular homology functor.
background
The Mathlib Cohomology Bridge module records the exact backend objects needed to replace the project's concrete $S^1$ cohomology encoding. Mathlib already exposes the singular homology functor API, but the T8 replacement path still needs a pinned computation of $H_1(S^1;\mathbb{Z})$ (and later an Alexander-duality bridge from circle-complement homology to reduced cohomology). This module deliberately refuses to fake that backend by recycling a project-local nontriviality lemma.
Here the target is named once: apply Mathlib's singularHomologyFunctor in the category of $\mathbb{Z}$-modules, at homological degree $1$, to the topological $1$-sphere TopCat.sphere 1, with coefficient object $\mathbb{Z}$. Downstream certificates then talk about nonvanishing ($\neg\mathrm{IsZero}$) and the strong isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ relative to this single imported object.
proof idea
Definitional abbreviation, not a proof. The right-hand side is the double application of Mathlib's singular homology functor: first fix coefficients $\mathrm{ModuleCat},\mathbb{Z}$ and degree $1$, then evaluate on TopCat.sphere 1. Marked noncomputable because the singular homology construction is. Equality to the expanded Mathlib term is definitional (rfl in the sibling identity theorem).
why it matters
This is the single pinned import target for the circle-$H_1$ handoff. Downstream, circleH1ZNonzero asks Mathlib for nonvanishing, circleH1ZIsoInt asks for $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, and the structures CircleH1MathlibComputation, CircleH1TargetCertificate, and MathlibBackendHandoffCertificate all require that the target equal this object rather than a project-local stand-in. The sibling theorem circleH1Z_is_mathlib_singular_homology records that equality by rfl.
In the broader Recognition chain, T8 forces $D=3$ spatial dimensions; the circle appears as the residual $S^1$ whose homology must be nontrivial for winding and octave bookkeeping. The project already has an unconditional nonvanishing proof for a concrete chain complex (homologyOne_nonzero in CircleWindingChain). This abbrev is the bridge name that lets that concrete story be retired once Mathlib supplies the isomorphic computation, without silently swapping in a homemade replacement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.