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

De Rham integration is a cochain map

Statement

For every smooth manifold $M$ , possibly with boundary, integration is a real cochain map from its de Rham complex to its smooth singular cochain complex: $δ I_{M}^{k} (ω) = I_{M}^{k + 1} (d ω) (ω \in Ω^{k} (M)) .$ Both complexes are zero in negative degrees. The boundary convention for forms is the one in the definition of $I_{M}$ .

Facts & Assumptions

[F1]

De Rham integration cochain defines $I_{M}$ by integration and proves its real linearity in each degree, including the zero-map conventions.

[F2]

Stokes theorem for smooth singular chains gives $\int_{c} d ω = \int_{\partial c} ω$ for a smooth $(k + 1)$ -chain and a $k$ -form with $k \geq 0$ .

[F3]

Smooth singular chain and cochain complexes defines $(δ φ) (c) = φ (\partial c)$ , without an extra sign.

Proof

Given: A manifold $M$ , $k \geq 0$ , a form $ω \in Ω^{k} (M)$ and an arbitrary finite smooth $(k + 1)$ -chain $c$ .

1.1

The definition of the cochain differential, followed by integration and [F2], gives $(δ I_{M}^{k} (ω)) (c) = I_{M}^{k} (ω) (\partial c) = \int_{\partial c} ω = \int_{c} d ω = I_{M}^{k + 1} (d ω) (c) .$ The same coefficients and alternating boundary signs occur in [F2] and [F3], so no sign adjustment is required.

F1F2F3given

2.1

Since step 1.1 holds for every chain, the two linear functionals are equal. Together with the degreewise real linearity in [F1], this is precisely the cochain-map identity. For $k = 0$ it is the fundamental-theorem formula for values at the two endpoints of each smooth one-simplex, including constant paths. For $k = \dim M$ , the form $d ω$ is zero, and the same equality proves $δ I_{M}^{k} (ω) = 0$ without assuming there are no higher-dimensional singular simplices.

F1F2step 1.1

3.1

If $k > \dim M$ or $k < 0$ , the form and all relevant source differentials are zero, so the identity is an equality of zero cochains; this includes the map out of degree minus one. If $M$ is empty, both complexes are zero. Zero chains and degenerate simplices were included in [F2], so they create no exception to step 1.1. Every evaluation uses a finite chain and a previously well-defined integral; no choice axiom enters.

F1F2F3step 2.1∎

Depends on

Used by

The de Rham map is a cochain map without Stokes on simplices False statement
De Rham integration respects wedge and cup in cohomology Lemma
The de Rham map commutes with Mayer–Vietoris connectors Lemma
The de Rham map on cohomology is well defined Theorem

Cited to discharge well-definedness by De Rham integration cochain.

Dependency tree · two levels

13 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

Peter S. Park, Proof of de Rham's Theorem (standard reference, not scraped)