mathlib3 documentation

geometry.manifold.vector_bundle.tangent

Tangent bundles #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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
Instances for tangent_bundle_core
@[protected, instance]
@[nolint]
def tangent_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_4} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_6} [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
Instances for tangent_space
@[protected, instance]
@[nolint, reducible]
def tangent_bundle {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_4} [topological_space H] (I : model_with_corners 𝕜 E H) (M : Type u_6) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] :
Type (max u_6 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 tangent_space.module {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_4} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_6} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (x : M) :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[simp]

The tangent bundle to the model space #

@[simp]

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
theorem in_coordinates_tangent_bundle_core_model_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] (I : model_with_corners 𝕜 E H) {H' : Type u_5} [topological_space H'] (I' : model_with_corners 𝕜 E' H') (x₀ x : H) (y₀ y : H') (ϕ : E →L[𝕜] E') :

The map in_coordinates for the tangent bundle is trivial on the model spaces

noncomputable def in_tangent_coordinates {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] (I : model_with_corners 𝕜 E H) {H' : Type u_5} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M : Type u_6} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {N : Type u_9} (f : N M) (g : N M') (ϕ : N (E →L[𝕜] E')) :
N N (E →L[𝕜] E')

When ϕ x is a continuous linear map that changes vectors in charts around f x to vectors in charts around g x, in_tangent_coordinates I I' f g ϕ x₀ x is a coordinate change of this continuous linear map that makes sense from charts around f x₀ to charts around g x₀ by composing it with appropriate coordinate changes. Note that the type of ϕ is more accurately Π x : N, tangent_space I (f x) →L[𝕜] tangent_space I' (g x). We are unfolding tangent_space in this type so that Lean recognizes that the type of ϕ doesn't actually depend on f or g.

This is the underlying function of the trivializations of the hom of (pullbacks of) tangent spaces.

Equations
theorem in_tangent_coordinates_model_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] (I : model_with_corners 𝕜 E H) {H' : Type u_5} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {N : Type u_9} (f : N H) (g : N H') (ϕ : N (E →L[𝕜] E')) (x₀ : N) :
in_tangent_coordinates I I' f g ϕ x₀ = ϕ
theorem in_tangent_coordinates_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] (I : model_with_corners 𝕜 E H) {H' : Type u_5} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M : Type u_6} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {N : Type u_9} (f : N M) (g : N M') (ϕ : N (E →L[𝕜] E')) {x₀ x : N} (hx : f x (charted_space.chart_at H (f x₀)).to_local_equiv.source) (hy : g x (charted_space.chart_at H' (g x₀)).to_local_equiv.source) :
in_tangent_coordinates I I' f g ϕ x₀ x = ((tangent_bundle_core I' M').coord_change (achart H' (g x)) (achart H' (g x₀)) (g x)).comp ((ϕ x).comp ((tangent_bundle_core I M).coord_change (achart H (f x₀)) (achart H (f x)) (f x)))