Basic smooth bundles

In general, a smooth bundle is a bundle over a smooth manifold, whose fiber is a manifold, and for which the coordinate changes are smooth. In this definition, there are charts involved at several places: in the manifold structure of the base, in the manifold structure of the fibers, and in the local trivializations. This makes it a complicated object in general. There is however a specific situation where things are much simpler: when the fiber is a vector space (no need for charts for the fibers), and when the local trivializations of the bundle and the charts of the base coincide. Then everything is expressed in terms of the charts of the base, making for a much simpler overall structure, which is easier to manipulate formally.

Most vector bundles that naturally occur in differential geometry are of this form: the tangent bundle, the cotangent bundle, differential forms (used to define de Rham cohomology) and the bundle of Riemannian metrics. Therefore, it is worth defining a specific constructor for this kind of bundle, that we call basic smooth bundles.

A basic smooth bundle is thus a smooth bundle over a smooth manifold whose fiber is a vector space, and which is trivial in the coordinate charts of the base. (We recall that in our notion of manifold there is a distinguished atlas, which does not need to be maximal: we require the triviality above this specific atlas). It can be constructed from a basic smooth bundled core, defined below, specifying the changes in the fiber when one goes from one coordinate chart to another one. We do not require that this changes in fiber are linear, but only diffeomorphisms.

Main definitions

• basic_smooth_bundle_core I M F: assuming that M is a smooth manifold over the model with corners I on (𝕜, E, H), and F is a normed vector space over 𝕜, this structure registers, for each pair of charts of M, a smooth change of coordinates on F. This is the core structure from which one will build a smooth bundle with fiber F over M.

Let Z be a basic smooth bundle core over M with fiber F. We define Z.to_topological_fiber_bundle_core, the (topological) fiber bundle core associated to Z. From it, we get a space Z.to_topological_fiber_bundle_core.total_space (which as a Type is just M × F), with the fiber bundle topology. It inherits a manifold structure (where the charts are in bijection with the charts of the basis). We show that this manifold is smooth.

Then we use this machinery to construct the tangent bundle of a smooth manifold.

• tangent_bundle_core I M: the basic smooth bundle core associated to a smooth manifold M over a model with corners I.
• tangent_bundle I M : the total space of tangent_bundle_core I M. It is itself a smooth manifold over the model with corners I.tangent, the product of I and the trivial model with corners on E.
• tangent_space I x : the tangent space to M at x
• tangent_bundle.proj I M: the projection from the tangent bundle to the base manifold

Implementation notes

In the definition of a basic smooth bundle core, we do not require that the coordinate changes of the fibers are linear map, only that they are diffeomorphisms. Therefore, the fibers of the resulting fiber bundle do not inherit a vector space structure (as an algebraic object) in general. As the fiber, as a type, is just F, one can still always register the vector space structure, but it does not make sense to do so (i.e., it will not lead to any useful theorem) unless this structure is canonical, i.e., the coordinate changes are linear maps.

For instance, we register the vector space structure on the fibers of the tangent bundle. However, we do not register the normed space structure coming from that of F (as it is not canonical, and we also want to keep the possibility to add a Riemannian structure on the manifold later on without having two competing normed space instances on the tangent spaces).

We require F to be a normed space, and not just a topological vector space, as we want to talk about smooth functions on F. The notion of derivative requires a norm to be defined.

TODO

construct the cotangent bundle, and the bundles of differential forms. They should follow functorially from the description of the tangent bundle as a basic smooth bundle.

Tags

Smooth fiber bundle, vector bundle, tangent space, tangent bundle