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.
Main definitions #
basic_smooth_vector_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 linear change of coordinates onF
depending smoothly on the base point. This is the core structure from which one will build a smooth vector bundle with fiberF
overM
.
Let Z
be a basic smooth bundle core over M
with fiber F
. We define
Z.to_topological_vector_bundle_core
, the (topological) vector bundle core associated to Z
. From
it, we get a space Z.to_topological_vector_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 #
We register the vector space structure on the fibers of the tangent bundle, but 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 : β₯(charted_space.atlas H M) β β₯(charted_space.atlas H M) β H β (F βL[π] F)
- coord_change_self : β (i : β₯(charted_space.atlas H M)) (x : H), x β i.val.to_local_equiv.target β β (v : F), β(self.coord_change i i x) v = v
- coord_change_comp : β (i j k : β₯(charted_space.atlas H M)) (x : H), x β ((i.val.symm.trans j.val).trans (j.val.symm.trans k.val)).to_local_equiv.source β β (v : F), β(self.coord_change j k (β(i.val.symm.trans j.val) x)) (β(self.coord_change i j x) v) = β(self.coord_change i k x) v
- coord_change_smooth_clm : β (i j : β₯(charted_space.atlas H M)), cont_diff_on π β€ (self.coord_change i j β β(I.symm)) (βI '' (i.val.symm.trans j.val).to_local_equiv.source)
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 require the change of coordinates of the fibers to be linear, so that the resulting bundle
is a vector bundle.
Instances for basic_smooth_vector_bundle_core
- basic_smooth_vector_bundle_core.has_sizeof_inst
- basic_smooth_vector_bundle_core.inhabited
The trivial basic smooth bundle core, in which all the changes of coordinates are the identity.
Equations
- trivial_basic_smooth_vector_bundle_core I M F = {coord_change := Ξ» (i j : β₯(charted_space.atlas H M)) (x : H), continuous_linear_map.id π F, coord_change_self := _, coord_change_comp := _, coord_change_smooth_clm := _}
Equations
Vector bundle core associated to a basic smooth bundle core
Equations
- Z.to_topological_vector_bundle_core = {base_set := Ξ» (i : β₯(charted_space.atlas H M)), i.val.to_local_equiv.source, is_open_base_set := _, index_at := achart H _inst_6, mem_base_set_at := _, coord_change := Ξ» (i j : β₯(charted_space.atlas H M)) (x : M), Z.coord_change i j (β(i.val) x), 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_vector_bundle_core.local_triv β¨e, heβ©).to_fiber_bundle_trivialization.to_local_homeomorph.trans (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 β charted_space.atlas H M), {Z.chart he}, chart_at := Ξ» (p : Z.to_topological_vector_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 : β₯(charted_space.atlas H M)) (x : H), fderiv_within π (βI β β(j.val) β β(i.val.symm) β β(I.symm)) (set.range βI) (βI x), coord_change_self := _, coord_change_comp := _, coord_change_smooth_clm := _}
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_vector_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 Sigma type. Defined in terms of
bundle.total_space
to be able to put a suitable topology on it.
Equations
The projection from the tangent bundle of a smooth manifold to the manifold. As the tangent
bundle is represented internally as a sigma 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
- tangent_space.inhabited I x = {default := 0}
Equations
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 := _}