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

Positive-degree cup products on a suspension vanish

Statement

For a nonempty CW complex X, its unreduced two-cone suspension ΣX, and a commutative unital ring R, every product of two positive-degree reduced cohomology classes is zero. In particular clR(ΣX)1. No AC is required.

Facts & Assumptions

[F2]

The exponential law: for a locally compact metric X and any spaces Z and Y, transposition is a bijection between C(X×Z,Y) and C(Z,C(X,Y)) with the compact-open topology applies with locally compact metric domain I=[0,1], arbitrary parameter space and arbitrary target. It makes a function on Z×I continuous precisely when its transpose ZC(I,Y) is continuous.

[F3]

Homotopic maps induce equal maps in singular cohomology gives homotopy invariance with arbitrary coefficients.

[F4]

Long exact sequence of a pair in singular cohomology identifies the kernel of restriction to a subspace with the image of its relative cohomology.

[F5]

Relative cup product for an excisive triad gives the product for two open subspaces and its canonical comparison to the union-relative target.

[F6]

Cup length over a coefficient ring defines cup length from nonzero finite positive-degree products.

Proof

Given: X,R as stated. Use the quotient map q:X×[0,1]ΣX of [F1].

1.1

We first justify homotopies on quotient cylinders. If r:EZ is quotient and a function h:Z×IY has continuous composite h(r×1), its paths are continuous by surjectivity of r. By [F2], the transpose upstairs is continuous and equals h^r. The quotient criterion makes h^ continuous, hence [F2] makes h continuous. This does not assume that an arbitrary product preserves quotient maps.

F2given
1.2

The singular cochain complex of a point has one copy of R in each nonnegative degree. The boundary of its unique degree-n simplex has coefficient i=0n(1)i, equal to 1 for positive even n and 0 for odd n. With positive coboundary the differential from degree k is therefore identity for odd k and zero for even k. Every positive-degree cocycle is consequently a coboundary, while H0()=R.

given
2.1

Let U=q(X×[0,2/3)) and V=q(X×(1/3,1]). Their inverse images are saturated open sets, so U,V are open, their restrictions of q are quotient maps, and they cover ΣX. On U set hs([x,t])=[x,(1s)t], a contraction to its lower apex. On V use ks([x,t])=[x,1(1s)(1t)], a contraction to its upper apex. Each formula is continuous before quotienting, is constant on the collapsed face, and stays in the indicated set. Step 1.1 proves that the descended homotopies are continuous, including at their apex and time endpoints.

F1step 1.1
3.1

Steps 1.2 and 2.1, together with [F3], give Hp(U;R)=Hq(V;R)=0 for p,q>0. Let aHp(ΣX;R) and bHq(ΣX;R), with positive degrees (equivalently reduced classes). Their restrictions to U,V respectively vanish. By [F4], there exist relative classes a~Hp(ΣX,U;R) and b~Hq(ΣX,V;R) mapping to a,b. This uses only two witnesses from exactness.

F3F4step 1.2step 2.1
4.1

Their [F5] relative product belongs to Hp+q(ΣX,UV;R)=Hp+q(ΣX,ΣX;R)=0, since the relative chain quotient is zero. Its image in absolute cohomology is ab: both are obtained by the same front/back formula and the quotient comparison commutes with the map to the empty subspace. Hence ab=0.

F5step 3.1
5.1

Every product of length at least two vanishes, by applying step 4.1 to the first two factors and associating the rest. Thus [F6] gives cup length at most one, allowing zero when all positive-degree classes vanish. This includes point X, disconnected X, and R=0. The nonempty hypothesis ensures both apices in the prescribed quotient; the separately stipulated empty suspension is outside this statement. Degree-zero factors are excluded, as they could be units. Cochains in step 1.2 and the relative construction retain degenerate simplices. The homotopies are explicit and the only selections in step 3.1 are finite, so no AC is used.

F6step 1.2step 2.1step 3.1step 4.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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