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.
Associated bundles
Definition
Let be a smooth right principal -bundle, meaning that the topological principal charts of Principal g bundle and associated fiber bundle are diffeomorphisms, and let be a smooth finite-dimensional real representation. Define a right action on by
The vector bundle associated to and is the quotient set with quotient topology
Write for the orbit of . Equivalently, the generating relation is
The projection is
It is well defined because and continuous by the quotient universal property For a quotient map , a map out of is continuous iff its composite with is; a continuous map on constant on the fibres of factors uniquely through ; and a composite of quotient maps is a quotient map. The inverse in the diagonal action is essential: it makes the displayed relation and the right action law agree. The quotient construction itself uses no choices. The homogeneous principal bundle of G to G/H is a smooth principal H-bundle is one instance, not a hypothesis of the general definition. The next theorem supplies the smooth vector-bundle atlas in the sense of Vector bundle charts and transition functions.
Depends on
- G to G/H is a smooth principal H-bundle
- Vector bundle charts and transition functions
- Principal g bundle and associated fiber bundle
- The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection
- For a quotient map $q : X \to Y$, a map out of $Y$ is continuous iff its composite with $q$ is; a continuous map on $X$ constant on the fibres of $q$ factors uniquely through $q$; and a composite of quotient maps is a quotient map
Used by
Dependency tree · two levels
19 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. (standard reference, not scraped)