Alphabeta Math
LemmaStatement: 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.

Any ordinary homology theory has a cellular chain complex on a cw pair

Statement

For a CW pair (X,A) and an ordinary theory h with coefficient G, put F1=A and Fr=AXr for r0. Set Crh(X,A)=hr(Fr,Fr1)(r0),Crh=0(r<0). Each Crh is the direct sum of copies of G indexed by the relative r-cells. Define d0=0 and for r1 let dr be the triple boundary to hr1(Fr1,A) followed by its map to hr1(Fr1,Fr2). Then dr1dr=0, naturally for cellular maps of CW pairs.

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

[F1]

Let h be an ordinary theory with coefficient group G=h0(). For every n0 and kZ, hk(Dn,Sn1){Gk=n,0kn. At n=0 the pair means (,). Also h~k(Sn)G for k=n and zero otherwise, including n=0. Choose the disk identifications by ordered orientations and iterated cone boundaries, so they commute with these boundaries. (Any ordinary homology theory computes relative cell groups from its coefficient group)

[F2]

Ordinary unreduced theories on CW pairs and reduced ordinary theories on based CW spaces with vertex basepoints determine one another, naturally and compatibly with morphisms and coefficients. For A the correspondence gives hn(X,A)h~n(X/A); for A= it gives hn(X)h~n(X+), where X+=X{}. Under this correspondence, pair boundaries are cofiber boundaries followed by inverse suspension, and arbitrary disjoint-sum additivity corresponds to arbitrary wedge additivity. For a CW triple BAX there is a natural exact sequence hn(A,B)hn(X,B)hn(X,A)hn1(A,B), whose last map is the pair boundary followed by hn1(A)hn1(A,B). (Unreduced pair and reduced quotient axioms are equivalent on cw pairs)

[F3]

Write Xn for the union of cells of dimension at most n, with X1=. A CW subcomplex AX is a union of open cells such that, whenever A contains an open cell e, it contains the whole closure e. A relative CW complex (X,A) is formed from the subcomplex A by attaching cells in stages; thus AX is a cellular inclusion. (Skeleta, CW subcomplexes, and relative CW complexes)

Proof

1.1

By the skeletal definition F3, collapsing Fr1 leaves a wedge of one r-sphere per relative cell, using the disjoint-basepoint convention when Fr1 is empty. Quotient identification and arbitrary wedge additivity in F2, followed by F1, show hk(Fr,Fr1) is zero for kr and the stated direct sum for k=r. This includes no cells and zero-dimensional cells.

F1F2F3
1.2

Write δr:hr(Fr,Fr1)hr1(Fr1,A) for the triple boundary and ρr:hr(Fr,A)hr(Fr,Fr1) for the quotient map. The differential is dr=ρr1δr. Exactness of the triple (Fr1,Fr2,A) gives δr1ρr1=0.

F2
2.1

Consequently dr1dr=ρr2(δr1ρr1)δr=0 for r2; for r=1 it holds because d0=0. A cellular map preserves each Fr and all natural triple maps, so it commutes with these differentials. No sphere-map incidence identification has been used.

F2step 1.2algebra

Depends on

Used by

Dependency tree · two levels

7 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