Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-09-10 (Codex)
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 ACω. Let i:S↪M be a closed smooth embedded submanifold. Then there are an open neighbourhood Ω⊆ν(S) of the zero section in the quotient normal bundle and a diffeomorphism Φ:Ω→U onto an open neighbourhood U of i(S) in M, with Φ(0p)=i(p) for every p∈S. Thus S has a tubular neighbourhood in M.

Facts & Assumptions

Given: Countable choice and a closed smooth embedded submanifold i:S↪M.

[A1]

Countable choice is The Axiom of Countable Choice (ACω). It covers the embedding, Euclidean tube and normal-bundle structures used below. No additional family of local inverse radii will be selected.

[F1]

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

[L1]

Under [A1], M admits a proper smooth embedding j:M→Rk; its image P=j(M) is an embedded submanifold and j:M→P is a diffeomorphism (Every smooth manifold embeds in some finite-dimensional Euclidean space, The image of a smooth embedding is an embedded submanifold).

[L2]

Under [A1], normal addition on the Euclidean normal bundle of P is a diffeomorphism from an open zero-section neighbourhood onto an open W⊇P (The Euclidean tubular neighbourhood theorem). That bundle's projection πP(p,v)=p is smooth and its addition is p+v (The normal addition map for a Euclidean submanifold).

[L3]

A smooth bundle metric is a fibrewise inner product with smooth local coefficients (Smooth bundle metrics). For such a metric on TM, the orthogonal complements Cp=(dip(TpS))⊥⊆Ti(p)M form a smooth subbundle C and the quotient map restricts to a smooth bundle isomorphism Q:C→ν(S), 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).

[L4]

The inclusion i 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).

[L5]

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

[L6]

Nonempty bounded-above real sets have suprema, with their least-upper-bound property (Complete ordered field (least-upper-bound property)).

Proof

technique · direct
1.1A1L1L2L5givenchoose

If S=∅, take the empty normal-bundle neighbourhood and empty diffeomorphism onto the open set ∅⊆M. Otherwise choose j:M→P⊆Rk by [L1] and use [L2] to obtain EP:Θ→W. Put R=πP∘EP−1:W→P. This is smooth and fixes P pointwise, since EP(p,0)=p. Thus a Euclidean retraction of a neighbourhood of the entire ambient manifold has been supplied without invoking the theorem being proved.

2.1A1L1L3L4step 1.1constructalgebra

Define a metric on TM by gx(v,w)=⟨djx(v),djx(w)⟩Rk. It is positive definite because djx is injective. Its coordinate coefficients are finite sums of products of first partial derivatives of the smooth coordinate functions of j, 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 C and Q:C→ν(S). For p∈S write b(p)=j(i(p)),λp(v)=dji(p)(v)(v∈Cp),∣v∣=∥λp(v)∥. Fibrewise, Ti(p)M=dip(TpS)⊕Cp.

3.1L3L4L5step 2.1constructalgebra

The map (p,v)↦(b(p),λp(v)) identifies C topologically with its image in Rk×Rk, and its coordinate expressions are smooth. To check the topology, work in a local frame e1,…,ec of C. The vectors λp(eα(p)) are linearly independent and smooth in p. Their Gram matrix is invertible, and the coefficients of a vector z 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 b, this proves the asserted inverse topology in every frame patch. For rank c=0 the same assertion just concerns the zero section. Thus the sets Va(p)={(q,v)∈C:∥b(q)−b(p)∥<a, ∣v∣<a} are open and form a neighbourhood basis at (p,0).

4.1L1L4L5step 1.1step 2.1step 3.1constructalgebra

Define the open subset D={(p,v)∈C:b(p)+λp(v)∈W} and the smooth map F:D→M,F(p,v)=j−1(R(b(p)+λp(v))). The coordinate formula in step 3.1 makes the addition smooth and continuous, so D is open and contains the zero section; also F(p,0)=i(p). At (p,0), local bundle coordinates identify T(p,0)C with TpS⊕Cp. Differentiating the addition sends (u,w) to dji(p)(dip(u)+w): derivatives of the frame vectors are multiplied by the zero fibre coordinates and vanish. Since R fixes P, differentiating that identity and using [L4] shows dF(p,0)(u,w)=dip(u)+w. This is an isomorphism by the direct sum in step 2.1. Therefore [L4] makes F a local diffeomorphism at each zero vector.

5.1L6step 3.1step 4.1constructalgebra

For each p∈S form the set Ap={a∈(0,1]:Va(p)⊆D, F∣Va(p) is a diffeomorphism onto an open subset of M}. The neighbourhood basis from step 3.1 and the local inverse from step 4.1 make Ap nonempty. It is bounded above by one, so let r(p)=sup⁡Ap∈(0,1] by [L6]. The cap is imposed BEFORE taking the supremum, and these unique supremum values require no simultaneous choice of inverse neighbourhoods. Every 0<a<r(p) is eligible: choose b∈Ap with a<b and restrict its diffeomorphism to Va(p).

6.1L5step 5.1algebra

The map F is a diffeomorphism on Vr(p)(p) as well. Each point there lies in a smaller Va(p) with a<r(p), hence in D and in a local diffeomorphism domain. Any two points lie in a COMMON such smaller domain, by taking a above their finitely many strict distance bounds. Thus F is injective on Vr(p)(p); 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.

7.1L6step 5.1step 6.1algebra

For p,q∈S and 0<a<r(p)−∥b(p)−b(q)∥, the triangle inequality gives Va(q)⊆Vr(p)(p) and a<1. Thus a∈Aq by step 6.1. Taking the supremum over such a when the upper endpoint is positive, and using r(q)>0 otherwise, proves r(q)≥r(p)−∥b(p)−b(q)∥. Interchanging p,q gives ∣r(p)−r(q)∣≤∥b(p)−b(q)∥. Hence r is positive and continuous on S.

8.1L5step 4.1step 6.1step 7.1construct

Shrink by TWO conditions, including displacement of the image in the Euclidean ambient space: ΩC={(p,v)∈D:∣v∣<r(p)/4, ∥j(F(p,v))−b(p)∥<r(p)/4}. All displayed functions are continuous, so ΩC is open. It contains every (p,0) because F(p,0)=i(p) and r(p)>0. At any (p,v)∈ΩC, one has (p,v)∈Vr(p)(p), so step 6.1 makes F∣ΩC a local diffeomorphism. No positive smooth radius or geodesic exponential is being assumed.

9.1step 6.1step 8.1algebra

If F(p,v)=F(q,w) for two points of ΩC, arrange r(q)≤r(p). With z=j(F(p,v))=j(F(q,w)), step 8.1 gives ∥b(p)−b(q)∥≤∥b(p)−z∥+∥z−b(q)∥<r(p)+r(q)4≤r(p)2<r(p). Also ∣v∣<r(p)/4 and ∣w∣<r(q)/4≤r(p)/4. Thus both points lie in Vr(p)(p), 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 b(p)+λp(v)=b(q)+λq(w).

10.1F1L3L5step 1.1step 2.1step 4.1step 8.1step 9.1construct∎

Set U=F(ΩC). Step 8.1 makes U open, and it contains i(S) because the zero section is included. By step 9.1, F:ΩC→U is bijective and a local diffeomorphism. Its inverse is smooth since the local smooth inverses agree, so it is a diffeomorphism. Finally put Ω=Q(ΩC)⊆ν(S),Φ=F∘Q−1:Ω→U. The bundle isomorphism Q is a diffeomorphism and sends zero vectors to zero vectors. Consequently Ω is open, contains the zero section, and Φ is a diffeomorphism with Φ(0p)=i(p). By [F1] this is the required tubular neighbourhood. Together with step 1.1 this proves the statement.

Depends on

Used by

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