Pith. sign in
module module high

IndisputableMonolith.Foundation.CircleH1Computation

show as:
view Lean formalization →

Algebraic model of the reduced cellular chain complex of the circle, concentrated in degree 1 with integer coefficients. Supplies the finite chain complex whose H_1 is Z, together with transport lemmas along isomorphisms and quasi-isomorphisms to that single-degree complex. Cited by anyone computing circle homology before singular transport to TopCat.sphere 1. Structure is definitional plus a ladder of iso/quasi-iso transfer lemmas.

claimThe reduced cellular chain complex of $S^1$ is modelled by the integer chain complex supported only in degree $1$: $C_1 \cong \mathbb{Z}$ and $C_n = 0$ for $n \neq 1$. Consequently $H_1(C_\bullet) \cong \mathbb{Z}$. Any chain complex isomorphic (or quasi-isomorphic at degree 1) to this single-degree complex inherits $H_1 \cong \mathbb{Z}$.

background

Recognition Science needs an explicit computation of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as the algebraic backbone of the winding invariant and the T8 dimensional forcing. Mathlib supplies singular homology functors, but the finite circle model is built by hand first.

Upstream, CircleParam fixes the carrier and basepoint of TopCat.sphere 1 and the constant singular 1-simplex identities. CircleFundamentalSimplex constructs the once-around generator whose two faces meet at that basepoint. MathlibCohomologyBridge records the backend contract for reduced cohomology of $S^1$ and the Alexander-duality link from circle-complement homology.

This module sits between those primitives and the singular transport: it defines the purely algebraic reduced cellular model (one free generator in degree 1, zeros elsewhere) and the comparison lemmas that move $H_1\cong\mathbb{Z}$ along isomorphisms and quasi-isomorphisms.

proof idea

Definitional core: introduce the single-degree integer complex (nonzero only in degree 1) and the reduced cellular circle chain model, then prove the degree-1 term is $\mathbb{Z}$ and the degree-0 term vanishes.

Transfer ladder: a sequence of lemmas pushes the identification $H_1\cong\mathbb{Z}$ first along an isomorphism to the single-degree complex, then along a quasi-isomorphism at degree 1, and finally along a full quasi-isomorphism of complexes. Parallel nonempty-iso variants handle the non-empty homology package used downstream. No deep spectral-sequence work; everything is short-complex and single-homology API from Mathlib.

why it matters in Recognition Science

Feeds CircleWindingChain, which lifts path-level winding to singular 1-simplices of TopCat.sphere 1 and proves the kills-boundaries identity that makes displacement a homology invariant. Without a clean algebraic $H_1\cong\mathbb{Z}$ model, that invariant has nowhere to land.

In the broader foundation stack this is the algebraic core of the finite circle model before topological transport. It supports the Mathlib-backed reduced-cohomology computation demanded by the T8 replacement path (D=3 spatial dimensions via circle/sphere duality). The module closes the gap between hand-built cellular data and the singular simplicial set of the actual sphere object.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (54)