CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Isotopic embeddings of a compact manifold have diffeomorphic complements

Statement

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. Then there is a diffeomorphism $H : N \to N$ with $H \circ f_{0} = f_{1}$ ; consequently $H$ restricts to a diffeomorphism of pairs $(N, f_{0} (M)) ≅ (N, f_{1} (M))$ , hence restricts to a diffeomorphism of complements $N ∖ f_{0} (M) ≅ N ∖ f_{1} (M) .$ Moreover, if $W$ is a smooth manifold containing $M$ as an embedded submanifold and $f_{0}$ extends to an embedding $W \to N$ , then $f_{1}$ extends to an embedding $W \to N$ as well.

Facts & Assumptions

Given: Countable choice, a boundaryless $N$ , compact $M$ and isotopic embeddings $f_{0}, f_{1} : M \to N$ .

[F1]

Isotopic embeddings are joined by a smooth isotopy $F : M \times I \to N$ with $F_{0} = f_{0}$ and $F_{1} = f_{1}$ ; an ambient isotopy $H$ of $N$ extends $F$ when $H_{t} \circ F_{0} = F_{t}$ (Smooth isotopies, diffeotopies and ambient isotopies).

[L1]

Under ${A C}_{ω}$ , every smooth isotopy of a compact $M$ , possibly with boundary, into a boundaryless $N$ extends to an ambient isotopy supported in any prescribed neighbourhood of its image, with no constancy assumption near the ends (The isotopy extension theorem, clause 4). [F1]

[L2]

A diffeomorphism is a bijective smooth map with smooth inverse; a smooth embedding is an injective immersion that is a homeomorphism onto its image (Diffeomorphisms and local diffeomorphisms of manifolds, Smooth embeddings).

[A1]

Countable choice is inherited from the extension theorem [L1]; the rest of the argument selects nothing (The Axiom of Countable Choice ( ${A C}_{ω}$ ), Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

Proof

technique · direct

1.1F1L1A1

Let $F : M \times I \to N$ be an isotopy with $F_{0} = f_{0}$ and $F_{1} = f_{1}$ by [F1]; since $M$ is compact and [L1] allows source boundary with the isotopy definition's product-corner coordinate convention, [L1] applied to $F$ produces an ambient isotopy $H : N \times I \to N$ with $H_{t} \circ f_{0} = F_{t}$ for all $t \in I$ , supported in a prescribed neighbourhood of $F (M \times I)$ .

2.1L2step 1.1

The time-one map $H_{1}$ is a diffeomorphism of $N$ by [L2] and satisfies $H_{1} \circ f_{0} = F_{1} = f_{1}$ ; hence it restricts to a bijection $f_{0} (M) \to f_{1} (M)$ with smooth inverse (the restriction of $H_{1}^{- 1}$ ), so it is a diffeomorphism of pairs $(N, f_{0} (M)) \to (N, f_{1} (M))$ and carries $N ∖ f_{0} (M)$ onto $N ∖ f_{1} (M)$ with smooth inverse, giving the claimed diffeomorphism of complements.

3.1L2step 2.1

The extension clause: if $g : W \to N$ is an embedding extending $f_{0}$ , then $H_{1} \circ g : W \to N$ is a smooth map with injective differential (a composite of the immersion $g$ and the diffeomorphism $H_{1}$ ) and is injective because $H_{1}$ and $g$ are; it is a smooth embedding again by [L2] applied to the composite, and it extends $f_{1}$ because $(H_{1} \circ g) ∣_{M} = H_{1} \circ f_{0} = f_{1}$ .

4.1step 2.1step 3.1∎

The claims are steps 2.1 and 3.1.

Depends on

Used by

Compact isotopic submanifolds have isomorphic normal bundles and diffeomorphic complements Example

Dependency tree · two levels

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