# mathlib3documentation

geometry.manifold.vector_bundle.basic

# Smooth vector bundles #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines smooth vector bundles over a smooth manifold.

Let E be a topological vector bundle, with model fiber F and base space B. We consider E as carrying a charted space structure given by its trivializations -- these are charts to B × F. Then, by "composition", if B is itself a charted space over H (e.g. a smooth manifold), then E is also a charted space over H × F

Now, we define smooth_vector_bundle as the Prop of having smooth transition functions. Recall the structure groupoid smooth_fiberwise_linear on B × F consisting of smooth, fiberwise linear local homeomorphisms. We show that our definition of "smooth vector bundle" implies has_groupoid for this groupoid, and show (by a "composition" of has_groupoid instances) that this means that a smooth vector bundle is a smooth manifold.

Since smooth_vector_bundle is a mixin, it should be easy to make variants and for many such variants to coexist -- vector bundles can be smooth vector bundles over several different base fields, they can also be C^k vector bundles, etc.

## Main definitions and constructions #

• fiber_bundle.charted_space: A fiber bundle E over a base B with model fiber F is naturally a charted space modelled on B × F.

• fiber_bundle.charted_space': Let B be a charted space modelled on HB. Then a fiber bundle E over a base B with model fiber F is naturally a charted space modelled on HB.prod F.

• smooth_vector_bundle: Mixin class stating that a (topological) vector_bundle is smooth, in the sense of having smooth transition functions.

• smooth_fiberwise_linear.has_groupoid: For a smooth vector bundle E over B with fiber modelled on F, the change-of-co-ordinates between two trivializations e, e' for E, considered as charts to B × F, is smooth and fiberwise linear, in the sense of belonging to the structure groupoid smooth_fiberwise_linear.

• bundle.total_space.smooth_manifold_with_corners: A smooth vector bundle is naturally a smooth manifold.

• vector_bundle_core.smooth_vector_bundle: If a (topological) vector_bundle_core is smooth, in the sense of having smooth transition functions (cf. vector_bundle_core.is_smooth), then the vector bundle constructed from it is a smooth vector bundle.

• vector_prebundle.smooth_vector_bundle: If a vector_prebundle is smooth, in the sense of having smooth transition functions (cf. vector_prebundle.is_smooth), then the vector bundle constructed from it is a smooth vector bundle.

• bundle.prod.smooth_vector_bundle: The direct sum of two smooth vector bundles is a smooth vector bundle.

### Charted space structure on a fiber bundle #

@[protected, instance]
def fiber_bundle.charted_space {B : Type u_2} {F : Type u_4} {E : B Type u_6} [Π (x : B), topological_space (E x)] [ E] :
charted_space (B × F) E)

A fiber bundle E over a base B with model fiber F is naturally a charted space modelled on B × F.

Equations
@[protected, instance]
def fiber_bundle.charted_space' {B : Type u_2} {F : Type u_4} {E : B Type u_6} [Π (x : B), topological_space (E x)] {HB : Type u_7} [ B] [ E] :

Let B be a charted space modelled on HB. Then a fiber bundle E over a base B with model fiber F is naturally a charted space modelled on HB.prod F.

Equations
theorem fiber_bundle.charted_space_chart_at {B : Type u_2} {F : Type u_4} {E : B Type u_6} [Π (x : B), topological_space (E x)] {HB : Type u_7} [ B] [ E] (x : E) :
x =
theorem fiber_bundle.charted_space_chart_at_symm_fst {B : Type u_2} {F : Type u_4} {E : B Type u_6} [Π (x : B), topological_space (E x)] {HB : Type u_7} [ B] [ E] (x : E) (y : F) (hy : y (charted_space.chart_at (model_prod HB F) x).to_local_equiv.target) :
@[protected]
theorem fiber_bundle.ext_chart_at {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B Type u_6} [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} (IB : HB) [ B] [ E] (x : E) :

### Smoothness of maps in/out fiber bundles #

Note: For these results we don't need that the bundle is a smooth vector bundle, or even a vector bundle at all, just that it is a fiber bundle over a charted base space.

theorem bundle.cont_mdiff_within_at_total_space {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B Type u_6} [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} {EM : Type u_10} [ EM] {HM : Type u_11} {IM : HM} [ M] {n : ℕ∞} [ B] [ E] (f : M ) {s : set M} {x₀ : M} :
(IB.prod F)) n f s x₀ IB n (λ (x : M), (f x).proj) s x₀ n (λ (x : M), ( (f x₀).proj) (f x)).snd) s x₀

Characterization of C^n functions into a smooth vector bundle.

theorem bundle.cont_mdiff_at_total_space {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B Type u_6} [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} {EM : Type u_10} [ EM] {HM : Type u_11} {IM : HM} [ M] {n : ℕ∞} [ B] [ E] (f : M ) (x₀ : M) :
(IB.prod F)) n f x₀ IB n (λ (x : M), (f x).proj) x₀ n (λ (x : M), ( (f x₀).proj) (f x)).snd) x₀

Characterization of C^n functions into a smooth vector bundle.

theorem bundle.cont_mdiff_at_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B Type u_6} [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} {n : ℕ∞} [ B] [ E] (s : Π (x : B), E x) (x₀ : B) :
(IB.prod F)) n (λ (x : B), {proj := x, snd := s x}) x₀ n (λ (x : B), ( x₀) {proj := x, snd := s x}).snd) x₀

Characterization of C^n sections of a smooth vector bundle.

theorem bundle.cont_mdiff_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B Type u_6) [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} {n : ℕ∞} [ B] [ E] :
theorem bundle.smooth_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B Type u_6) [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} [ B] [ E] :
theorem bundle.cont_mdiff_on_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B Type u_6) [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} {n : ℕ∞} [ B] [ E] {s : set E)} :
theorem bundle.smooth_on_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B Type u_6) [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} [ B] [ E] {s : set E)} :
theorem bundle.cont_mdiff_at_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B Type u_6) [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} {n : ℕ∞} [ B] [ E] {p : E} :
theorem bundle.smooth_at_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B Type u_6) [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} [ B] [ E] {p : E} :
theorem bundle.cont_mdiff_within_at_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B Type u_6) [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} {n : ℕ∞} [ B] [ E] {s : set E)} {p : E} :
theorem bundle.smooth_within_at_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B Type u_6) [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} [ B] [ E] {s : set E)} {p : E} :
s p
theorem bundle.smooth_zero_section (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B Type u_6) [ F] [Π (x : B), topological_space (E x)] {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} [ B] [ E] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] [ E] :
smooth IB (IB.prod F)) E)

### Smooth vector bundles #

@[class]
structure smooth_vector_bundle {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B Type u_6) {EB : Type u_7} [ EB] {HB : Type u_8} (IB : HB) [ B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] [ F] [Π (x : B), topological_space (E x)] [ E] [ E] :
Prop

When B is a smooth manifold with corners with respect to a model IB and E is a topological vector bundle over B with fibers isomorphic to F, then smooth_vector_bundle F E IB registers that the bundle is smooth, in the sense of having smooth transition functions. This is a mixin, not carrying any new data.

Instances of this typeclass
@[protected, instance]
def smooth_fiberwise_linear.has_groupoid {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B Type u_6) {EB : Type u_7} [ EB] {HB : Type u_8} (IB : HB) [ B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] [ F] [Π (x : B), topological_space (E x)] [ E] [ E] [ IB] :
IB)

For a smooth vector bundle E over B with fiber modelled on F, the change-of-co-ordinates between two trivializations e, e' for E, considered as charts to B × F, is smooth and fiberwise linear.

@[protected, instance]
def bundle.total_space.smooth_manifold_with_corners {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B Type u_6) {EB : Type u_7} [ EB] {HB : Type u_8} (IB : HB) [ B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] [ F] [Π (x : B), topological_space (E x)] [ E] [ E] [ IB] :
E)

A smooth vector bundle E is naturally a smooth manifold.

### Core construction for smooth vector bundles #

@[class]
structure vector_bundle_core.is_smooth {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {EB : Type u_7} [ EB] {HB : Type u_8} [ B] [ F] {ι : Type u_11} (Z : F ι) (IB : HB) :
Prop

Mixin for a vector_bundle_core stating smoothness (of transition functions).

Instances of this typeclass
@[protected, instance]
def vector_bundle_core.smooth_vector_bundle {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {EB : Type u_7} [ EB] {HB : Type u_8} (IB : HB) [ B] [ F] {ι : Type u_11} (Z : F ι) [Z.is_smooth IB] :
IB

If a vector_bundle_core has the is_smooth mixin, then the vector bundle constructed from it is a smooth vector bundle.

### The trivial smooth vector bundle #

@[protected, instance]
def bundle.trivial.smooth_vector_bundle {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) {EB : Type u_7} [ EB] {HB : Type u_8} (IB : HB) [ B] [ F] :
IB

A trivial vector bundle over a smooth manifold is a smooth vector bundle.

### Direct sums of smooth vector bundles #

@[protected, instance]
def bundle.prod.smooth_vector_bundle {𝕜 : Type u_1} {B : Type u_2} {EB : Type u_7} [ EB] {HB : Type u_8} (IB : HB) [ B] (F₁ : Type u_11) [ F₁] (E₁ : B Type u_12) [topological_space E₁)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] (F₂ : Type u_13) [ F₂] (E₂ : B Type u_14) [topological_space E₂)] [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), topological_space (E₂ x)] [ E₁] [ E₂] [ F₁ E₁] [ F₂ E₂] [ E₁ IB] [ E₂ IB] :
smooth_vector_bundle (F₁ × F₂) (λ (x : B), E₁ x × E₂ x) IB

The direct sum of two smooth vector bundles over the same base is a smooth vector bundle.

### Prebundle construction for smooth vector bundles #

@[class]
structure vector_prebundle.is_smooth {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B Type u_6} {EB : Type u_7} [ EB] {HB : Type u_8} (IB : HB) [ B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] [ F] [Π (x : B), topological_space (E x)] (a : E) :
Prop

Mixin for a vector_prebundle stating smoothness of coordinate changes.

Instances of this typeclass
noncomputable def vector_prebundle.smooth_coord_change {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B Type u_6} {EB : Type u_7} [ EB] {HB : Type u_8} (IB : HB) [ B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] [ F] [Π (x : B), topological_space (E x)] (a : E) [ha : a] {e e' : bundle.total_space.proj} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) (b : B) :
F →L[𝕜] F

A randomly chosen coordinate change on a smooth_vector_prebundle, given by the field exists_coord_change. Note that a.smooth_coord_change need not be the same as a.coord_change.

Equations
• he' b =
theorem vector_prebundle.smooth_on_smooth_coord_change {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B Type u_6} {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} [ B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] [ F] [Π (x : B), topological_space (E x)] (a : E) [ha : a] {e e' : bundle.total_space.proj} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) :
(F →L[𝕜] F)) he') (e.base_set e'.base_set)
theorem vector_prebundle.smooth_coord_change_apply {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B Type u_6} {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} [ B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] [ F] [Π (x : B), topological_space (E x)] (a : E) [ha : a] {e e' : bundle.total_space.proj} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) {b : B} (hb : b e.base_set e'.base_set) (v : F) :
he' b) v = (e' {proj := b, snd := e.symm b v}).snd
theorem vector_prebundle.mk_smooth_coord_change {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B Type u_6} {EB : Type u_7} [ EB] {HB : Type u_8} {IB : HB} [ B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] [ F] [Π (x : B), topological_space (E x)] (a : E) [ha : a] {e e' : bundle.total_space.proj} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) {b : B} (hb : b e.base_set e'.base_set) (v : F) :
(b, he' b) v) = e' {proj := b, snd := e.symm b v}
theorem vector_prebundle.smooth_vector_bundle {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B Type u_6} {EB : Type u_7} [ EB] {HB : Type u_8} (IB : HB) [ B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] [ F] [Π (x : B), topological_space (E x)] (a : E) [ha : a] :
IB

Make a smooth_vector_bundle from a smooth_vector_prebundle`.