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.
A vector bundle quotient by a subbundle is a smooth vector bundle
Statement
If is a smooth rank- subbundle of a smooth rank- vector bundle , then the fibrewise quotient is a smooth rank- vector bundle.
Facts & Assumptions
Given: A smooth vector bundle and a smooth rank- subbundle .
Locally, a subbundle is spanned by part of a frame of the ambient bundle (Vector subbundles).
Proof
Around each point of , choose a local frame of such that is a local frame of . Then the quotient classes of form a basis of each quotient fibre .
Using the basis from step 1.1, identify the quotient fibre over with by reading the coefficients of the classes of . If one changes to another adapted frame, the change-of-frame matrix has block upper-triangular form , so the quotient coordinates transform by . Hence the quotient charts are smoothly compatible and define a smooth rank- vector bundle.
Depends on
Used by
- Normal bundle of a formal immersion Definition
- The Bott partial connection on the normal bundle of a foliation Definition
- The fibrewise quotient of a vector bundle by arbitrary varying subspaces is a vector bundle False statement
- Formal immersion gives the tangent normal-bundle identity Lemma
- Normal bundle of the zero locus of a transverse section Lemma
- Stiefel-Whitney classes of the tangent bundle of real projective space Lemma
- The normal bundle of the diagonal is canonically the tangent bundle Lemma
- Assuming countable choice, normal and conormal bundles are smooth vector bundles Proposition
- The canonical map to a quotient bundle is a smooth bundle map Proposition
- The Euler class of an oriented even-rank normal bundle controls self-intersection Proposition
- The pullback foliation under a transverse map Proposition
Dependency tree · two levels
10 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)