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 #

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.

Smooth vector bundles #

Core construction for smooth vector bundles #

The trivial smooth vector bundle #

Direct sums of smooth vector bundles #

Prebundle construction for smooth vector bundles #