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 xis the fiber of the tangent bundle atx : M, which is defined to beE. -
tangent_bundle I Mis the total space oftangent_space I M, proven to be a smooth vector bundle.
theorem
hidden.cont_diff_on_fderiv_coord_change
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(i j : β₯(charted_space.atlas H M)) :
Auxiliary lemma for tangent spaces: the derivative of a coordinate change between two charts is smooth on its source.
noncomputable
def
hidden.tangent_bundle_core
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
vector_bundle_core π M E β₯(charted_space.atlas H M)
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
@[simp]
theorem
hidden.tangent_bundle_core_coord_change
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(i j : β₯(charted_space.atlas H M))
(x : M) :
@[simp]
theorem
hidden.tangent_bundle_core_base_set
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(i : β₯(charted_space.atlas H M)) :
(hidden.tangent_bundle_core I M).base_set i = i.val.to_local_equiv.source
@[simp]
theorem
hidden.tangent_bundle_core_index_at
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
(hidden.tangent_bundle_core I M).index_at x = achart H x
theorem
hidden.tangent_bundle_core_coord_change_achart
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x x' z : M) :
(hidden.tangent_bundle_core I M).coord_change (achart H x) (achart H x') z = fderiv_within π (β(ext_chart_at I x') β β((ext_chart_at I x).symm)) (set.range βI) (β(ext_chart_at I x) z)
@[nolint]
def
hidden.tangent_space
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
Type u_2
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
@[protected, instance]
def
hidden.tangent_space.add_comm_group
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
@[protected, instance]
def
hidden.tangent_space.topological_add_group
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
@[protected, instance]
def
hidden.tangent_space.topological_space
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
@[nolint, reducible]
def
hidden.tangent_bundle
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
Type (max u_4 u_2)
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
@[protected, instance]
def
hidden.tangent_space.module
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
module π (hidden.tangent_space I x)
Equations
@[protected, instance]
def
hidden.tangent_space.inhabited
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
Equations
- hidden.tangent_space.inhabited I x = {default := 0}
@[protected, instance]
noncomputable
def
hidden.tangent_bundle.topological_space
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
@[protected, instance]
noncomputable
def
hidden.tangent_space.fiber_bundle
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
Equations
@[protected, instance]
def
hidden.tangent_space.vector_bundle
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
vector_bundle π E (hidden.tangent_space I)
theorem
hidden.tangent_space_chart_at
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(p : hidden.tangent_bundle I M) :
charted_space.chart_at (model_prod H E) p = ((hidden.tangent_bundle_core I M).to_fiber_bundle_core.local_triv (achart H p.fst)).to_local_homeomorph.trans ((charted_space.chart_at H p.fst).prod (local_homeomorph.refl E))
theorem
hidden.tangent_space_chart_at_to_local_equiv
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(p : hidden.tangent_bundle I M) :
(charted_space.chart_at (model_prod H E) p).to_local_equiv = ((hidden.tangent_bundle_core I M).to_fiber_bundle_core.local_triv_as_local_equiv (achart H p.fst)).trans ((charted_space.chart_at H p.fst).to_local_equiv.prod (local_equiv.refl E))
@[protected, instance]
def
hidden.tangent_bundle_core.is_smooth
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
(hidden.tangent_bundle_core I M).is_smooth I
@[protected, instance]
def
hidden.tangent_bundle.smooth_vector_bundle
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
The tangent bundle to the model space #
@[simp]
theorem
hidden.tangent_bundle_model_space_chart_at
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(p : hidden.tangent_bundle I H) :
(charted_space.chart_at (model_prod H E) p).to_local_equiv = (equiv.sigma_equiv_prod H E).to_local_equiv
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.
@[simp]
theorem
hidden.tangent_bundle_model_space_coe_chart_at
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(p : hidden.tangent_bundle I H) :
β(charted_space.chart_at (model_prod H E) p) = β(equiv.sigma_equiv_prod H E)
@[simp]
theorem
hidden.tangent_bundle_model_space_coe_chart_at_symm
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners π E H)
(p : hidden.tangent_bundle I H) :
β((charted_space.chart_at (model_prod H E) p).symm) = β((equiv.sigma_equiv_prod H E).symm)
def
hidden.tangent_bundle_model_space_homeomorph
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
(H : Type u_3)
[topological_space H]
(I : model_with_corners π E H) :
hidden.tangent_bundle I H ββ model_prod H E
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 := _}
@[simp]
theorem
hidden.tangent_bundle_model_space_homeomorph_coe
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
(H : Type u_3)
[topological_space H]
(I : model_with_corners π E H) :
@[simp]
theorem
hidden.tangent_bundle_model_space_homeomorph_coe_symm
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
(H : Type u_3)
[topological_space H]
(I : model_with_corners π E H) :