TheoremStatement: 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.

Cup product Leibniz identity

Statement

For cochains $φ \in C^{p} (X; R)$ and $ψ \in C^{q} (X; R)$ , $p, q \geq 0$ , over a commutative unital ring with positive coboundary, $δ (φ ⌣ ψ) = δ φ ⌣ ψ + (- 1)^{p} φ ⌣ δ ψ .$ Thus the product of cocycles is a cocycle, and changing either cocycle representative by a coboundary changes their product by a coboundary.

Facts & Assumptions

[F1]

Singular cup product on cochains defines $φ ⌣ ψ = J (φ, ψ) D_{X}$ , with $D_{X}$ a chain map.

[F2]

The additive singular cohomology cross product is well-defined proves $δ J (φ, ψ) = J (δ φ, ψ) + (- 1)^{p} J (φ, δ ψ)$ on the signed tensor complex.

Proof

Given: $X, R, p, q, φ, ψ$ as stated. Negative cochain degrees are zero, and $δ^{2} = 0$ .

1.1

Since $D_{X} \partial = d D_{X}$ , precomposing the tensor-functional identity with $D_{X}$ gives $δ (φ ⌣ ψ) = J (φ, ψ) D_{X} \partial = J (φ, ψ) d D_{X} = (J (δ φ, ψ) + (- 1)^{p} J (φ, δ ψ)) D_{X} .$ By the cup formula this is exactly the asserted identity. If both inputs are closed its right side is zero.

F1F2given

2.1

Now assume $δ φ = δ ψ = 0$ . Let $u \in C^{p - 1} (X; R)$ and $v \in C^{q - 1} (X; R)$ . Bilinearity expands the change to $(φ + δ u) ⌣ (ψ + δ v) - φ ⌣ ψ = δ u ⌣ ψ + φ ⌣ δ v + δ u ⌣ δ v$ . Step 1.1, applied to each pair, identifies this as $δ (u ⌣ ψ + (- 1)^{p} φ ⌣ v + u ⌣ δ v) .$ Indeed the respective other Leibniz terms contain $δ ψ$ , $δ φ$ , or $δ^{2} v$ , and vanish. This proves simultaneous descent and, by setting $u = 0$ or $v = 0$ , each separate descent.

F1step 1.1given

3.1

If $p = 0$ , then $u = 0$ and its two terms in the primitive are absent; if $q = 0$ , then $v = 0$ and its terms are absent. For $p = q = 0$ both representatives are unchanged, while the Leibniz identity itself still holds, with sign $+ 1$ . At zero input or zero coefficient ring the equality is zero by bilinearity. An empty space has zero cochains, and a point or a degenerate simplex satisfies the same chain-map and tensor identities. No representative, basis, or primitive was chosen from an arbitrary family: the primitive is the displayed expression in the given $u, v$ . Thus no AC is used.

F1F2step 1.1step 2.1∎

Depends on

Used by

Relative cup product for an excisive triad Definition
Singular cohomology ring Definition
De Rham integration respects wedge and cup in cohomology Lemma
Relative cup products are natural and connector-compatible Proposition
Cohomological Kunneth cross product is a ring isomorphism Theorem

Dependency tree · two levels

8 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

Hatcher Lemma 3.6; Miller Lecture 28 (standard reference, not scraped)