Hgrp
plain-language theorem explainer
Degree-n singular homology of a topological space X with integer coefficients, written as the homology of the singular chain complex. Algebraic topologists and anyone proving arc-complement acyclicity or linking-vanishing statements cite it as the standard H_n(X;ℤ) object. The body is a one-line abbreviation of the homology functor applied to the singular chain complex.
Claim. For a topological space $X$ and $n \in \mathbb{N}$, write $H_n(X;\mathbb{Z})$ for the degree-$n$ singular homology module of $X$ with coefficients in $\mathbb{Z}$, i.e. the homology in degree $n$ of the singular chain complex of $X$.
background
Singular homology is the standard algebraic invariant of a space obtained by taking free $\mathbb{Z}$-modules on continuous maps $\Delta^n \to X$, forming the singular chain complex, and passing to homology. In this module the singular chain complex is abbreviated SC X: the image of $X$ under the singular-chain-complex functor valued in chain complexes of $\mathbb{Z}$-modules.
The ambient development sits in Foundation.SingularSphere and its imports (singular prisms, pairs, subdivision, Mayer–Vietoris). The goal is classical sphere topology used later for linking and arc-complement statements: complements of arcs in $S^D$ should be $H_1$-acyclic (Hatcher 2B.1 style).
Upstream, SC is exactly "the singular chain complex of $X$ with $\mathbb{Z}$ coefficients." Homology of that complex is the usual $H_n(X;\mathbb{Z})$.
proof idea
One-line abbreviation: Hgrp X n is defined to be (SC X).homology n. No further proof obligations; Mathlib supplies homology of a chain complex of modules. Noncomputable because the singular-chain functor and homology are noncomputable in this setup.
why it matters
This is the workhorse homology object for the arc-complement and linking stack. Downstream, arcComplementsAcyclic states that every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement in every dimension $D$. Lemmas such as bounds_of_isZero, bounds_of_mv, and bounds_of_halves quantify vanishing of Hgrp W 1 or Hgrp _ 2 to conclude that 1-cycles bound, feeding the bisection argument (bad_step) that shrinks a nonbounding cycle along an arc.
In the Recognition Science forcing chain, spatial dimension $D=3$ is forced at T8; sphere-complement acyclicity and linking vanishing in high dimension are the topological substrate for that geometric uniqueness. The abbreviation keeps every later statement readable as ordinary singular homology rather than raw chain-complex homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.