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 fiber
Fover 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 pullback
f *ᵖ Eby 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 #
- bundle.pullback.add_comm_monoid E f = λ (x : B'), _inst_1 (f x)
- bundle.pullback.module R E f = λ (x : B'), _inst_3 (f x)