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 thatM
is a smooth manifold over the model with cornersI
on(π, E, H)
, andF
is a normed vector space overπ
, this structure registers, for each pair of charts ofM
, a smooth change of coordinates onF
. This is the core structure from which one will build a smooth bundle with fiberF
overM
.
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 Ξ£ (x : 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 manifoldM
over a model with cornersI
.tangent_bundle I M
: the total space oftangent_bundle_core I M
. It is itself a smooth manifold over the model with cornersI.tangent
, the product ofI
and the trivial model with corners onE
.tangent_space I x
: the tangent space toM
atx
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
- coord_change : β₯(atlas H M) β β₯(atlas H M) β H β F β F
- coord_change_self : β (i : β₯(atlas H M)) (x : H), x β i.val.to_local_equiv.target β β (v : F), c.coord_change i i x v = v
- coord_change_comp : β (i j k : β₯(atlas H M)) (x : H), x β ((i.val.symm β«β j.val) β«β j.val.symm β«β k.val).to_local_equiv.source β β (v : F), c.coord_change j k (β(i.val.symm β«β j.val) x) (c.coord_change i j x v) = c.coord_change i k x v
- coord_change_smooth : β (i j : β₯(atlas H M)), times_cont_diff_on π β€ (Ξ» (p : E Γ F), c.coord_change i j (β(I.symm) p.fst) p.snd) ((βI '' (i.val.symm β«β j.val).to_local_equiv.source).prod set.univ)
Core structure used to create a smooth bundle above M
(a manifold over the model with
corner I
) with fiber the normed vector space F
over π
, which is trivial in the chart domains
of M
. This structure registers the changes in the fibers when one changes coordinate charts in the
base. We do not require the change of coordinates of the fibers to be linear, only smooth.
Therefore, the fibers of the resulting bundle will not inherit a canonical vector space structure
in general.
The trivial basic smooth bundle core, in which all the changes of coordinates are the identity.
Equations
- trivial_basic_smooth_bundle_core I M F = {coord_change := Ξ» (i j : β₯(atlas H M)) (x : H) (v : F), v, coord_change_self := _, coord_change_comp := _, coord_change_smooth := _}
Equations
- basic_smooth_bundle_core.inhabited = {default := trivial_basic_smooth_bundle_core I M F _inst_9}
Fiber bundle core associated to a basic smooth bundle core
Equations
- Z.to_topological_fiber_bundle_core = {base_set := Ξ» (i : β₯(atlas H M)), i.val.to_local_equiv.source, is_open_base_set := _, index_at := Ξ» (x : M), β¨chart_at H x, _β©, mem_base_set_at := _, coord_change := Ξ» (i j : β₯(atlas H M)) (x : M) (v : F), Z.coord_change i j (β(i.val) x) v, coord_change_self := _, coord_change_continuous := _, coord_change_comp := _}
Local chart for the total space of a basic smooth bundle
Equations
- Z.chart he = Z.to_topological_fiber_bundle_core.local_triv β¨e, heβ© β«β e.prod (local_homeomorph.refl F)
The total space of a basic smooth bundle is endowed with a charted space structure, where the charts are in bijection with the charts of the basis.
Equations
- Z.to_charted_space = {atlas := β (e : local_homeomorph M H) (he : e β atlas H M), {Z.chart he}, chart_at := Ξ» (p : Z.to_topological_fiber_bundle_core.total_space), Z.chart _, mem_chart_source := _, chart_mem_atlas := _}
Smooth manifold structure on the total space of a basic smooth bundle
Basic smooth bundle core version of the tangent bundle of a smooth manifold M
modelled over a
model with corners I
on (E, H)
. The fibers are equal to E
, and the coordinate change in the
fiber corresponds to the derivative of the coordinate change in M
.
Equations
- tangent_bundle_core I M = {coord_change := Ξ» (i j : β₯(atlas H M)) (x : H) (v : E), β(fderiv_within π (βI β β(j.val) β β(i.val.symm) β β(I.symm)) (set.range βI) (βI x)) v, coord_change_self := _, coord_change_comp := _, coord_change_smooth := _}
The tangent space at a point of the manifold M
. It is just E
. We could use instead
(tangent_bundle_core I M).to_topological_fiber_bundle_core.fiber x
, but we use E
to help the
kernel.
Equations
- tangent_space I x = E
The tangent bundle to a smooth manifold, as a plain type. We could use
(tangent_bundle_core I M).to_topological_fiber_bundle_core.total_space
, but instead we use the
(definitionally equal) Ξ£ (x : M), tangent_space I x
, to make sure that rcasing an element of the
tangent bundle gives a second component in the tangent space.
Equations
- tangent_bundle I M = Ξ£ (x : M), tangent_space I x
The projection from the tangent bundle of a smooth manifold to the manifold. As the tangent
bundle is represented internally as a product type, the notation p.1
also works for the projection
of the point p
.
Equations
- tangent_bundle.proj I M = Ξ» (p : tangent_bundle I M), p.fst
Equations
Equations
Equations
Equations
- tangent_space.inhabited I x = {default := 0}
The tangent bundle projection on the basis is a continuous map.
The tangent bundle projection on the basis is an open map.
In the tangent bundle to the model space, the charts are just the canonical identification
between a product type and a sigma type, a.k.a. equiv.sigma_equiv_prod
.
The canonical identification between the tangent bundle to the model space and the product, as a homeomorphism
Equations
- tangent_bundle_model_space_homeomorph H I = {to_equiv := {to_fun := (equiv.sigma_equiv_prod H E).to_fun, inv_fun := (equiv.sigma_equiv_prod H E).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}