CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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 is continuous homotopy invariant on smooth manifolds

Statement

Assume countable choice ${A C}_{ω}$ . Continuously homotopic smooth maps induce equal de Rham maps. Continuous homotopy equivalences between smooth manifolds induce inverse de Rham graded algebra maps via smooth representatives, independently of those representatives.

Facts & Assumptions

Given: Boundaryless smooth manifolds and countable choice. First let $F : P \to N$ be continuous and smooth on an open $V$ containing a closed set $A$ .

[F1]

Smoothly homotopic maps induce the same de rham map: Smoothly homotopic smooth maps induce equal maps on de Rham cohomology in every degree.

[F2]

De rham cohomology is smooth homotopy invariant: A smooth homotopy equivalence induces an isomorphism of de Rham graded real algebras.

[F3]

The standard smooth step function: Let $β$ be the standard flat function. The standard smooth step function is $σ (t) : = \frac{β (t)}{β (t) + β (1 - t)} .$ Because $β$ is smooth and positive on $(0, \infty)$ , the denominator is positive on $(0, 1)$ , while $σ (t) = 0$ for $t \leq 0$ and $σ (t) = 1$ for $t \geq 1$ .

[F4]

Precomposition and postcomposition by continuous maps preserve homotopies, including their relative form: Let $f, g : X \to Y$ be continuous and suppose $f ≃_{A} g$ for a subspace $A \subseteq X$ . 1. If $u : W \to X$ is continuous, $B \subseteq W$ , and $u [B] \subseteq A$ , then $f \circ u ≃_{B} g \circ u$ . 2. If $v : Y \to Z$ is continuous, then $v \circ f ≃_{A} v \circ g$ .

[F5]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): The Axiom of Countable Choice, written ${A C}_{ω}$ , is the following statement. > For every family $(X_{n})_{n \in N}$ of nonempty sets indexed by > $N$ there is a function $f$ with domain $N$ such that > $f (n) \in X_{n}$ for every $n \in N$ . Equivalently, in the vocabulary of def-choice-function: every at most countable family of nonempty sets (def-countable) has a choice function.

[F6]

Products of smooth manifolds have a canonical product smooth structure: Let $(M, S)$ and $(N, T)$ be smooth manifolds of dimensions $m$ and $n$ . Then $M \times N$ with the product topology is a topological $(m + n)$ -manifold. If $A$ and $B$ are smooth atlases with $[A] = S$ and $[B] = T$ , then the set of product charts $A \times B : = {(V \times W, φ \times ψ) : (V, φ) \in A, (W, ψ) \in B}$ is a smooth atlas on $M \times N$ , and the maximal atlas it generates is independent of the presenting atlases: it depends only on $S$ and $T$ . This maximal atlas is the product smooth structure of $M \times N$ .

[F7]

Every smooth manifold embeds in some finite-dimensional Euclidean space: Assume countable choice ${A C}_{ω}$ . Every smooth manifold embeds smoothly in some finite-dimensional Euclidean space. More precisely, for a smooth $n$ -manifold $M$ there are a bounded smooth map $G : M \to R^{4 (2 n + 1)}$ and a smooth nonnegative proper exhaustion $ρ : M \to R$ such that $J : M ⟶ R^{4 (2 n + 1)} \times R, J (p) = (G (p), ρ (p))$ is a proper smooth embedding. In particular the bounded-plus-proper form is available when $M$ is noncompact.

[F8]

Whitney approximation for Euclidean-valued maps: Assume countable choice ${A C}_{ω}$ . Let $F : M \to R^{k}$ be continuous, where $M$ is a smooth manifold, and let $ε : M \to (0, \infty)$ be a positive continuous error function. Then there exists a smooth map $\tilde{F} : M \to R^{k}$ such that $∥ \tilde{F} (p) - F (p) ∥ < ε (p) for all p \in M .$

[F9]

Smooth partitions of unity exist on manifolds: Every open cover of a smooth manifold admits a smooth partition of unity subordinate to it.

[F10]

Smooth partitions of unity subordinate to an open cover: Let $M$ be a smooth manifold and let $(U_{i})_{i \in I}$ be an open cover of $M$ . A family of smooth functions $(ϕ_{i})_{i \in I}$ with $ϕ_{i} : M \to [0, 1]$ is a smooth partition of unity subordinate to $(U_{i})_{i \in I}$ when: 1. the family $(supp (ϕ_{i}))_{i \in I}$ is locally finite; 2. $supp (ϕ_{i}) \subseteq U_{i}$ for every $i \in I$ ; and 3. $\sum_{i} ϕ_{i} (p) = 1$ for every $p \in M$ .

[F11]

The normal addition map for a Euclidean submanifold: Let $S \subseteq R^{m}$ be an embedded smooth submanifold. Using the Euclidean inner product, define its orthogonal normal bundle by $N^{⊥} S : = {(p, v) \in S \times R^{m} : v ⊥ T_{p} S} .$ Local slice charts and orthogonal projection onto $T_{p} S$ give this set its standard smooth rank- $(m - \dim S)$ vector-bundle structure. The normal addition map is $E : N^{⊥} S \to R^{m}, E (p, v) : = p + v .$ It restricts on the zero section to the inclusion $S ↪ R^{m}$ and is the basic model map used to build Euclidean tubular neighbourhoods.

[F12]

Normal addition is a local diffeomorphism along the zero section: Let $S \subseteq R^{m}$ be an embedded smooth submanifold, and let $E : N^{⊥} S \to R^{m}$ be its normal addition map. For every $p \in S$ the differential $d E_{(p, 0)} : T_{(p, 0)} (N^{⊥} S) \to T_{p} R^{m} ≅ R^{m}$ is an isomorphism. Consequently, $E$ is a local diffeomorphism at every point of the zero section.

Proof

technique · direct

1.1

If $P$ is empty the smoothing assertion is immediate; if $N$ is empty a map forces $P$ empty. Otherwise the repaired embedding theorem gives a proper smooth embedding $j : N \to R^{m}$ under the assumed countable choice. Put $S = j (N)$ and let $E (p, v) = p + v$ on its orthogonal normal bundle. The bundle has the subspace topology in $S \times R^{m}$ , and $E$ is a local diffeomorphism at every $(p, 0)$ .

F5F7F11F12given

1.2

Apply the partition theorem to ${V, P ∖ A}$ . In its refinement-indexed output assign a function to $V$ whenever its support is contained in $V$ , and to $P ∖ A$ otherwise. Let $χ$ be the sum of the first group. Locally finite smooth sums give $0 \leq χ \leq 1$ and smoothness. Each grouped union of closed supports is closed, since locally it is a finite union; the first is contained in $V$ , and the second misses $A$ . Therefore $supp χ \subseteq V$ , and $χ = 1$ on the open complement of the second union, a neighbourhood of $A$ .

F9F10given

2.1

For $p \in S$ put $V_{a} (p) = {(q, v) : ∣ q - p ∣ < a, ∣ v ∣ < a}$ and let $h (p)$ be the supremum of the radii $0 < a \leq 1$ for which $E ∣_{V_{a} (p)}$ is a diffeomorphism onto its image. Local invertibility and the subspace topology provide at least one such radius, so $0 < h (p) \leq 1$ . Eligibility is downward closed, and every $a < h (p)$ is smaller than an eligible radius. Each point or pair of points in $V_{h (p)} (p)$ therefore lies in a smaller eligible set: $E$ is locally invertible and injective on all of $V_{h (p)} (p)$ .

step 1.1construct

2.2

The countable-choice cost in this partition application can be implemented in its coordinate-ball construction as follows. Form all admissible chart tuples, and for each member of a fixed countable basis contained in an eligible chart use countable choice to select a tuple; these charts cover. Take least suitable integer indices in the exhaustion refinement. For each compact annulus, the set of finite ordered lists of nested chart pairs covering it is nonempty by compactness; countable choice selects those lists and then the countable family of bump functions. Their normalized locally finite sum is the partition used above. This uses no point-indexed choice and no dependent choice.

F5F9step 1.2

3.1

If $0 < a < h (p) - ∣ p - q ∣$ , the triangle inequality gives $V_{a} (q) \subseteq V_{h (p)} (p)$ . The restriction of an injective local diffeomorphism to this open set is a diffeomorphism onto its open image, so $h (q) \geq a$ . Taking suprema, and exchanging $p, q$ , proves $∣ h (p) - h (q) ∣ \leq ∣ p - q ∣$ ; when the lower bound is nonpositive, positivity suffices. Thus $h$ is continuous.

step 2.1algebra

4.1

The set $Ω = {(p, v) : ∣ v ∣ < h (p) / 2}$ is open, and $E$ is locally invertible there. If $E (p, v) = E (q, w)$ , relabel so $h (q) \leq h (p)$ . Then $∣ p - q ∣ \leq ∣ v ∣ + ∣ w ∣ < (h (p) + h (q)) / 2 \leq h (p)$ , and both pairs lie in $V_{h (p)} (p)$ . Its injectivity gives $(p, v) = (q, w)$ . Hence $E : Ω \to U = E (Ω)$ is an injective open local diffeomorphism; its local smooth inverses agree. The map $r = π E^{- 1} : U \to S$ is smooth and satisfies $r (p) = p$ .

F11step 2.1step 3.1

5.1

If $U^{c}$ is nonempty, set $e (x) = \min (1, dist (j F (x), U^{c}) / 2)$ , and otherwise set $e = 1$ . For a nonempty set $B \subseteq R^{m}$ , triangle inequalities and infima give $∣ dist (z, B) - dist (z', B) ∣ \leq ∣ z - z' ∣$ ; distances are finite by fixing one point of $B$ . Openness of $U$ makes this distance positive at $j F (x)$ . Thus $e$ is finite, positive and continuous, and $B_{e (x)} (j F (x)) \subseteq U$ . Euclidean Whitney approximation supplies smooth $Q : P \to R^{m}$ with $∣ Q - j F ∣ < e$ .

F5F8step 4.1

6.1

Put $R = χ j F + (1 - χ) Q$ . It is smooth on $V$ , and outside $supp χ$ it agrees locally with $Q$ , hence is globally smooth. It agrees with $j F$ near $A$ , and $∣ R - j F ∣ = (1 - χ) ∣ Q - j F ∣ < e$ . Consequently $G = j^{- 1} r R$ is smooth, agrees with $F$ near $A$ , and $j^{- 1} r ((1 - s) j F + s R)$ is a continuous homotopy from $F$ to $G$ fixed on $A$ : its whole segment stays in $B_{e} (j F)$ .

step 4.1step 5.1step 1.2

7.1

Now let $H : M \times [0, 1] \to N$ continuously join smooth maps $f_{0}, f_{1}$ . On the smooth product $P = M \times R$ , put $λ (t) = σ (3 t - 1)$ and $F (x, t) = H (x, λ (t))$ . It is smooth on $V = M \times ((- \infty, 1 / 3) \cup (2 / 3, \infty))$ , where it equals an endpoint map. The closed set $A = M \times ((- \infty, 1 / 4] \cup [3 / 4, \infty))$ lies in $V$ . Step 6.1 gives a smooth map fixed near these collars. Its restriction to $M \times [0, 1]$ is a smooth homotopy with exact endpoints $f_{0}, f_{1}$ . Thus their induced maps agree.

F1F3F6step 6.1

8.1

Taking $A = V = \emptyset$ and $χ = 0$ in step 6.1 gives a smooth representative of every continuous map, with an explicit homotopy to it. If continuous $f, g$ are homotopy inverses, choose smooth representatives $f', g'$ . Composition of homotopies and their concatenation give $g' f' ≃ id$ and $f' g' ≃ id$ . Step 7.1 smooths each of these endpoint homotopies; smooth homotopy invariance now makes $(f')^{*}, (g')^{*}$ inverse graded algebra maps. Two smooth representatives of one continuous class are continuously homotopic by concatenation, so step 7.1 also proves independence.

F2F4step 6.1step 7.1∎

Source locator

Lee, Theorem 6.21, pp.136–137; normal addition and tubular retraction, pp.137–141; Theorem 6.26, p.141; Theorem 17.11, pp.445–446. The bounded supremum tube proof and smaller closed collars are the explicit local construction here, supported by the declared normal-addition local inverse. The current published embedding and absolute approximation proofs, repaired 2026-09-09, were read in full; no historical relative-Whitney assertion is imported.

Depends on

Used by

De rham cohomology of a contractible smooth manifold Theorem

Dependency tree · two levels

70 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

John M. Lee, Introduction to Smooth Manifolds, second edition (standard reference, not scraped)