Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedaudited 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.

Singular cup product on cochains

Definition

Let X be a space, let R be a commutative unital ring, and use the positive coboundary δφ=φ of Singular cochain complex with coefficients. For p,q0 and cochains φCp(X;R), ψCq(X;R), their cup product is (φψ)(σ)=φ(σ[0,,p])ψ(σ[p,,p+q])(σ:Δp+qX). Extend from simplex generators R-linearly. The product is R-bilinear in the cochains by distributivity and commutativity in R. Zero or negative-degree inputs give zero.

With J(φ,ψ) the tensor functional of Additive singular cohomology cross product and A=AW from Alexander–Whitney map and diagonal approximation, this is exactly J(φ,ψ)AΔ#. Indeed only the cut of bidegree (p,q) survives. Equivalently, define the AW external cochain by J(φ,ψ)A and pull it back along the diagonal. There is no extra cochain sign.

The earlier additive cohomology cross product was expressed through a specified shuffle inverse T. The comparison with it is an equality of classes: Alexander--Whitney and shuffle are natural chain-homotopy inverses constructs K with AT=dK+Kd. For cocycles, The additive singular cohomology cross product is well-defined gives Jd=0, hence J(AT)Δ#=JKdΔ#=δ(JKΔ#). Here postcomposition with the diagonal commutes with boundary, as proved in the diagonal definition. Thus the AW cup class equals diagonal pullback of the earlier external product; equality of the two chosen external cochains is not required. At total degree zero the displayed primitive is zero and the identity is literal. The same tensor-functional identity gives δ(JAΔ#)=0 for cocycles, so the compared classes exist.

For degree-zero cochains the formula on a vertex is ordinary multiplication of their values. A constant cochain of value 1 multiplies any cochain on either side without changing it, including on disconnected spaces. On empty X or over R=0 all cochains and products are zero. Face restrictions make sense for every singular simplex, including degenerate ones. A bare abelian coefficient group has no specified multiplication to insert in this formula. No AC or selection of representatives is used in this definition or comparison.

Depends on

Used by

Dependency tree · two levels

16 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