Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05
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.

Zero-th singular homology is free on path components

Statement

For every topological space X, H0sing(X;Z)Cπ0path(X)ZeC, the free abelian group on the path components of X.

Facts & Assumptions

Given: A topological space X.

[L1]

Singular homology in degree 0 is Z0(X;Z)/B0(X;Z), and the reduced complex uses the augmentation kernel in degree 0 (The singular chain complex and singular homology, Augmentation at 0-simplices and reduced singular homology).

[L2]

A path component is the equivalence class of the path relation (Paths, path-connected spaces and path components).

Proof

technique · direct
1.1

Let Φ:C0(X;Z)Cπ0path(X)ZeC send each singular 0-simplex σ to the basis vector indexed by the path component of its unique image point. If τ:Δ1X is a singular 1-simplex, then the map sτ(1s,s) is a path in X from the image point of τδ1 to the image point of τδ0. Hence Φ(1τ)=0, so Φ kills B0(X;Z) and descends to a homomorphism Φ:H0sing(X;Z)Cπ0path(X)ZeC.

L1L2given
2.1

The map Φ is surjective: if X= there is nothing to prove, and otherwise any finite sum k=1makeCk is the image of the 0-cycle k=1makσk, where σk is any singular 0-simplex landing at a chosen point of Ck.

step 1.1L2
2.2

Let z=k=1makσk be a 0-cycle with Φ([z])=0. For each path component that meets the finite support of z, choose one base point simplex σC. Since Φ([z])=0, the total coefficient in each such component is zero. If σk and σC lie in the same path component, [L2] gives a path γk:IX from the image point of σk to the image point of σC. Define the singular 1-simplex γk:Δ1X by γk(t0,t1)=γk(t1). Then 1γk=σCσk. Therefore [z]=C(σkCak)[σC]=0 in H0sing(X;Z). Thus Φ is injective.

L1L2step 1.1algebra
3.1

Steps 2.1 and 2.2 show that Φ is an isomorphism, so H0sing(X;Z) is free on the path components of X.

step 2.1step 2.2

Depends on

Used by

Dependency tree · two levels

18 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