Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Singular homology satisfies dimension and arbitrary additivity

Statement

For any abelian group G, H0(∗;G)≅G and Hn(∗;G)=0 for every integer n≠0. For every set-indexed family of pairs the canonical map ⨁αHn(Xα,Aα;G)⟶Hn(⨆αXα,⨆αAα;G) is an isomorphism. Together with the structural axioms, singular homology is an ordinary theory with coefficient group G.

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

[F1]

A CW pair is (X,A) with A a CW subcomplex of X, as in def-skeleta-cw-subcomplex-and-relative-cw-complex. Morphisms are all continuous maps of pairs, not just cellular maps. An ordinary unreduced homology theory assigns covariant functors hn from CW pairs to abelian groups, for every n∈Z, and natural homomorphisms ∂:hn(X,A)→hn−1(A), where hn(X)=hn(X,∅), satisfying: - Homotopic maps of pairs induce equal homomorphisms. - The inclusion maps and ∂ form an exact sequence ⋯→hn(A)→hn(X)→hn(X,A)→hn−1(A)→⋯. - For CW subcomplexes U,V of X=U∪V, inclusion induces hn(U,U∩V)≅hn(X,V). - For a point ∗, hn(∗)=0 when n≠0; write G=h0(∗). - For every set-indexed family of CW pairs, including the empty family, the inclusions induce ⨁αhn(Xα,Aα)≅hn(⨆αXα,⨆αAα). Thus hn(∅)=0. No finite-dimensionality or finite-cell restriction is implicit. (Unreduced homology theory on cw pairs)

[F2]

For every fixed abelian group G, singular homology Hn(−,−;G), extended by zero in negative degrees, satisfies homotopy invariance, pair exactness, naturality of the connecting maps, and CW excision in def-unreduced-homology-theory-on-cw-pairs. (Singular homology satisfies homotopy exactness and excision)

[F3]

For a topological space X and an abelian group G, the singular chain groups and boundary maps of def-singular-boundary-operator form the singular chain complex C∙(X;G):=(⋯→Cn(X;G)→∂nCn−1(X;G)→⋯ ), because thm-the-singular-boundary-squares-to-zero gives ∂n−1∂n=0. Its degree-n cycles and boundaries are Znsing(X;G):=ker⁡∂n,Bnsing(X;G):=im⁡∂n+1, in the sense of def-cycle-and-boundary-subobjects-of-a-complex. The nth singular homology group is the homology object of this chain complex: Hnsing(X;G):=Znsing(X;G)/Bnsing(X;G), equivalently Hn(C∙(X;G)) in the notation of def-homology-object-of-a-chain-complex. When the coefficient group is Z, write simply Cn(X) and Hn(X) when no confusion can arise. (The singular chain complex and singular homology)

[F4]

Let X=⨆α∈AXα be a disjoint union of topological spaces, and let G be an abelian group. Then for every n≥0, Hnsing(X;G)≅⨁α∈AHnsing(Xα;G). (The singular homology of a disjoint union is the direct sum)

Proof

1.1F3algebra

In the point complex there is one singular simplex in every nonnegative degree. The boundary on its copy of G is multiplication by ∑j=0n(−1)j: it is the identity for positive even n and zero for odd n; ∂0=0. Thus its homology is G in degree zero and zero in every other degree, also when G=0.

1.2F4F3

A singular simplex has connected domain and hence its image lies in a single summand of a disjoint union. The chain complex of a union is consequently the direct sum of the chain complexes; this is the chain mechanism underlying F4. Taking the quotient by the corresponding subspace chains gives the direct sum of the relative chain complexes.

2.1F1F2step 1.1step 1.2∎

A finite-support tuple is a cycle exactly when every coordinate is a cycle. It is a boundary exactly when every coordinate is a boundary: choose a bounding chain in each of its finitely many nonzero coordinates. Thus homology commutes with this direct sum. This includes the empty family, whose chain complex is zero, and a singleton family. With F2 this verifies all axioms of F1.

Depends on

Used by

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources