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 zero section is a smooth embedding
Statement
For a smooth vector bundle , the zero section , , is a smooth embedding.
Facts & Assumptions
Given: A smooth vector bundle .
In a vector bundle chart, the bundle is identified over the identity with (Smooth vector bundles, rank, fibres, and trivial bundles).
A smooth embedding is an injective immersion which is a homeomorphism onto its image with the subspace topology (Smooth embeddings).
Proof
In a local trivialization , the zero section is represented by . This map is smooth, injective, and its image is the slice .
The coordinate slice is an embedded submanifold of the product, so is an immersion and a homeomorphism onto its image. Transporting this property through the bundle charts proves that is a smooth embedding by [L2].
Depends on
Used by
- A smooth section transverse to the zero section has a submanifold zero set Corollary
- Nondegenerate zero of a vector field Definition
- Smooth sections, local sections, and support Definition
- The self-intersection number of a complementary-dimensional oriented submanifold Definition
- Self-intersection of the zero section in an oriented plane bundle Example
- A smooth function is Morse if and only if its differential section is transverse to the zero section Lemma
- Normal bundle of the zero locus of a transverse section Lemma
- A vector bundle section with surjective vertical differential at every zero has a submanifold zero set Proposition
- The index of a zero is its zero-section intersection number Proposition
- Every smooth function admits arbitrarily fine strong-topology perturbations whose differential is transverse to zero, supported away from a closed set where transversality already holds Theorem
- For a compact manifold embedded in Euclidean space, the restricted linear height is Morse for generic directions Theorem
Dependency tree · two levels
15 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 (standard reference, not scraped)
- Will J. Merry, Differential Geometry (standard reference, not scraped)