mathlib documentation

geometry.manifold.vector_bundle.basic

Smooth vector bundles #

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 #

Charted space structure on a fiber bundle #

@[protected, instance]

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

Equations
@[protected, instance]

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

Smooth vector bundles #

@[class]
structure smooth_vector_bundle {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B Type u_6) [nontrivially_normed_field 𝕜] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module 𝕜 (E x)] [normed_add_comm_group F] [normed_space 𝕜 F] [topological_space (bundle.total_space E)] [Π (x : B), topological_space (E x)] {EB : Type u_7} [normed_add_comm_group EB] [normed_space 𝕜 EB] {HB : Type u_8} [topological_space HB] (IB : model_with_corners 𝕜 EB HB) [topological_space B] [charted_space HB B] [smooth_manifold_with_corners IB B] [fiber_bundle F E] [vector_bundle 𝕜 F 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) [nontrivially_normed_field 𝕜] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module 𝕜 (E x)] [normed_add_comm_group F] [normed_space 𝕜 F] [topological_space (bundle.total_space E)] [Π (x : B), topological_space (E x)] {EB : Type u_7} [normed_add_comm_group EB] [normed_space 𝕜 EB] {HB : Type u_8} [topological_space HB] (IB : model_with_corners 𝕜 EB HB) [topological_space B] [charted_space HB B] [smooth_manifold_with_corners IB B] [fiber_bundle F E] [vector_bundle 𝕜 F E] [smooth_vector_bundle F E 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]

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} [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {EB : Type u_7} [normed_add_comm_group EB] [normed_space 𝕜 EB] {HB : Type u_8} [topological_space HB] [topological_space B] [charted_space HB B] {ι : Type u_9} (Z : vector_bundle_core 𝕜 B F ι) (IB : model_with_corners 𝕜 EB 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} [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {EB : Type u_7} [normed_add_comm_group EB] [normed_space 𝕜 EB] {HB : Type u_8} [topological_space HB] (IB : model_with_corners 𝕜 EB HB) [topological_space B] [charted_space HB B] [smooth_manifold_with_corners IB B] {ι : Type u_9} (Z : vector_bundle_core 𝕜 B F ι) [Z.is_smooth 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]

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} [nontrivially_normed_field 𝕜] {EB : Type u_7} [normed_add_comm_group EB] [normed_space 𝕜 EB] {HB : Type u_8} [topological_space HB] (IB : model_with_corners 𝕜 EB HB) [topological_space B] [charted_space HB B] [smooth_manifold_with_corners IB B] (F₁ : Type u_9) [normed_add_comm_group F₁] [normed_space 𝕜 F₁] (E₁ : B Type u_10) [topological_space (bundle.total_space E₁)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜 (E₁ x)] (F₂ : Type u_11) [normed_add_comm_group F₂] [normed_space 𝕜 F₂] (E₂ : B Type u_12) [topological_space (bundle.total_space E₂)] [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜 (E₂ x)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), topological_space (E₂ x)] [fiber_bundle F₁ E₁] [fiber_bundle F₂ E₂] [vector_bundle 𝕜 F₁ E₁] [vector_bundle 𝕜 F₂ E₂] [smooth_vector_bundle F₁ E₁ IB] [smooth_vector_bundle F₂ 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.