# mathlib3documentation

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 #

theorem cont_diff_on_fderiv_coord_change {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) {M : Type u_6} [ M] (i j : M)) :

Auxiliary lemma for tangent spaces: the derivative of a coordinate change between two charts is smooth on its source.

@[simp]
theorem tangent_bundle_core_base_set {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (i : M)) :
noncomputable def tangent_bundle_core {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M]  :
E 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
Instances for tangent_bundle_core
@[simp]
theorem tangent_bundle_core_coord_change {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (i j : M)) (x : M) :
i j x = ((j.val.extend I) ((i.val.extend I).symm)) (set.range I) ((i.val.extend I) x)
@[simp]
theorem tangent_bundle_core_index_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (x : M) :
M).index_at x = x
theorem tangent_bundle_core_coord_change_achart {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) {M : Type u_6} [ M] (x x' z : M) :
(achart H x) (achart H x') z = ( x') ((ext_chart_at I x).symm)) (set.range I) ( x) z)
@[protected, instance]
def tangent_space.topological_space {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) {M : Type u_6} [ M] (x : M) :
@[protected, instance]
def tangent_space.topological_add_group {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) {M : Type u_6} [ M] (x : M) :
@[nolint]
def tangent_space {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) {M : Type u_6} [ 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
• = E
Instances for tangent_space
@[protected, instance]
def tangent_space.add_comm_group {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) {M : Type u_6} [ M] (x : M) :
@[nolint, reducible]
def tangent_bundle {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ 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} {E : Type u_2} [ E] {H : Type u_4} (I : H) {M : Type u_6} [ M] (x : M) :
x)
Equations
@[protected, instance]
def tangent_space.inhabited {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) {M : Type u_6} [ M] (x : M) :
Equations
@[protected, instance]
def tangent_space.has_continuous_add {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) {M : Type u_6} [ M] {x : M} :
@[protected, instance]
noncomputable def tangent_bundle.topological_space {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M]  :
Equations
@[protected, instance]
noncomputable def tangent_space.fiber_bundle {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M]  :
Equations
@[protected, instance]
def tangent_space.vector_bundle {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M]  :
@[protected]
theorem tangent_bundle.chart_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (p : M) :
p = p.proj).prod
theorem tangent_bundle.chart_at_to_local_equiv {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (p : M) :
theorem tangent_bundle.trivialization_at_eq_local_triv {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (x : M) :
@[simp]
theorem tangent_bundle.trivialization_at_source {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (x : M) :
@[simp]
theorem tangent_bundle.trivialization_at_target {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (x : M) :
@[simp]
theorem tangent_bundle.trivialization_at_base_set {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (x : M) :
theorem tangent_bundle.trivialization_at_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (x : M) (z : M) :
z = (z.proj, ( x).extend I) z.proj).extend I).symm)) (set.range I) ( z.proj).extend I) z.proj)) z.snd)
@[simp]
theorem tangent_bundle.trivialization_at_fst {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (x : M) (z : M) :
( z).fst = z.proj
@[simp]
theorem tangent_bundle.mem_chart_source_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (p q : M) :
@[simp]
theorem tangent_bundle.mem_chart_target_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (p : H × E) (q : M) :
@[simp]
theorem tangent_bundle.coe_chart_at_fst {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (p q : M) :
( q) p).fst = p.proj
@[simp]
theorem tangent_bundle.coe_chart_at_symm_fst {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] (p : H × E) (q : M) :
@[simp]
theorem tangent_bundle.trivialization_at_continuous_linear_map_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] {b₀ b : M} (hb : b b₀).base_set) :
= (achart H b) (achart H b₀) b
@[simp]
theorem tangent_bundle.trivialization_at_symmL {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M] {b₀ b : M} (hb : b b₀).base_set) :
b = (achart H b₀) (achart H b) b
@[simp]
theorem tangent_bundle.coord_change_model_space {𝕜 : Type u_1} {F : Type u_8} [ F] (b b' x : F) :
(achart F b) (achart F b') x = 1
@[simp]
theorem tangent_bundle.symmL_model_space {𝕜 : Type u_1} {F : Type u_8} [ F] (b b' : F) :
= 1
@[simp]
theorem tangent_bundle.continuous_linear_map_at_model_space {𝕜 : Type u_1} {F : Type u_8} [ F] (b b' : F) :
@[protected, instance]
def tangent_bundle_core.is_smooth {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M]  :
M).is_smooth I
@[protected, instance]
def tangent_bundle.smooth_vector_bundle {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (M : Type u_6) [ M]  :

## The tangent bundle to the model space #

@[simp]
theorem tangent_bundle_model_space_chart_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (p : H) :

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 tangent_bundle_model_space_coe_chart_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (p : H) :
p) =
@[simp]
theorem tangent_bundle_model_space_coe_chart_at_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (p : H) :
theorem tangent_bundle_core_coord_change_model_space {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) (x x' z : H) :
(achart H x) (achart H x') z =
def tangent_bundle_model_space_homeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] (H : Type u_4) (I : H) :

The canonical identification between the tangent bundle to the model space and the product, as a homeomorphism

Equations
@[simp]
theorem tangent_bundle_model_space_homeomorph_coe {𝕜 : Type u_1} {E : Type u_2} [ E] (H : Type u_4) (I : H) :
@[simp]
theorem tangent_bundle_model_space_homeomorph_coe_symm {𝕜 : Type u_1} {E : Type u_2} [ E] (H : Type u_4) (I : H) :
theorem in_coordinates_tangent_bundle_core_model_space {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} (I : H) {H' : Type u_5} (I' : H') (x₀ x : H) (y₀ y : H') (ϕ : E →L[𝕜] E') :
x₀ x y₀ y ϕ = ϕ

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

noncomputable def in_tangent_coordinates {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} (I : H) {H' : Type u_5} (I' : H') {M : Type u_6} [ M] {M' : Type u_7} [ M'] [ 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
• f g ϕ = λ (x₀ x : N), (f x₀) (f x) (g x₀) (g x) (ϕ x)
theorem in_tangent_coordinates_model_space {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} (I : H) {H' : Type u_5} (I' : H') {N : Type u_9} (f : N H) (g : N H') (ϕ : N (E →L[𝕜] E')) (x₀ : N) :
f g ϕ x₀ = ϕ
theorem in_tangent_coordinates_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} (I : H) {H' : Type u_5} (I' : H') {M : Type u_6} [ M] {M' : Type u_7} [ M'] [ M'] {N : Type u_9} (f : N M) (g : N M') (ϕ : N (E →L[𝕜] E')) {x₀ x : N} (hx : f x (f x₀)).to_local_equiv.source) (hy : g x (g x₀)).to_local_equiv.source) :
f g ϕ x₀ x = M').coord_change (achart H' (g x)) (achart H' (g x₀)) (g x)).comp ((ϕ x).comp M).coord_change (achart H (f x₀)) (achart H (f x)) (f x)))
@[protected, instance]
def tangent_space.path_connected_space {E : Type u_1} [ E] {H : Type u_2} {I : H} {M : Type u_3} [ M] {x : M} :