Alphabeta Math
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.

✓ 37 results · all verified · 9 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 28 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Smooth Vector Bundles and Sections

1 · Prerequisites

2 · Summary

This page turns finite-rank smooth vector bundles into usable global objects. It starts from local triviality and transition functions, constructs bundles from cocycles, and then moves through sections, frames, bundle maps, pullbacks, Whitney sums, quotient bundles, bundle metrics, complements, and the normal and conormal bundles of an embedded submanifold.

The two main traps on this page are kept explicit. First, smoothness and local triviality are always checked in honest bundle charts rather than by fibrewise set theory. Second, the image of a bundle map over a non-identity base map belongs naturally in a pullback bundle, not naively in the original target over its old base.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Smooth fibre bundles and local trivializations

Definition

Let M and E be smooth manifolds, let F be a smooth manifold, and let π:E→M be a smooth surjection.

A smooth local trivialization with model fibre F on an open set U⊆M is a diffeomorphism

Φ:π−1(U)→U×F

over U, meaning that pr⁡1∘Φ=π.

The map π:E→M is a smooth fibre bundle with model fibre F when there is an open cover (Uα) of M such that each restriction π−1(Uα)→Uα admits a smooth local trivialization.

Thus each point of M has a neighborhood on which E is smoothly identified with a product over the identity on the base.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Smooth vector bundles, rank, fibres, and trivial bundles

Definition

Let π:E→M be a smooth fibre bundle and let r∈N.

A smooth vector bundle of rank r is a smooth fibre bundle for which every fibre Ep:=π−1(p) is an r-dimensional real vector space and there is an open cover (Uα) of M such that each restriction π−1(Uα)→Uα admits a local trivialization

Φα:π−1(Uα)→Uα×Rr

whose restriction on each fibre Ep is a linear isomorphism Ep→Rr.

The fibre over p∈M is called the fibre at p. A vector bundle is trivial when it is globally isomorphic over M to the product bundle M×Rr→M.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

A vector bundle projection is a surjective submersion

Statement

If π:E→M is a smooth vector bundle, then π is a surjective submersion.

Facts & Assumptions

Given: A smooth vector bundle π:E→M.

[L1]

A smooth vector bundle is, in particular, a smooth fibre bundle with local trivializations over the identity on the base (Smooth vector bundles, rank, fibres, and trivial bundles).

[L2]

A smooth map is a submersion exactly when its differential is surjective at every point (Immersions, submersions, and constant-rank maps).

Proof

technique · direct
1.1L1given

Surjectivity is part of the definition of a smooth fibre bundle, so π is surjective. Fix e∈E with p=π(e), and choose a local trivialization Φ:π−1(U)→U×Rr around e. In this chart, π becomes the product projection pr⁡1:U×Rr→U.

2.1L2step 1.1algebra∎

In product coordinates the differential of pr⁡1 is the coordinate projection TpU⊕TvRr→TpU, which is surjective. Therefore dπe is surjective, and since e was arbitrary, π is a submersion by [L2].

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Vector bundle charts and transition functions

Definition

Let π:E→M be a smooth rank-r vector bundle and let Φα:π−1(Uα)→Uα×Rr be a local trivialization whose restriction on each fibre is a linear isomorphism. The pair (Uα,Φα) is a vector bundle chart.

For two vector bundle charts (Uα,Φα) and (Uβ,Φβ), the overlap map

Φβ∘Φα−1:(Uα∩Uβ)×Rr→(Uα∩Uβ)×Rr

has the form

Φβ∘Φα−1(p,v)=(p,gβα(p)v),

where gβα:Uα∩Uβ→GL(r,R) is smooth. The map gβα is the transition function from chart α to chart β.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Vector bundle transition functions satisfy the cocycle identities

Statement

For vector bundle charts on a rank-r bundle, the transition functions satisfy

gαα(p)=Ir,gγα(p)=gγβ(p)gβα(p)

on every overlap where the expressions are defined.

Facts & Assumptions

Given: Three vector bundle charts (Uα,Φα), (Uβ,Φβ), and (Uγ,Φγ) on one rank-r bundle.

[L1]

In a vector bundle chart overlap, Φβ∘Φα−1(p,v)=(p,gβα(p)v) with gβα(p)∈GL(r,R) (Vector bundle charts and transition functions).

Proof

technique · direct
1.1L1given

On Uα, the map Φα∘Φα−1 is the identity, so [L1] gives (p,gαα(p)v)=(p,v) for every v∈Rr. Hence gαα(p)=Ir.

2.1L1step 1.1algebra∎

On a triple overlap, Φγ∘Φα−1=(Φγ∘Φβ−1)∘(Φβ∘Φα−1). Applying [L1] to (p,v) gives (p,gγα(p)v)=(p,gγβ(p)gβα(p)v) for every v, so gγα(p)=gγβ(p)gβα(p).

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Construction of a vector bundle from a smooth cocycle

Statement

Let M be a smooth manifold, let (Uα)α∈A be a supplied countable open cover of M, let r∈N, and let gβα:Uα∩Uβ→GL(r,R) be smooth maps satisfying the identities of Vector bundle transition functions satisfy the cocycle identities. Then the quotient of ∐α∈A(Uα×Rr) by the relation

(p,v)α∼(p,gβα(p)v)β

is a smooth rank-r vector bundle over M.

Facts & Assumptions

Given: A smooth manifold M, a supplied countable open cover (Uα), and a smooth GL(r,R)-cocycle gβα on the overlaps.

[L1]

The transition functions satisfy the identity and cocycle laws on all overlaps (Vector bundle transition functions satisfy the cocycle identities).

[L2]

A countable disjoint union of fixed-dimensional smooth manifolds carries the obvious smooth-manifold structure (Countable disjoint unions of fixed-dimensional smooth manifolds are smooth manifolds).

[F1]

The quotient topology is the topology for which a set is open exactly when its full preimage under the quotient map is open (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection).

Proof

technique · direct
1.1L1givenconstruct

Let X=∐α∈A(Uα×Rr) and declare (p,v)α∼(q,w)β when p=q∈Uα∩Uβ and w=gβα(p)v. By [L1], this relation is reflexive, symmetric, and transitive, so it is an equivalence relation on X.

2.1F1L1step 1.1

Let E=X/∼ and write q:X→E for the quotient map. For each α, define ψα:q(Uα×Rr)→Uα×Rr by ψα([p,v]α)=(p,v). The cocycle relation shows that every class meeting Uα×Rr has a unique representative there, so ψα is bijective. Its domain is open because q−1(q(Uα×Rr)) is the union over β of the open sets {(p,gαβ(p)w)β:p∈Uα∩Uβ, w∈Rr}, whence [F1] makes ψα a homeomorphism onto an open subset.

3.1L1step 2.1algebra

On overlaps, ψβ∘ψα−1(p,v)=(p,gβα(p)v), so the chart changes are smooth with smooth inverses. The projection π([p,v]α)=p is well defined and in chart α is the product projection Uα×Rr→Uα, while the fibre maps are linear by construction. Therefore the ψα form a smooth rank-r vector-bundle atlas on E→M.

4.1L2step 2.1step 3.1∎

Because the cover is countable and each chart image has a countable base, these bundle charts give E a countable base. Hausdorffness is local in the charts when two classes are distinct over one base point, and over different base points it comes from Hausdorffness of M. Hence E is a smooth manifold, and π:E→M is the required smooth vector bundle.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Isomorphic cocycles define isomorphic vector bundles

Statement

Suppose two smooth rank-r cocycles on the same open cover satisfy

gβα′(p)=hβ(p)gβα(p)hα(p)−1

for smooth maps hα:Uα→GL(r,R). Then the two cocycles define isomorphic smooth vector bundles.

Facts & Assumptions

Given: Two smooth cocycles (gβα) and (gβα′) on the same cover, together with a gauge family (hα) satisfying the displayed relation.

[L1]

A smooth cocycle on a countable cover determines a smooth vector bundle by the quotient construction (Construction of a vector bundle from a smooth cocycle).

Proof

technique · direct
1.1L1givenconstruct

On the α-th trivializing piece define Hα(p,v)=(p,hα(p)v). If (p,v)α∼(p,gβα(p)v)β, then the gauge relation gives Hβ(p,gβα(p)v)=(p,gβα′(p)hα(p)v)=Hα(p,v), so the local maps descend to a well-defined bundle map H:E→E′.

2.1L1step 1.1algebra∎

In the quotient charts of [L1], the descended map is (p,v)↦(p,hα(p)v), hence smooth and fibrewise linear. Replacing hα by hα−1 gives the inverse construction, so H is a smooth bundle isomorphism.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Restrictions of vector bundles

Definition

Let π:E→M be a smooth vector bundle and let U⊆M be open. The restriction of E to U is

E∣U:=π−1(U)

with projection π∣E∣U:E∣U→U.

The fibres of E∣U are the same vector spaces Ep for p∈U, and the smooth structure on E∣U is the one induced from the open subset π−1(U)⊆E.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

The zero section is a smooth embedding

Statement

For a smooth vector bundle π:E→M, the zero section 0M:M→E, p↦0p, is a smooth embedding.

Facts & Assumptions

Given: A smooth vector bundle π:E→M.

[L1]

In a vector bundle chart, the bundle is identified over the identity with U×Rr (Smooth vector bundles, rank, fibres, and trivial bundles).

[L2]

A smooth embedding is an injective immersion which is a homeomorphism onto its image with the subspace topology (Smooth embeddings).

Proof

technique · direct
1.1L1given

In a local trivialization Φ:π−1(U)→U×Rr, the zero section is represented by p↦(p,0). This map is smooth, injective, and its image is the slice U×{0}.

2.1L2step 1.1algebra∎

The coordinate slice U×{0} is an embedded submanifold of the product, so p↦(p,0) is an immersion and a homeomorphism onto its image. Transporting this property through the bundle charts proves that 0M is a smooth embedding by [L2].

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

The total space of a rank-r bundle has dimension dim M + r

Statement

If π:E→M is a smooth vector bundle of rank r and dim⁡M=n, then dim⁡E=n+r.

Facts & Assumptions

Given: A rank-r smooth vector bundle π:E→M with dim⁡M=n.

[L1]

Every point of E lies in a vector bundle chart identified with U×Rr over an open set U⊆M (Vector bundle charts and transition functions).

Proof

technique · direct
1.1L1given

Fix e∈E with base point p=π(e). Choose a chart of M sending a neighborhood of p diffeomorphically onto an open subset of Rn, and combine it with a vector bundle chart from [L1]. This identifies a neighborhood of e in E with an open subset of Rn×Rr.

2.1step 1.1algebra∎

Since Rn×Rr≅Rn+r, every point of E has a chart of dimension n+r. Therefore the total space E is an (n+r)-manifold.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Smooth sections, local sections, and support

Definition

Let π:E→M be a smooth vector bundle.

A smooth section of E is a smooth map s:M→E such that π∘s=id⁡M.

If U⊆M is open, a smooth local section on U is a smooth map s:U→E∣U with π∘s=id⁡U.

The support of a section s is the closure of the set {p∈M:s(p)≠0p}. A section is compactly supported when this set has compact closure.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Local and global frames of a vector bundle

Definition

Let π:E→M be a smooth rank-r vector bundle and let U⊆M be open.

A tuple of smooth local sections (s1,…,sr) on U is a local frame when, for every p∈U, the vectors s1(p),…,sr(p) form a basis of the fibre Ep.

When U=M, the same data are called a global frame.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Local frames and local trivializations are equivalent data

Statement

Let E→M be a rank-r smooth vector bundle and let U⊆M be open. A local frame (s1,…,sr) on U determines a vector bundle chart on U, and every vector bundle chart on U determines a local frame. These two constructions are inverse to one another.

Facts & Assumptions

Given: A rank-r vector bundle E→M and an open set U⊆M.

[L2]

Vector bundle chart changes are fibrewise linear (Vector bundle charts and transition functions).

Proof

technique · direct
1.1L1givenconstructalgebra

If (s1,…,sr) is a local frame on U, then [L1] gives for each p∈U and v∈Ep unique scalars a1,…,ar with v=∑iaisi(p). Around any p∈U, choose an existing vector bundle chart Ψ:E∣W→W×Rr with W⊆U. Writing Ψ(si(x))=(x,ai(x)), the column vectors ai(x) form a smooth matrix A(x)∈GL(r,R) because the si(x) are a basis of Ex. Thus the local coordinate map is ΦW(v)=(x,A(x)−1u) when Ψ(v)=(x,u), so ΦW and its inverse (x,λ)↦Ψ−1(x,A(x)λ) are smooth. By uniqueness of the coordinates from [L1], these local formulas agree on overlaps and patch to a vector bundle chart Φ:E∣U→U×Rr.

1.2L2givenconstruct

Conversely, if Φ:E∣U→U×Rr is a vector bundle chart, let e1,…,er be the standard basis of Rr and set si(p)=Φ−1(p,ei). Then each si is a smooth local section, and the vectors si(p) form a basis of Ep because Φ∣Ep is a linear isomorphism.

2.1step 1.1step 1.2algebra∎

Applying the second construction to the chart from step 1.1 recovers the original frame because Φ(si(p))=(p,ei) by construction. Applying the first construction to the sections from step 1.2 recovers the original chart because the resulting coordinates are exactly the fibre coordinates already read by Φ. Hence local frames and local trivializations are inverse constructions.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

A vector bundle is trivial if and only if it has a global frame

Statement

A smooth rank-r vector bundle is trivial if and only if it has a global frame.

Facts & Assumptions

Given: A smooth rank-r vector bundle E→M.

[L1]

Local frames and local trivializations are equivalent data on any open set (Local frames and local trivializations are equivalent data).

Proof

technique · direct
1.1L1given

If E is trivial, then the global bundle chart E≅M×Rr exists. Applying [L1] on U=M to that chart produces a global frame.

1.2L1given

If E has a global frame, then applying [L1] on U=M to that frame gives a global trivialization E≅M×Rr. Therefore E is trivial.

2.1step 1.1step 1.2∎

Steps 1.1 and 1.2 prove both directions of the biconditional.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Smoothness of a section is equivalent to smooth local components

Statement

Let E→M be a smooth vector bundle, let U⊆M be open, and let (s1,…,sr) be a local frame on U. A local section σ on U is smooth if and only if there are smooth functions f1,…,fr:U→R with

σ(p)=∑i=1rfi(p)si(p)(p∈U).

Facts & Assumptions

Given: A local frame (s1,…,sr) on U and a local section σ:U→E∣U.

[L1]

A local frame determines a local trivialization, and conversely (Local frames and local trivializations are equivalent data).

[L2]

Smoothness is local on the source (Smoothness is local on the source).

Proof

technique · direct
1.1L1given

By [L1], the chosen frame gives a bundle chart Φ:E∣U→U×Rr in which si(p) corresponds to the i-th standard basis vector. Therefore Φ(σ(p))=(p,f1(p),…,fr(p)) exactly when σ(p)=∑ifi(p)si(p).

2.1L2step 1.1algebra∎

In this chart, σ is smooth exactly when the coordinate map p↦(f1(p),…,fr(p)) is smooth. Equivalently, each component fi is smooth, and the criterion is local on U by [L2].

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Smooth sections form a module over smooth functions

Statement

If E→M is a smooth vector bundle, then the smooth sections of E form a module over C∞(M) under pointwise addition and scalar multiplication.

Facts & Assumptions

Given: A smooth vector bundle E→M.

[L1]

A section is smooth exactly when its local frame components are smooth (Smoothness of a section is equivalent to smooth local components).

Proof

technique · direct
1.1L1given

Let σ,τ be smooth sections and let f∈C∞(M). On a local frame, write σ=∑aisi and τ=∑bisi with smooth components ai,bi. Then σ+τ=∑(ai+bi)si and fσ=∑(fai)si.

2.1L1L2step 1.1∎

By [L2], the component functions ai+bi and fai are smooth, so [L1] shows that σ+τ and fσ are again smooth sections. The module axioms hold fibrewise because each fibre is a vector space.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Every vector in a fibre extends to a compactly supported smooth section

Statement

Let π:E→M be a smooth vector bundle, let p∈M, and let v∈Ep. Then there is a compactly supported smooth section σ of E with σ(p)=v.

Facts & Assumptions

Given: A smooth vector bundle E→M, a point p∈M, and a vector v∈Ep.

[L1]

Around p there is a local frame of E (Local and global frames of a vector bundle).

[L2]

There is a smooth bump function equal to 1 at p and supported in a prescribed chart neighborhood (A chart bump at a point with prescribed support).

[L3]

Multiplying a smooth section by a smooth function keeps it smooth (Smooth sections form a module over smooth functions).

[L4]

A section is smooth exactly when its local frame components are smooth (Smoothness of a section is equivalent to smooth local components).

Proof

technique · direct
1.1L1givenchoose

Choose a local frame (s1,…,sr) on an open set U containing p. Write v=∑iaisi(p) and define a local section τ=∑iaisi on U. Then τ(p)=v.

2.1L2L3L4step 1.1construct∎

Choose a smooth bump function χ:M→R with χ(p)=1 and supp⁡(χ)⊆U. On U define σ=χτ, which is smooth by [L3]. Because supp⁡(χ)⊆U, there is an open neighborhood V of M∖U on which χ=0; define σ=0 on V, which is smooth by [L4]. On U∩V the two formulas agree, so they paste to a smooth global section. Its support is contained in supp⁡(χ), hence compact, and σ(p)=χ(p)τ(p)=v.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Locally finite linear combinations of sections are smooth

Statement

Let (σi)i∈I be smooth sections of a vector bundle E→M and let (fi)i∈I be smooth real-valued functions on M. If the family of supports (supp⁡(fiσi))i∈I is locally finite, then the pointwise sum

∑i∈Ifiσi

defines a smooth section of E.

Facts & Assumptions

Given: Smooth sections σi, smooth functions fi, and a locally finite family of supports supp⁡(fiσi).

[L1]

A section is smooth exactly when its local frame components are smooth (Smoothness of a section is equivalent to smooth local components).

[L2]

A locally finite sum of smooth scalar functions is smooth (A locally finite sum of smooth functions is smooth).

Proof

technique · direct
1.1L1given

Fix a local frame (s1,…,sr) on an open set U. Write σi∣U=∑jaijsj with smooth coefficient functions aij. Then on U the formal sum has components ∑ifiaij. Because the supports of fiσi are locally finite, only finitely many terms are nonzero near each point.

2.1L1L2step 1.1∎

Each component ∑ifiaij is therefore a locally finite sum of smooth scalar functions, so it is smooth by [L2]. Applying [L1] again shows that ∑ifiσi is a smooth section on U, and hence on all of M.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Vector bundle maps over a smooth base map

Definition

Let πE:E→M and πF:F→N be smooth vector bundles, and let f:M→N be a smooth map.

A vector bundle map over f is a smooth map Φ:E→F such that πF∘Φ=f∘πE and, for every p∈M, the restriction Φ∣Ep:Ep→Ff(p) is linear.

When f=id⁡M, one also says that Φ is a bundle map over the identity.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Smoothness of a bundle map is equivalent to smooth local matrices

Statement

Let Φ:E→F be a fibrewise linear map over a smooth base map f:M→N. Choose local frames (e1,…,er) for E on U⊆M and (u1,…,us) for F on V⊆N with f(U)⊆V. Then Φ is smooth on E∣U if and only if there are smooth scalar functions aji:U→R such that

Φ(ei(p))=∑j=1saji(p)uj(f(p))

for every p∈U.

Facts & Assumptions

Given: A fibrewise linear map Φ:E→F over a smooth map f:M→N and local frames on U and V as above.

[L1]

Local frames are equivalent to local trivializations (Local frames and local trivializations are equivalent data).

[L2]

A section is smooth exactly when its local components are smooth (Smoothness of a section is equivalent to smooth local components).

Proof

technique · direct
1.1L1given

By [L1], the chosen frames identify E∣U with U×Rr and F∣V with V×Rs. In these trivializations, fibrewise linearity forces Φ to have the form Φ(p,v)=(f(p),A(p)v) for a unique matrix A(p)=(aji(p)).

2.1L2step 1.1algebra∎

The local representative (p,v)↦(f(p),A(p)v) is smooth exactly when its matrix entries aji are smooth on U. Equivalently, the images Φ(ei)=∑jajiuj∘f have smooth local components, which is the criterion in [L2].

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

A fibrewise bijective smooth bundle map over a diffeomorphism is a bundle isomorphism

Statement

Let Φ:E→F be a smooth vector bundle map over a diffeomorphism f:M→N. If each fibre map Φp:Ep→Ff(p) is bijective, then Φ is a vector bundle isomorphism.

Facts & Assumptions

Given: A smooth bundle map Φ:E→F over a diffeomorphism f:M→N, with each Φp bijective.

[L1]

In local frames, smooth bundle maps are given by smooth matrix-valued functions (Smoothness of a bundle map is equivalent to smooth local matrices).

[L2]

A real square matrix is invertible exactly when its determinant is nonzero (A finite square real matrix is invertible if and only if its determinant is nonzero).

[L3]

A smooth matrix-valued map has smooth inverse matrix entries wherever its determinant never vanishes (Matrix inversion preserves Ck regularity where the determinant is nonzero).

Proof

technique · direct
1.1L1L2given

If the common fibre rank is 0, then every fibre is the zero vector space, so Φ is already the unique smooth bundle map between zero bundles over f and hence a bundle isomorphism. Otherwise choose local frames so that on one trivializing neighborhood, Φ(p,v)=(f(p),A(p)v). Fibrewise bijectivity means that each matrix A(p) is invertible, so [L2] gives det⁡A(p)≠0 for every p.

2.1L3step 1.1algebra∎

In the positive-rank case, [L3] makes the entries of A−1 smooth on the same neighborhood. Thus the local inverse is (q,w)↦(f−1(q),A(f−1(q))−1w), which is smooth because f−1 is smooth. These local inverses agree on overlaps, so Φ is a smooth bundle isomorphism. Together with the rank-0 branch of step 1.1, this proves the proposition.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-31Open item page →

Vector subbundles

Definition

Let π:E→M be a smooth rank-r vector bundle, and let k∈N satisfy 0≤k≤r. A subset S⊆E is a smooth vector subbundle of rank k when:

  1. S∩Ep is a k-dimensional linear subspace of Ep for every p∈M, and
  2. every point of M has an open neighborhood U with a local frame (s1,…,sr) of E∣U such that (s1,…,sk) is a local frame of the fibrewise subsets S∩Ep: explicitly, S∩Ep=span⁡{s1(p),…,sk(p)} for every p∈U.

In particular, a vector subbundle has constant fibre dimension and is locally spanned by part of a frame of the ambient bundle.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Constant-rank kernels and images of bundle maps over one base are subbundles

Statement

Let Φ:E→F be a smooth vector bundle map over id⁡M, and assume that the fibre rank of Φp:Ep→Fp is the same integer k for every p∈M. Then ker⁡Φ is a smooth vector subbundle of E and im⁡Φ is a smooth vector subbundle of F.

Facts & Assumptions

Given: A smooth bundle map Φ:E→F over id⁡M with constant fibre rank k.

[L1]

In local frames, Φ is represented by a smooth matrix-valued function (Smoothness of a bundle map is equivalent to smooth local matrices).

[L2]

A smooth matrix-valued map has smooth inverse matrix entries wherever its determinant never vanishes (Matrix inversion preserves Ck regularity where the determinant is nonzero).

Proof

technique · direct
1.1L1given

If k=0, then every fibre map is zero, so ker⁡Φ=E and im⁡Φ is the zero subbundle of F. Assume now that k≥1, fix p∈M, and write Φ in local frames near p as a smooth matrix A(x). Because rank⁡A(p)=k, after reordering coordinates some k×k minor B(x) is nonzero at p, hence nonzero on a smaller neighborhood.

2.1L2step 1.1algebra

Writing source coordinates as (u,w) for that split, the kernel equation becomes B(x)u+C(x)w=0, so [L2] makes B(x)−1 smooth and gives u=−B(x)−1C(x)w. Therefore the kernel fibres are spanned by smooth local sections depending on the free variables w.

3.1L1step 1.1step 2.1algebra∎

The same chosen k columns of A(x) remain linearly independent nearby, so they form a smooth local frame of the image bundle. Thus in the positive-rank case both the kernel and the image are locally spanned by part of a frame, and step 1.1 already handled k=0. Therefore ker⁡Φ and im⁡Φ are smooth vector subbundles.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Pullback vector bundles as fibre products

Definition

Let π:E→M be a smooth vector bundle and let f:N→M be a smooth map. The pullback set of E along f is

f∗E:={(q,e)∈N×E:f(q)=π(e)}.

Its projection to N is (q,e)↦q, and its fibre over q∈N is canonically identified with Ef(q). The following theorem shows that this set carries a natural smooth vector-bundle structure.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

The pullback fibre product is a smooth vector bundle

Statement

If π:E→M is a smooth rank-r vector bundle and f:N→M is smooth, then the fibre product f∗E is a smooth rank-r vector bundle over N.

Facts & Assumptions

Given: A smooth rank-r vector bundle π:E→M and a smooth map f:N→M.

[L1]

A vector bundle chart on E over U⊆M is a diffeomorphism E∣U≅U×Rr with transition functions of the form (p,v)↦(p,gβα(p)v) (Vector bundle charts and transition functions).

[L2]

The restriction E∣U is the same total space over the smaller open base (Restrictions of vector bundles).

[L3]

Products of smooth manifolds have the product topology and smooth structure (Products of smooth manifolds have a canonical product smooth structure). Hausdorffness and second countability pass to subspaces (T0, T1, and Hausdorffness are hereditary, Second countability is hereditary).

[L4]

A smooth fibre bundle has a smooth manifold total space, a smooth surjective projection, and smooth local trivializations (Smooth fibre bundles and local trivializations).

Proof

technique · direct
1.1L1L2L3givenconstruct

Give f∗E={(q,e)∈N×E:f(q)=π(e)} the subspace topology from the product manifold N×E of [L3]. It is Hausdorff and second countable by [L3]. For a bundle chart Φα:E∣Uα→Uα×Rr, put Vα=f−1(Uα), an open subset of N. The pullback over Vα is open in f∗E because it is the intersection with Vα×E.

2.1L1L2L3step 1.1

For (q,e) over Vα, define Φ~α(q,e)=(q,v) when Φα(e)=(f(q),v). Its inverse is explicitly (q,v)↦(q,Φα−1(f(q),v)). The forward map is continuous as the restriction of the product of the identity on N with pr⁡2∘Φα; the inverse is continuous because q↦f(q) and Φα−1 are continuous. Thus Φ~α is a homeomorphism onto the open product manifold Vα×Rr. These homeomorphisms cover f∗E.

3.1L1L3L4step 1.1step 2.1∎

On overlaps, Φ~β∘Φ~α−1(q,v)=(q,gβα(f(q))v). This is smooth because gβα and f are smooth, and it is linear in each fibre coordinate. Combine the homeomorphisms of step 2.1 with product charts on Vα×Rr; their smooth overlap maps give a smooth atlas on the already Hausdorff second-countable space f∗E. In these charts the projection (q,e)↦q is the first projection, hence smooth and surjective, and each fibre is linearly identified with Ef(q)≅Rr. Consequently [L4] gives a smooth rank-r vector bundle over N. Empty bases and rank zero obey the same construction.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Pullback is functorial up to canonical bundle isomorphism

Statement

For a smooth vector bundle π:E→M, there are canonical bundle isomorphisms

id⁡M∗E≅E,(f∘g)∗E≅g∗(f∗E).

Facts & Assumptions

Given: A smooth vector bundle E→M and smooth maps g:P→N and f:N→M.

[L1]

The pullback bundle is the fibre-product set with its smooth bundle structure (Pullback vector bundles as fibre products, The pullback fibre product is a smooth vector bundle).

Proof

technique · direct
1.1L1givenconstruct

For the identity map, define I:id⁡M∗E→E by I(p,e)=e. This is well defined because p=π(e) in the identity pullback, and its inverse is e↦(π(e),e).

2.1L1step 1.1algebra∎

An element of g∗(f∗E) is a pair (x,(g(x),e)) with f(g(x))=π(e). Send it to (x,e)∈(f∘g)∗E. The inverse is (x,e)↦(x,(g(x),e)). In the pulled-back bundle charts of [L1], both maps are the identity on the fibre coordinate, so they are smooth vector bundle isomorphisms.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Whitney sums of vector bundles

Definition

Let E→M and F→M be smooth vector bundles over the same base. Their Whitney sum is the disjoint union

E⊕F:=∐p∈M(Ep⊕Fp),

with projection sending (p,v,w) to p. Fibrewise, the vector space over p is the direct sum of Ep and Fp.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Whitney sums are smooth vector bundles

Statement

If E→M and F→M are smooth vector bundles of ranks r and s, then E⊕F→M is a smooth vector bundle of rank r+s.

Facts & Assumptions

Given: Smooth vector bundles E→M and F→M.

[L1]

On a common trivializing neighborhood, vector bundle charts identify E and F with U×Rr and U×Rs (Vector bundle charts and transition functions).

Proof

technique · direct
1.1L1givenconstruct

On a common trivializing neighborhood U, use [L1] to identify E∣U⊕F∣U with U×(Rr⊕Rs)≅U×Rr+s. This gives a local trivialization of the Whitney sum.

2.1L1step 1.1algebra∎

If the transition matrices for E and F are gβα and hβα, then the transition matrix for E⊕F is the block diagonal matrix diag⁡(gβα,hβα), which is smooth on overlaps. Therefore these local trivializations define a smooth rank-(r+s) bundle.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Dual and Hom vector bundles

Definition

Let E→M and F→M be smooth vector bundles over the same base.

The dual bundle E∗→M has fibre Ep∗ over p∈M.

The Hom bundle Hom⁡(E,F)→M has fibre Hom⁡(Ep,Fp) over p∈M.

The next theorem equips these fibrewise constructions with smooth vector-bundle structures.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

Dual and Hom transition functions define smooth bundles

Statement

If E→M and F→M are smooth vector bundles, then E∗→M and Hom⁡(E,F)→M are smooth vector bundles. In local bundle charts, the dual transition matrices are (gβα−1)T and the Hom transition matrices are A↦hβαAgβα−1.

Facts & Assumptions

Proof

technique · direct
1.1givenL3construct

Put A=E and B=F, of ranks r,s. For r,s>0, let D⊆Ar×Br consist of tuples (a1,…,ar,b1,…,br) over a common base point p, with (ai) a basis of Ap. Give D the finite-product subspace topology. It is second countable: choose one countable base of each supplied total space, take finite product boxes, and restrict them to D. Only finitely many bases are chosen, and [L3] makes the resulting family countable.

2.1step 1.1L4L5construct

Let H=∐p∈MHom⁡(Ap,Bp) as a set. Send a tuple in D to the unique fibre map taking ai to bi. This map q:D→H is onto: a basis can be chosen for each one fibre without selecting bases for all fibres simultaneously. Give H the quotient topology. On a common local trivialization over U, the open saturated set DU has coordinates (p,C,V)∈U×GL(r,R)×Ms×r(R), and the composite of q with the proposed Hom matrix chart is (p,C,V)↦(p,VC−1). This is a continuous open surjection: (p,C,V)↦(p,C,VC−1) is a homeomorphism by [L5], followed by the open product projection. By [L4], the induced chart HU→U×Ms×r(R) is a homeomorphism and HU is open.

3.1step 1.1step 2.1L3

The map q is globally open because its restriction over every such open HU is open. Images of a countable base of D then form a countable base of H: for each h∈W open, choose one d∈q−1(h) and a basic neighbourhood C with d∈C⊆q−1(W), so h∈q(C)⊆W. Distinct maps over distinct base points separate by base neighbourhoods; distinct maps over one point separate in one Hausdorff matrix chart. Thus H is Hausdorff and second countable.

4.1step 2.1step 3.1L1L5algebra

If the original bundle frames change by gβα and hβα, a Hom matrix T changes to hβαTgβα−1. These maps and their inverses are smooth by [L1] and [L5], so the charts in step 2.1 give H a smooth vector-bundle atlas; a boundary base chart yields the corresponding half-space product chart. Fibre addition and scalar multiplication are linear in these coordinates. If r=0 or s=0, H is the zero bundle M; if M is empty, it is empty.

5.1step 4.1L2algebra∎

Take B=M×R in steps 1.1–4.1 to obtain E∗=Hom⁡(E,M×R) as a smooth bundle. A functional with row coordinates ℓ changes to ℓgβα−1; by [L2], its column transition matrix is (gβα−1)T. Step 4.1 gives the stated Hom transition matrix.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-09-24 (gpt-6-sol)Open item page →

Sections of Hom are the same as smooth fibrewise linear maps

Statement

For smooth vector bundles E,F→M, smooth sections of Hom⁡(E,F) are in natural bijection with smooth vector bundle maps E→F over id⁡M.

Facts & Assumptions

Given: Smooth vector bundles E,F→M.

[L1]

In local frames, a smooth bundle map over the identity is equivalent to a smooth matrix of coefficients (Smoothness of a bundle map is equivalent to smooth local matrices).

[L2]

The Hom bundle is built from the same local matrices (Dual and Hom transition functions define smooth bundles).

Proof

technique · direct
1.1L1L2givenconstruct

A section s:M→Hom⁡(E,F) assigns to each p∈M a linear map s(p):Ep→Fp. Define Φs:E→F by Φs(v)=s(π(v))(v). In a pair of local frames, the matrix entries of s are exactly the matrix entries of Φs.

2.1L1L2step 1.1algebra∎

Conversely, a bundle map Φ:E→F over id⁡M gives a section sΦ(p)=Φ∣Ep∈Hom⁡(Ep,Fp). The constructions are inverse to one another, and [L1] together with [L2] shows that smoothness on either side is the same local matrix condition.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Bundle maps over f are sections of the pulled-back Hom bundle

Statement

Let Φ:E→F be a smooth vector bundle map over a smooth map f:M→N. Then Φ is naturally equivalent to a smooth section of the pulled-back Hom bundle Hom⁡(E,f∗F)→M.

Facts & Assumptions

Given: Smooth vector bundles E→M, F→N, a smooth map f:M→N, and a bundle map Φ:E→F over f.

[L1]

The pullback fibre product f∗F is a smooth vector bundle over M (The pullback fibre product is a smooth vector bundle).

[L2]

Sections of a Hom bundle are the same as fibrewise linear bundle maps over the identity (Sections of Hom are the same as smooth fibrewise linear maps).

Proof

technique · direct
1.1L1givenconstruct

For each p∈M, the fibre map Φp:Ep→Ff(p) may be viewed as a linear map Ep→(f∗F)p because (f∗F)p is canonically Ff(p). Hence p↦Φp defines a section of Hom⁡(E,f∗F)→M.

2.1L1L2step 1.1algebra∎

In local trivializations the matrix of this section is exactly the local matrix of Φ, so the section is smooth exactly when Φ is smooth. Therefore [L2] applied to the bundles E and f∗F yields the required bijection.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Quotient vector bundles by a subbundle

Definition

Let S⊆E be a smooth vector subbundle of a smooth vector bundle E→M. The quotient bundle set E/S→M has fibre

(E/S)p:=Ep/Sp

over each p∈M.

Its total space is the disjoint union of these fibrewise quotients. The next theorem shows that this fibrewise construction carries a natural smooth vector-bundle structure.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

A vector bundle quotient by a subbundle is a smooth vector bundle

Statement

If S⊆E is a smooth rank-k subbundle of a smooth rank-r vector bundle E→M, then the fibrewise quotient E/S→M is a smooth rank-(r−k) vector bundle.

Facts & Assumptions

Given: A smooth vector bundle E→M and a smooth rank-k subbundle S⊆E.

[L1]

Locally, a subbundle is spanned by part of a frame of the ambient bundle (Vector subbundles).

Proof

technique · direct
1.1L1givenchoose

Around each point of M, choose a local frame (e1,…,er) of E such that (e1,…,ek) is a local frame of S. Then the quotient classes of ek+1,…,er form a basis of each quotient fibre Ep/Sp.

2.1step 1.1algebra∎

Using the basis from step 1.1, identify the quotient fibre over p with Rr−k by reading the coefficients of the classes of ek+1,…,er. If one changes to another adapted frame, the change-of-frame matrix has block upper-triangular form [AB0C], so the quotient coordinates transform by C. Hence the quotient charts are smoothly compatible and define a smooth rank-(r−k) vector bundle.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The canonical map to a quotient bundle is a smooth bundle map

Statement

If S⊆E is a smooth vector subbundle, then the fibrewise quotient map q:E→E/S is a smooth vector bundle map over id⁡M, and its kernel is S.

Facts & Assumptions

Given: A smooth vector bundle E→M and a smooth subbundle S⊆E.

[L1]

The quotient E/S→M is a smooth vector bundle (A vector bundle quotient by a subbundle is a smooth vector bundle).

Proof

technique · direct
1.1L1given

In an adapted local frame (e1,…,er) with S spanned by the first k vectors, the quotient bundle chart from [L1] identifies q with the map (p,u,w)↦(p,w), where u∈Rk and w∈Rr−k. Thus q is smooth and fibrewise linear.

2.1step 1.1algebra∎

In the same coordinates, q(p,u,w)=0 exactly when w=0, which means that the vector lies in the span of e1,…,ek, namely in Sp. Therefore ker⁡q=S.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Smooth bundle metrics

Definition

Let E→M be a smooth vector bundle. A smooth bundle metric on E is a choice of inner product ⟨⋅,⋅⟩p on each fibre Ep such that, for every pair of smooth local sections s,t, the function

p↦⟨s(p),t(p)⟩p

is smooth on the common domain of s and t.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

Every smooth vector bundle admits a smooth bundle metric

Statement

Assume the Axiom of Countable Choice. Every smooth vector bundle admits a smooth bundle metric.

Facts & Assumptions

Given: The Axiom of Countable Choice and a smooth vector bundle E→M.

[L1]

Under Countable Choice, the base manifold admits smooth partitions of unity subordinate to indexed open covers (Smooth partitions of unity exist on manifolds, The Axiom of Countable Choice (ACω)).

[L2]

Local frames are equivalent to local trivializations (Local frames and local trivializations are equivalent data).

Proof

technique · direct
1.1L2givenconstruct

Index an open cover by all pairs (Uα,τα) supplied by the bundle's local trivializations, so each cover member comes with its trivialization and no separate family of frame choices is needed. Pull back the Euclidean inner product on Rr through τα to obtain a smooth local bundle metric hα on E∣Uα.

2.1L1step 1.1constructalgebra∎

Under the stated Countable Choice, [L1] gives a smooth partition of unity (ρα) indexed by these same trivialization pairs, with supp⁡ρα⊆Uα. Define ραhα on Uα and extend it by zero outside Uα; this is smooth because every point outside the closed support of ρα has a neighbourhood where the term vanishes. The sum h:=∑αραhα is locally finite and smooth. At each point p, some ρα(p)>0, all weights are nonnegative, and ∑αρα(p)=1, so hp is positive definite. Thus h is a smooth bundle metric.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Orthogonal complements of subbundles are smooth subbundles

Statement

Let S⊆E be a smooth vector subbundle of a smooth vector bundle E→M equipped with a smooth bundle metric. Then the orthogonal complements

Sp⊥:={v∈Ep:⟨v,w⟩p=0 for every w∈Sp}

form a smooth vector subbundle S⊥⊆E.

Facts & Assumptions

Given: A smooth vector bundle E→M, a smooth subbundle S⊆E, and a smooth bundle metric on E.

[L1]

Locally, S is spanned by part of a frame of E (Vector subbundles).

[L2]

Proof

technique · direct
1.1L1L2givenchoose

Around each point, choose a local frame (e1,…,er) of E such that (e1,…,ek) spans S. Apply smooth Gram-Schmidt from [L2] to obtain a local orthonormal frame (u1,…,ur). Because the first k input vectors already lie in S, the first k orthonormalized vectors still span S.

2.1step 1.1algebra∎

For each fibre, the orthogonal complement of Sp is then spanned by uk+1(p),…,ur(p). These vectors vary smoothly, so they give a local frame of S⊥. Hence S⊥ is a smooth vector subbundle of E.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

Every vector subbundle has a smooth complement

Statement

Assume the Axiom of Countable Choice. Every smooth vector subbundle S⊆E has a smooth complement in E.

Facts & Assumptions

Given: The Axiom of Countable Choice and a smooth vector subbundle S⊆E.

[L1]

Under Countable Choice, the bundle E admits a smooth bundle metric (Every smooth vector bundle admits a smooth bundle metric, The Axiom of Countable Choice (ACω)).

[L2]

Orthogonal complements of subbundles are smooth subbundles (Orthogonal complements of subbundles are smooth subbundles).

Proof

technique · direct
1.1L1givenchoose

Choose a smooth bundle metric on E by [L1].

2.1L2step 1.1algebra∎

With that metric, [L2] gives a smooth subbundle S⊥⊆E, and fibrewise one has Ep=Sp⊕Sp⊥. Thus S⊥ is a smooth complement of S.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

Every short exact sequence of smooth vector bundles splits

Statement

Assume the Axiom of Countable Choice. Every short exact sequence of smooth vector bundles over one base,

0→E→iG→qF→0,

admits a smooth splitting s:F→G with q∘s=id⁡F.

Facts & Assumptions

Given: The Axiom of Countable Choice and a short exact sequence of smooth vector bundles over one base M.

[L1]

Constant-rank kernels and images of bundle maps over one base are smooth subbundles (Constant-rank kernels and images of bundle maps over one base are subbundles).

[L2]

Under Countable Choice, every vector subbundle has a smooth complement (Every vector subbundle has a smooth complement, The Axiom of Countable Choice (ACω)).

[L3]

A fibrewise bijective smooth bundle map over the identity is a bundle isomorphism (A fibrewise bijective smooth bundle map over a diffeomorphism is a bundle isomorphism).

Proof

technique · direct
1.1L1L2givenchoose

Exactness gives i(E)=ker⁡q⊆G. By [L1], this image is a smooth subbundle of G. Choose a smooth complement H⊆G to i(E) by [L2], so Gp=i(Ep)⊕Hp for every p∈M.

2.1L3step 1.1algebra∎

Because ker⁡(q∣Hp)=Hp∩i(Ep)=0 and qp is surjective, q∣H:H→F is fibrewise bijective. By [L3] it is a smooth bundle isomorphism, so its inverse s:F→H⊆G is smooth and satisfies q∘s=id⁡F. Thus the sequence splits.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-31Open item page →

Normal and conormal bundles of an embedded submanifold

Definition

Let S⊆M be an embedded submanifold.

Equip S with the smooth structure supplied by Slice-chart restrictions form a smooth atlas. The inclusion i:S↪M is then a smooth embedding by The inclusion of an embedded submanifold is a smooth embedding, so its differential is defined. Identify TpS with the linear subspace dip(TpS)⊆TpM. Here the notation TM∣S:=∐p∈STpM,T∗M∣S:=∐p∈STp∗M means the fibrewise restriction of these disjoint unions to base points in S; it does not invoke restriction to an open subset.

The normal-bundle set of S in M is the fibrewise quotient

ν(S):=∐p∈STpM/TpS.

The conormal-bundle set of S in M is the fibrewise annihilator

N∗S:={ξ∈T∗M∣S:ξ∣TpS=0 for the base point p}.

Both are intrinsic constructions attached to the embedding S↪M. The next proposition supplies their smooth vector-bundle structures.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Assuming countable choice, normal and conormal bundles are smooth vector bundles

Statement

Assume ACω. If S⊆M is an embedded submanifold, then the normal bundle ν(S)=TM∣S/TS and the conormal bundle N∗S⊆T∗M∣S are smooth vector bundles over S.

Facts & Assumptions

Given: The axiom ACω and an embedded submanifold S⊆M.

[L0]
[L1]

Around each point of S there is a slice chart in which S is given by y1=⋯=yc=0 (Embedded submanifolds and slice charts).

[L2]

A quotient by a smooth vector subbundle is a smooth vector bundle (A vector bundle quotient by a subbundle is a smooth vector bundle).

Proof

technique · direct
1.1L0L1L2given

In a slice chart (x1,…,xk,y1,…,yc) with S={y=0}, the induced charts of [L0] make TM∣S a smooth vector bundle with local frame ∂x1,…,∂xk,∂y1,…,∂yc, while TS is spanned by the ∂xi. Hence TS is a smooth subbundle and the classes of ∂yj give a local frame of the quotient TM∣S/TS. By [L2], the normal bundle is smooth.

2.1L0L1step 1.1algebra∎

In the same slice chart, the induced cotangent charts of [L0] give the local coframe dx1,…,dxk,dy1,…,dyc, and the covectors annihilating TS are exactly the span of dy1,…,dyc. These local frames vary smoothly, so the conormal bundle is a smooth subbundle of T∗M∣S, hence a smooth vector bundle over S.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Assuming countable choice, an ambient metric identifies the two normal bundles

Statement

Assume ACω. Let S⊆M be an embedded submanifold and let g be a Riemannian metric on M. If q:TM∣S→ν(S)=TM∣S/TS is the quotient map, then

q∣TS⊥:TS⊥⟶ν(S)

is a smooth vector-bundle isomorphism. Thus the fixed metric g canonically identifies the quotient normal bundle with its g-orthogonal realization.

Facts & Assumptions

Given: The axiom ACω, an embedded submanifold S⊆M, and an ambient Riemannian metric g on M.

[L0]

Under ACω, TM has a smooth manifold structure for which the induced tangent-bundle charts form a smooth atlas (Assuming countable choice, the tangent bundle has a canonical smooth 2n-manifold structure).

[L4]

An induced tangent-bundle chart sends v=∑ivi∂xi∣p to (x(p),(v1,…,vn)) (The induced tangent bundle chart).

[L5]

A smooth vector bundle is locally trivialized by fibrewise linear charts (Smooth vector bundles, rank, fibres, and trivial bundles).

[L6]

The inclusion i:S↪M is smooth (The inclusion of an embedded submanifold is a smooth embedding).

[L7]

Pullback along a smooth map carries a smooth vector bundle to a smooth vector bundle (The pullback fibre product is a smooth vector bundle).

[L8]

In a slice chart, S is a coordinate slice (Embedded submanifolds and slice charts).

[L9]

A smooth subbundle is locally spanned by part of a smooth ambient frame (Vector subbundles).

[F0]

A smooth bundle metric is a fibrewise inner product whose pairing of any two smooth local sections is smooth (Smooth bundle metrics).

[L1]

The orthogonal complement of a smooth subbundle is a smooth subbundle (Orthogonal complements of subbundles are smooth subbundles).

[L2]

The quotient map TM∣S→ν(S) is a smooth bundle map (The canonical map to a quotient bundle is a smooth bundle map).

[L3]

A fibrewise bijective smooth bundle map over the identity is a bundle isomorphism (A fibrewise bijective smooth bundle map over a diffeomorphism is a bundle isomorphism).

Proof

technique · direct
1.1F0L0L1L4L5L6L7L8L9given

By [L0], [L4], and [L5], the induced charts make TM→M a smooth vector bundle. By [L6] and [L7], its pullback along i is the smooth vector bundle TM∣S→S. In a slice chart from [L8], its coordinate frame is ∂x1,…,∂xk,∂y1,…,∂yc and TS is spanned by the first k vectors, so [L9] makes TS a smooth subbundle. In that pulled-back frame, the coefficients of g∣S are the smooth coefficient functions of g composed with the smooth inclusion i; hence [F0] makes g∣S a smooth bundle metric on TM∣S. Applying [L1], the orthogonal complements TSp⊥ form a smooth subbundle and fibrewise TpM=TpS⊕TpS⊥.

2.1L2L3step 1.1algebra∎

Restrict the quotient map of [L2] to TS⊥. On each fibre this is the usual linear isomorphism from a chosen complement onto the quotient by TpS. Hence the restricted map TS⊥→ν(S) is fibrewise bijective, so [L3] shows that it is a smooth bundle isomorphism.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Assuming countable choice, every smooth manifold admits a Riemannian metric

Statement

Assume ACω. Every smooth manifold admits a Riemannian metric.

Facts & Assumptions

Given: The axiom ACω and a smooth manifold M.

[L1]

The tangent bundle TM→M is a smooth vector bundle (Assuming countable choice, the tangent bundle has a canonical smooth 2n-manifold structure).

[L2]

Every smooth vector bundle admits a smooth bundle metric (Every smooth vector bundle admits a smooth bundle metric).

Proof

technique · direct
1.1L1given

By [L1], the tangent bundle of M is a smooth vector bundle.

2.1L2step 1.1∎

Apply [L2] to TM. A smooth bundle metric on TM is exactly a Riemannian metric on M.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

A vector bundle section with surjective vertical differential at every zero has a submanifold zero set

Statement

Let π:E→M be a smooth rank-r vector bundle and let s:M→E be a smooth section. For a zero p of s, define the vertical differential Dvsp:TpM→Ep as the induced map from dsp:TpM→T0pE after quotienting by the tangent space to the zero section. If Dvsp is surjective at every zero of s, then the zero set Z(s)={p∈M:s(p)=0p} is an embedded submanifold of codimension r.

Facts & Assumptions

Given: A smooth section s:M→E of a smooth rank-r vector bundle.

[L1]

In a local frame, smoothness of a section is equivalent to smoothness of its component map to Rr (Smoothness of a section is equivalent to smooth local components).

[L2]

A regular level set is an embedded submanifold (A regular level set is an embedded submanifold).

Proof

technique · direct
1.1L1given

Let p∈Z(s) and choose a local frame near p. Then s(x)=∑ifi(x)ei(x) for a smooth map f=(f1,…,fr):U→Rr. Because s(p)=0p, one has f(p)=0. Under a change of frame by a matrix A(x), the new component map is A(x)f(x), whose derivative at p is A(p)dfp because the term (dA)pf(p) vanishes. Thus surjectivity of the vertical differential is exactly surjectivity of dfp, independent of the chosen frame.

2.1L2step 1.1algebra∎

Near p, the zero set of s is therefore the zero set of the component map f, and 0∈Rr is a regular value because dfp is surjective. By [L2], f−1(0) is an embedded submanifold of codimension r. Doing this at every zero proves that Z(s) is an embedded submanifold of codimension r.

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Every vector bundle is globally trivial

Statement

Every smooth vector bundle is globally trivial.

Facts & Assumptions

Given: The displayed universal triviality claim.

[L1]

A smooth cocycle defines a smooth vector bundle (Construction of a vector bundle from a smooth cocycle).

[L2]

A smooth vector bundle is trivial if and only if it has a global frame (A vector bundle is trivial if and only if it has a global frame).

Refutation

technique · direct
1.1L1givenconstruct

Cover S1 by the two standard arcs U0=S1∖{(−1,0)} and U1=S1∖{(1,0)}. Their overlap has an upper and a lower component. Define a rank-one cocycle by g10=1 on the upper overlap and g10=−1 on the lower overlap. By [L1], this glues a smooth line bundle L→S1.

2.1L2step 1.1contradiction∎

If L were trivial, then [L2] would give a nowhere-zero global frame. In local trivializations that would be given by nowhere-zero functions f0 on U0 and f1 on U1 with f1=f0 on the upper overlap and f1=−f0 on the lower overlap. Since U1 is connected, a nowhere-zero continuous f1 has constant sign, but the two overlap equations force opposite signs. This contradiction shows that L is not trivial.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

A continuous fibrewise linear map over a smooth base map is automatically smooth

Statement

A continuous fibrewise linear map over a smooth base map is automatically smooth.

Facts & Assumptions

Given: The displayed claim.

[L1]

Smoothness of a bundle map is equivalent to smoothness of its local matrix coefficients (Smoothness of a bundle map is equivalent to smooth local matrices).

Refutation

technique · direct
1.1L1givenconstruct

On the trivial line bundle R×R→R, define Φ(x,v)=(x,∣x∣v). This map is continuous, covers the smooth base map id⁡R, and is linear on every fibre.

2.1L1step 1.1∎

Its local matrix coefficient is the scalar function ∣x∣, which is not smooth at 0. Therefore [L1] implies that Φ is not smooth. So the displayed statement is false.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The fibrewise quotient of a vector bundle by arbitrary varying subspaces is a vector bundle

Statement

The fibrewise quotient of a vector bundle by arbitrary varying subspaces is always a smooth vector bundle.

Facts & Assumptions

Given: The displayed claim.

[L1]

A quotient bundle theorem requires a smooth vector subbundle, in particular constant fibre dimension and smooth local frames (A vector bundle quotient by a subbundle is a smooth vector bundle, Vector subbundles).

Refutation

technique · direct
1.1L1givenconstruct

In the trivial line bundle R×R→R, let Sx={0} for x≠0 and let S0=R. Then the quotient fibre is one-dimensional for x≠0 and zero-dimensional at x=0.

2.1L1step 1.1algebra∎

A smooth vector bundle has locally constant fibre dimension, so this family of quotients cannot be a vector bundle. The missing hypothesis is exactly that the subspaces form a smooth subbundle as in [L1].

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

A short exact sequence of vector bundles has a canonical splitting

Statement

Every short exact sequence of smooth vector bundles has a canonical splitting.

Facts & Assumptions

Given: The displayed claim.

The explicit sequence below has splittings, but none is invariant under all of its automorphisms.

Refutation

technique · direct
1.1givenconstruct

Consider the split exact sequence of trivial line bundles over any nonempty manifold M, 0→M×R→M×R2→M×R→0, where the first map is t↦(t,0) and the second is projection to the second coordinate. The map s0(p,u)=(p,(0,u)) is an explicit smooth splitting.

2.1step 1.1algebra∎

For every c∈R, the bundle automorphism Tc(p,(x,y))=(p,(x+cy,y)) fixes the included first summand and commutes with projection to the second summand, so it is an automorphism of the exact sequence in step 1.1. Every splitting has the form sa(p,u)=(p,(a(p)u,u)) for a smooth function a, while Tc∘sa=sa+c. Thus no splitting is fixed by all automorphisms of the sequence: taking c=1 moves every candidate. A splitting determined canonically by the sequence would have to be invariant under these automorphisms, so none exists.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The orthogonal normal bundle of a submanifold is defined without a metric

Statement

The orthogonal normal bundle of an embedded submanifold is defined without a metric.

Facts & Assumptions

Given: The displayed claim.

[L1]

The quotient normal bundle is intrinsic, but the orthogonal normal bundle is obtained only after choosing an ambient metric (Normal and conormal bundles of an embedded submanifold, Assuming countable choice, an ambient metric identifies the two normal bundles).

Refutation

technique · direct
1.1L1given

Let S=R×{0}⊆R2. For the Euclidean metric, the orthogonal complement of TS is spanned by ∂y.

2.1L1step 1.1algebra∎

For the metric g=dx2+2dx dy+2dy2, a vector a∂x+b∂y is orthogonal to ∂x exactly when a+b=0, so the orthogonal complement is spanned by ∂y−∂x. The orthogonal normal line therefore depends on the chosen metric, and only the quotient normal bundle is intrinsic.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The pullback bundle is the set-theoretic inverse image of the total space

Statement

The pullback bundle is the set-theoretic inverse image of the original total space.

Facts & Assumptions

Given: The displayed claim.

[L1]

The pullback bundle consists of pairs (q,e) with f(q)=π(e) (Pullback vector bundles as fibre products).

Refutation

technique · direct
1.1L1givenconstruct

Let f:R→{0}⊆R be the constant map and let E=R×R→R be the trivial line bundle. Then f∗E={(q,(0,v)):q∈R, v∈R}, which is naturally R×R.

2.1L1step 1.1algebra∎

Different base points q1≠q2 with the same fibre element v give distinct pullback points (q1,(0,v))≠(q2,(0,v)). Thus the pullback keeps new base information and is not a subset of the old total space. It is a fibre product, not a set-theoretic inverse image.

Sources