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

De Rham cohomology depends only on the underlying homotopy type

Statement

Assume ${A C}_{ω}$ . Homotopy-equivalent underlying spaces of smooth manifolds, possibly with boundary, have isomorphic real de Rham cohomology groups in every degree. In particular this holds for homeomorphic underlying spaces. A specified continuous homotopy equivalence $f : M \to N$ induces the comparison-transported isomorphism $T_{f} = J_{M}^{- 1} f_{s i n g}^{*} J_{N}$ . When $f$ is smooth, this is its usual de Rham pullback. For smooth homotopies the resulting equality of endpoint maps agrees with the direct de Rham homotopy formula.

Facts & Assumptions

[F1]

De Rham vector-space comparison with continuous singular cohomology gives the degreewise natural linear isomorphisms $J_{M}$ , with smooth-map naturality and boundary manifolds included.

[F2]

Singular cohomology is homotopy invariant proves that homotopic continuous maps induce equal real singular cohomology maps and that a supplied homotopy equivalence gives inverse pullbacks.

[F3]

De rham cohomology is smooth homotopy invariant proves the direct smooth-homotopy-equivalence result in the earlier boundaryless de Rham theory.

[F4]

The de Rham homotopy formula extends to boundary manifolds gives $H_{1}^{*} - H_{0}^{*} = d L_{H} + L_{H} d$ in the locally extendible boundary convention.

[F5]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) is the assumption inherited by [F1].

Proof

Given: A continuous homotopy equivalence $f : M \to N$ of the underlying spaces, with a supplied inverse $g : N \to M$ and the two continuous inverse homotopies, and ${A C}_{ω}$ .

1.1

Define $T_{f} = J_{M}^{- 1} f_{s i n g}^{*} J_{N}$ and $T_{g} = J_{N}^{- 1} g_{s i n g}^{*} J_{M}$ . These are linear maps in the required contravariant directions by [F1] and [F2]. Cancelling the adjacent comparisons and applying [F2] gives $T_{f} T_{g} = J_{M}^{- 1} (g f)_{s i n g}^{*} J_{M} = 1, T_{g} T_{f} = J_{N}^{- 1} (f g)_{s i n g}^{*} J_{N} = 1.$ Thus $T_{f}$ is an isomorphism in every degree with the displayed inverse. A homeomorphism and its actual inverse meet the hypothesis with constant inverse homotopies.

F1F2F5given

2.1

For any two homotopic continuous maps $f_{0}, f_{1} : M \to N$ , [F2] gives $f_{0}^{*}_{s i n g} = f_{1}^{*}_{s i n g}$ , hence $T_{f_{0}} = T_{f_{1}}$ by the same conjugation formula. If $f$ is smooth, the naturality equation $J_{M} f_{d R}^{*} = f_{s i n g}^{*} J_{N}$ in [F1] gives $T_{f} = f_{d R}^{*}$ after applying $J_{M}^{- 1}$ . No pullback of a form by a merely continuous map has been defined.

F1F2step 1.1

3.1

For a smooth homotopy $H$ and a closed form $ω$ , [F4] gives the actual exact-form identity $H_{1}^{*} ω - H_{0}^{*} ω = d (L_{H} ω)$ , so the usual endpoint pullbacks are equal on de Rham cohomology. By step 2.1 these usual pullbacks are exactly the transported endpoint maps. Thus the direct homotopy-operator equality and the comparison-transported equality concern the same maps. On boundaryless smooth homotopy equivalences this also recovers [F3], and on boundary manifolds [F4] supplies the direct formula for smooth homotopies. Merely continuous inverse homotopies are handled only by the singular comparison in steps 1.1--2.1; no smooth pullback or direct de Rham homotopy formula is asserted for them.

F1F2F3F4step 1.1step 2.1

4.1

A homotopy equivalence with an empty space forces both spaces empty, so both maps in step 1.1 are the maps on zero groups. Degree zero, degree one, dimension-zero manifolds, negative degrees and the top form degree are included in [F1] and [F2]. Constant homotopies and both time endpoints are included in [F4]. The only choice use is that of [F5] in the global comparisons [F1]; [F2] and [F4] themselves are choice-free, and the inverse in step 1.1 uses the supplied $g$ and unique inverses of isomorphisms.

F1F2F4F5step 1.1step 2.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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)