Tangent bundles #
This file defines the tangent bundle as a smooth vector bundle.
Let M
be a smooth manifold with corners with model I
on (E, H)
. We define the tangent bundle
of M
using the vector_bundle_core
construction indexed by the charts of M
with fibers E
.
Given two charts i, j : local_homeomorph M H
, the coordinate change between i
and j
at a point
x : M
is the derivative of the composite
I.symm i.symm j I
E -----> H -----> M --> H --> E
within the set range I β E
at I (i x) : E
.
This defines a smooth vector bundle tangent_bundle
with fibers tangent_space
.
Main definitions #
-
tangent_space I M x
is the fiber of the tangent bundle atx : M
, which is defined to beE
. -
tangent_bundle I M
is the total space oftangent_space I M
, proven to be a smooth vector bundle.
Auxiliary lemma for tangent spaces: the derivative of a coordinate change between two charts is smooth on its source.
Let M
be a smooth manifold with corners with model I
on (E, H)
.
Then vector_bundle_core I M
is the vector bundle core for the tangent bundle over M
.
It is indexed by the atlas of M
, with fiber E
and its change of coordinates from the chart i
to the chart j
at point x : M
is the derivative of the composite
I.symm i.symm j I
E -----> H -----> M --> H --> E
within the set range I β E
at I (i x) : E
.
Equations
- hidden.tangent_bundle_core I M = {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), fderiv_within π (β(j.val.extend I) β β((i.val.extend I).symm)) (set.range βI) (β(i.val.extend I) x), coord_change_self := _, continuous_on_coord_change := _, coord_change_comp := _}
Instances for hidden.tangent_bundle_core
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
- hidden.tangent_space I x = E
Instances for hidden.tangent_space
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
Equations
Equations
- hidden.tangent_space.inhabited I x = {default := 0}
Equations
The tangent bundle to the model space #
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
- hidden.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 := _}