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.
The tubular neighbourhood theorem in a smooth ambient manifold
Statement
Assume countable choice . Let be a closed smooth embedded submanifold. Then there are an open neighbourhood of the zero section in the quotient normal bundle and a diffeomorphism onto an open neighbourhood of in , with for every . Thus has a tubular neighbourhood in .
Facts & Assumptions
Given: Countable choice and a closed smooth embedded submanifold .
Countable choice is The Axiom of Countable Choice (). It covers the embedding, Euclidean tube and normal-bundle structures used below. No additional family of local inverse radii will be selected.
A tubular neighbourhood means precisely the open normal-bundle neighbourhood and diffeomorphism fixed on the zero section specified in the statement (Tubular neighbourhoods of embedded submanifolds).
Under [A1], admits a proper smooth embedding ; its image is an embedded submanifold and is a diffeomorphism (Every smooth manifold embeds in some finite-dimensional Euclidean space, The image of a smooth embedding is an embedded submanifold).
Under [A1], normal addition on the Euclidean normal bundle of is a diffeomorphism from an open zero-section neighbourhood onto an open (The Euclidean tubular neighbourhood theorem). That bundle's projection is smooth and its addition is (The normal addition map for a Euclidean submanifold).
A smooth bundle metric is a fibrewise inner product with smooth local coefficients (Smooth bundle metrics). For such a metric on , the orthogonal complements form a smooth subbundle and the quotient map restricts to a smooth bundle isomorphism , under [A1] (Assuming countable choice, an ambient metric identifies the two normal bundles). Smooth vector bundles have local linear trivializations (Smooth vector bundles, rank, fibres, and trivial bundles).
The inclusion is a smooth embedding; differentials of composites satisfy the chain rule; an invertible differential gives a smooth local inverse (The inclusion of an embedded submanifold is a smooth embedding, The chain rule for differentials of smooth maps, The smooth inverse function theorem on manifolds).
Smooth composites are smooth, smooth maps are continuous, and smoothness is local (Identity maps and composites of smooth maps are smooth, Smooth maps are continuous, Smoothness is local on the source).
Nonempty bounded-above real sets have suprema, with their least-upper-bound property (Complete ordered field (least-upper-bound property)).
Proof
If , take the empty normal-bundle neighbourhood and empty diffeomorphism onto the open set . Otherwise choose by [L1] and use [L2] to obtain . Put This is smooth and fixes pointwise, since . Thus a Euclidean retraction of a neighbourhood of the entire ambient manifold has been supplied without invoking the theorem being proved.
Define a metric on by It is positive definite because is injective. Its coordinate coefficients are finite sums of products of first partial derivatives of the smooth coordinate functions of , so are smooth; hence it is the smooth bundle metric of [L3]. This is an explicitly constructed induced metric, not an invocation of a later Riemannian-metric existence theorem. Apply [L3] to obtain and . For write Fibrewise, .
The map identifies topologically with its image in , and its coordinate expressions are smooth. To check the topology, work in a local frame of . The vectors are linearly independent and smooth in . Their Gram matrix is invertible, and the coefficients of a vector in their span are its inner products with these vectors multiplied by the inverse Gram matrix. These coefficient functions are continuous (indeed smooth), by the cofactor formula and the nonzero determinant. Together with the subspace topology of the embedding , this proves the asserted inverse topology in every frame patch. For rank the same assertion just concerns the zero section. Thus the sets are open and form a neighbourhood basis at .
Define the open subset and the smooth map The coordinate formula in step 3.1 makes the addition smooth and continuous, so is open and contains the zero section; also . At , local bundle coordinates identify with . Differentiating the addition sends to : derivatives of the frame vectors are multiplied by the zero fibre coordinates and vanish. Since fixes , differentiating that identity and using [L4] shows This is an isomorphism by the direct sum in step 2.1. Therefore [L4] makes a local diffeomorphism at each zero vector.
For each form the set The neighbourhood basis from step 3.1 and the local inverse from step 4.1 make nonempty. It is bounded above by one, so let by [L6]. The cap is imposed BEFORE taking the supremum, and these unique supremum values require no simultaneous choice of inverse neighbourhoods. Every is eligible: choose with and restrict its diffeomorphism to .
The map is a diffeomorphism on as well. Each point there lies in a smaller with , hence in and in a local diffeomorphism domain. Any two points lie in a COMMON such smaller domain, by taking above their finitely many strict distance bounds. Thus is injective on ; its image is open and its local smooth inverses agree and give a smooth global inverse. This proves the supremum-endpoint claim, not merely local invertibility at zero.
For and , the triangle inequality gives and . Thus by step 6.1. Taking the supremum over such when the upper endpoint is positive, and using otherwise, proves Interchanging gives . Hence is positive and continuous on .
Shrink by TWO conditions, including displacement of the image in the Euclidean ambient space: All displayed functions are continuous, so is open. It contains every because and . At any , one has , so step 6.1 makes a local diffeomorphism. No positive smooth radius or geodesic exponential is being assumed.
If for two points of , arrange . With , step 8.1 gives Also and . Thus both points lie in , where step 6.1 gives injectivity. They are equal. The displacement condition is essential here: for this retracted map, equality of images alone does not imply the normal-addition identity .
Set . Step 8.1 makes open, and it contains because the zero section is included. By step 9.1, is bijective and a local diffeomorphism. Its inverse is smooth since the local smooth inverses agree, so it is a diffeomorphism. Finally put The bundle isomorphism is a diffeomorphism and sends zero vectors to zero vectors. Consequently is open, contains the zero section, and is a diffeomorphism with . By [F1] this is the required tubular neighbourhood. Together with step 1.1 this proves the statement.
Depends on
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Tubular neighbourhoods of embedded submanifolds
- Every smooth manifold embeds in some finite-dimensional Euclidean space
- The image of a smooth embedding is an embedded submanifold
- The Euclidean tubular neighbourhood theorem
- The normal addition map for a Euclidean submanifold
- Smooth bundle metrics
- Assuming countable choice, an ambient metric identifies the two normal bundles
- Smooth vector bundles, rank, fibres, and trivial bundles
- The inclusion of an embedded submanifold is a smooth embedding
- The smooth inverse function theorem on manifolds
- The chain rule for differentials of smooth maps
- Identity maps and composites of smooth maps are smooth
- Smooth maps are continuous
- Smoothness is local on the source
- Complete ordered field (least-upper-bound property)
Used by
- Compatible tubular neighbourhoods agree near compact sets up to ambient isotopy Corollary
- Every closed embedded submanifold has a smooth neighborhood retraction Corollary
- A homology cobordism need not be an h-cobordism Counterexample
- A nontrivial Whitney circle in the fundamental group blocks cancellation Counterexample
- The self-intersection number of a complementary-dimensional oriented submanifold Definition
- A closed three-manifold with H₁ = Z/2 and H₂ = 0 does not embed in S⁴ Lemma
- A vector field along an embedded submanifold extends to a neighbourhood and globally when the submanifold is closed Lemma
- Compatible tubular charts realize a prescribed normal identification Lemma
- Embedded bands joining two framed spheres exist Lemma
- Every bordism class is realized by an embedded collapse Lemma
- Metastable approximation of maps by embeddings Lemma
- Moving a sphere off a lower-dimensional submanifold Lemma
- Normal push-off zeros are the self-intersection points Lemma
- One transverse intersection gives the standard local cancelling model Lemma
- Oriented real two-plane splitting with real-cohomology injection Lemma
- Pullback of the Thom class along a transverse section computes the Euler class Lemma
- Relative Poincaré primitive near a submanifold Lemma
- Restriction of formal-immersion data has the parametric lifting property Lemma
- Spheres of adjacent critical levels have product neighbourhoods Lemma
- Stable normal data supplies framings of the surgery spheres below the middle dimension Lemma
- The collapse of a regular preimage is homotopic to the original map Lemma
- The complement of an oriented link is a connected smooth three-manifold Lemma
- The double cover branched over a slice disk is a rational homology ball Lemma
- The framing obstruction lives in the normal bundle of the surgery sphere Lemma
- The normal Thom class realizes the Poincare dual of a closed submanifold Lemma
- The orientation-twisted diagonal realizes the Lefschetz trace Lemma
- The velocity field of an isotopy extends to a neighbourhood Lemma
- Transverse holonomy transport is well defined and equivariant on the model Lemma
- Two points avoiding a finite set lie in a common embedded ball Lemma
- Zero- and one-handles are eliminated in a simply connected h-cobordism Lemma
- Two tubular neighbourhood germs are isomorphic near the zero section Proposition
- Local normal form near a coisotropic submanifold Theorem
- Morse homology is naturally isomorphic to singular homology Theorem
- Symplectic neighborhood theorem Theorem
- Weinstein Lagrangian neighborhood theorem Theorem
Dependency tree · two levels
75 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, 2nd ed., Theorem 6.24 and Proposition 6.25, pp.139-141 (standard reference, not scraped)
- Ralph L. Cohen, Bundles, Manifolds, and Homotopy, Chapter 8 section 1, Theorem 8.1, pp.237-239 (standard reference, not scraped)