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.
Whitney sum, tensor, dual, Hom, and exterior-power bundles
Definition
Let and be finite-rank -vector bundles over , with transition matrices and on a common refinement. Apply Vector bundles are glued from transition cocycles to the following transition maps:
- : ;
- : ;
- : ;
- : ;
- : .
These define the Whitney sum, tensor product, dual, Hom, and exterior-power bundles. Their fibers are respectively , , , , and . The cocycle theorem also shows that changes of frame give canonically isomorphic bundles.
For a complex bundle, conjugating every transition matrix defines , and regarding those matrices as real-linear defines the underlying real bundle . We set and when . Applying the same matrices after precomposition with a base map shows, under the canonical comparisons of Vector-bundle pullback is canonically functorial, that every construction commutes with pullback.