Pith. sign in
module module moderate

IndisputableMonolith.Foundation.SingularSphere

show as:
view Lean formalization →

Defines integer singular homology groups and the supporting simplex, augmentation, and point-space apparatus used to compute the homology of spheres. Algebraic topologists and anyone tracing the RS foundation chain cite it for the classical identification of reduced homology of S^n. The module assembles prism, pair, subdivision, and Mayer–Vietoris infrastructure rather than a single theorem.

claimFor a topological space $X$ and degree $n\in\mathbb{Z}$, the module introduces the singular homology group $H_n(X;\mathbb{Z})$, constant simplices on a basepoint, the augmentation map on $0$-chains, and the comparison between a point and the constant $0$-simplex, as the algebraic substrate for sphere computations.

background

Singular homology with integer coefficients assigns to each space $X$ graded abelian groups $H_n(X;\mathbb{Z})$ built from free chains on continuous maps $\Delta^n\to X$, modulo boundaries. The module works in that classical setting, not in a specialized RS cost or ladder calculus.

Upstream imports supply the standard computational toolkit: prism operators (homotopies of chains), relative pairs, barycentric subdivision (for excision), and Mayer–Vietoris sequences. Mathlib contributes single-complex homology, path and convex contractibility, and the smooth sphere manifold instance.

Local definitions include the homology group abbreviation, the generator of the homology of a point, constant simplices, the point-extraction map on $0$-simplices, and the augmentation homomorphism that sends a $0$-chain to the sum of its coefficients. These are the usual bridges between geometric points and algebraic $0$-cycles.

proof idea

This is primarily a definition and infrastructure module. It wires Mathlib singular-chain and sphere instances to the in-house prism, pair, subdivision, and Mayer–Vietoris layers, then records elementary identities (point of a constant simplex, naturality of point-extraction under maps, generation properties of the augmentation). No single global theorem is proved here; sphere homology calculations are deferred to consumers that apply Mayer–Vietoris to hemispherical covers.

why it matters in Recognition Science

Sphere homology is the topological checkpoint that later geometric modules need before they can speak about fundamental classes, degrees, or dimension-sensitive statements in the foundation layer. The sole recorded consumer is SingularSphereGeometry, which imports this module to attach geometric content to the algebraic groups defined here.

In the broader Recognition Science forcing chain the classical facts $H_n(S^n)\cong\mathbb{Z}$ and vanishing in other degrees underwrite dimension and orientation arguments (including the T8 claim that space is three-dimensional). This file does not itself state those isomorphisms; it supplies the groups and the chain-level language in which they will be proved.

scope and limits

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (55)