Standard constructions on vector bundles #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file contains several standard constructions on vector bundles:
bundle.trivial.vector_bundle 𝕜 B F: the trivial vector bundle with scalar field
𝕜 and model
F over the base
vector_bundle.prod: for vector bundles
E₂ with scalar field
𝕜 over a common base,
a vector bundle structure on their direct sum
E₁ ×ᵇ E₂ (the notation stands for
λ x, E₁ x × E₂ x).
vector_bundle.pullback: for a vector bundle
B, a vector bundle structure on its
f *ᵖ E by a map
f : B' → B (the notation is a type synonym for
E ∘ f).
Vector bundle, direct sum, pullback
The trivial vector bundle #
Direct sum of two vector bundles #
The product of two vector bundles is a vector bundle.
Pullbacks of vector bundles #