ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck pass

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.

Compact isotopic submanifolds have isomorphic normal bundles and diffeomorphic complements

Example

Assume ${A C}_{ω}$ . Let $N$ be a smooth manifold without boundary, let $M$ be a compact smooth manifold and let $f_{0}, f_{1} : M \to N$ be isotopic embeddings with normal bundles $ν_{0} = f_{0}^{*} T N / T M$ and $ν_{1} = f_{1}^{*} T N / T M$ (Normal and conormal bundles of an embedded submanifold). Then $ν_{0} ≅ ν_{1}$ as smooth vector bundles over $M$ and $N ∖ f_{0} (M) ≅ N ∖ f_{1} (M)$ ; under AC every characteristic class defined on these normal bundles agrees (for orientation-dependent classes, use orientations transported by the displayed bundle isomorphism) and the complements are diffeomorphic. The example verifies the two embedding invariants supplied by isotopy: the ambient diffeomorphism of Isotopic embeddings of a compact manifold have diffeomorphic complements intertwines the normal bundles, and The isotopy extension theorem is the source of that diffeomorphism. (The converse fails: trivial normal bundles do not force isotopy, as the reflected-sphere counterexample on this page shows.)

Facts & Assumptions

Given: Countable choice, a boundaryless $N$ , a compact $M$ , isotopic embeddings $f_{0}, f_{1} : M \to N$ with normal bundles $ν_{0}, ν_{1}$ .

[F1]

Isotopic embeddings are joined by a smooth isotopy of embeddings (Smooth isotopies, diffeotopies and ambient isotopies, Smooth embeddings).

[L1]

Under ${A C}_{ω}$ there is a diffeomorphism $H : N \to N$ with $H \circ f_{0} = f_{1}$ , restricting to a diffeomorphism of pairs and of complements (Isotopic embeddings of a compact manifold have diffeomorphic complements, The isotopy extension theorem).

[L2]

Under countable choice the normal quotients have their smooth bundle structures by Assuming countable choice, normal and conormal bundles are smooth vector bundles. The chain rule is The chain rule for differentials of smooth maps. Under AC a characteristic class is natural in the bundle isomorphism class (Characteristic class as a universal natural bundle class). The normal bundle of the embedding $f_{i}$ is the fibrewise quotient $f_{i}^{*} T N / T M$ , with tangent maps $d f_{i}$ as in Normal and conormal bundles of an embedded submanifold, The tangent bundle as a disjoint union and The differential of a smooth map; a diffeomorphism $H$ carries $T N ∣_{f_{0} (M)}$ isomorphically onto $T N ∣_{f_{1} (M)}$ by its differential.

[A1]

Countable choice is inherited from [L1]; the bundle isomorphism below is an explicit induced map and selects nothing. The characteristic-class clauses additionally assume AC (The Axiom of Choice) (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Verification

technique · direct

1.1F1L1L2A1

By [L1] let $H$ be an ambient diffeomorphism with $H \circ f_{0} = f_{1}$ . Its differential restricts to a smooth bundle isomorphism $d H : T N ∣_{f_{0} (M)} \to T N ∣_{f_{1} (M)}$ covering $f_{1} \circ f_{0}^{- 1}$ .

2.1L2step 1.1

On the level of $M$ the map $d H$ induces a bundle map $ν_{0} \to ν_{1}$ over the identity of $M$ : by the chain rule, $d H$ carries the summand $d f_{0} (T M) \subseteq T N ∣_{f_{0} (M)}$ isomorphically onto $d f_{1} (T M) \subseteq T N ∣_{f_{1} (M)}$ , so it descends to an isomorphism of the fibrewise quotients $ν_{0} = f_{0}^{*} T N / T M \to ν_{1} = f_{1}^{*} T N / T M$ over ${i d}_{M}$ . A bundle map that is a linear isomorphism on each fibre is a bundle isomorphism, so $ν_{0} ≅ ν_{1}$ ; consequently the characteristic classes natural under this bundle isomorphism agree. For the characteristic-class construction assume additionally AC. Orientation-dependent classes agree when orientations are transported by it; unrelated choices of orientations are not being compared.

2.2L1step 1.1

The complement statement is the second conclusion of [L1]: $H$ restricts to a diffeomorphism $N ∖ f_{0} (M) \to N ∖ f_{1} (M)$ with smooth inverse. For the standard sphere and its reflection, the radial vectors at their image points give nowhere-zero smooth frames of the normal line bundles, so both are trivial. The reflected-sphere counterexample on this page proves they are not isotopic, establishing the parenthetical failure of the converse.

3.1step 2.1step 2.2∎

The normal bundles are isomorphic and the complements diffeomorphic, which is what the example claims.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

59 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.