# Documentation

Mathlib.Geometry.Manifold.VectorBundle.Tangent

# 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 VectorBundleCore construction indexed by the charts of M with fibers E. Given two charts i, j : LocalHomeomorph 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 TangentBundle with fibers TangentSpace.

## Main definitions #

• TangentSpace I M x is the fiber of the tangent bundle at x : M, which is defined to be E.

• TangentBundle I M is the total space of TangentSpace I M, proven to be a smooth vector bundle.

theorem contDiffOn_fderiv_coord_change {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] (i : ↑(atlas H M)) (j : ↑(atlas H M)) :
ContDiffOn 𝕜 (fderivWithin 𝕜 (↑() ↑()) ()) (LocalEquiv.trans () ()).source

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

@[simp]
theorem tangentBundleCore_indexAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (x : M) :
= achart H x
@[simp]
theorem tangentBundleCore_coordChange {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (i : ↑(atlas H M)) (j : ↑(atlas H M)) (x : M) :
= fderivWithin 𝕜 (↑() ↑()) () (↑() x)
def tangentBundleCore {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] :
VectorBundleCore 𝕜 M E ↑(atlas H M)

Let M be a smooth manifold with corners with model I on (E, H). Then VectorBundleCore 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.

Instances For
@[simp]
theorem tangentBundleCore_baseSet {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (i : ↑(atlas H M)) :
= (i).source
theorem tangentBundleCore_coordChange_achart {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] (x : M) (x' : M) (z : M) :
VectorBundleCore.coordChange () (achart H x) (achart H x') z = fderivWithin 𝕜 (↑(extChartAt I x') ↑()) () (↑() z)
def TangentSpace {𝕜 : Type u_10} {E : Type u_9} [] {H : Type u_11} [] (I : ) {M : Type u_12} [] [] (_x : M) :
Type u_9

The tangent space at a point of the manifold M. It is just E. We could use instead (tangentBundleCore I M).to_topological_vector_bundle_core.fiber x, but we use E to help the kernel.

Instances For
instance instTopologicalSpaceTangentSpace {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] {x : M} :
instance instAddCommGroupTangentSpace {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] {x : M} :
instance instTopologicalAddGroupTangentSpaceInstTopologicalSpaceTangentSpaceToAddGroupInstAddCommGroupTangentSpace {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] {x : M} :
@[reducible]
def TangentBundle {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] :
Type (max u_6 u_2)

The tangent bundle to a smooth manifold, as a Sigma type. Defined in terms of Bundle.TotalSpace to be able to put a suitable topology on it.

Instances For
instance instInhabitedTangentSpace {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] (x : M) :
instance instTopologicalSpaceTangentBundle {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] :
instance TangentSpace.fiberBundle {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] :
instance TangentSpace.vectorBundle {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] :
VectorBundle 𝕜 E ()
theorem TangentBundle.chartAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (p : ) :
chartAt () p = LocalHomeomorph.trans (FiberBundleCore.localTriv () (achart H p.proj)).toLocalHomeomorph (LocalHomeomorph.prod (chartAt H p.proj) ())
theorem TangentBundle.chartAt_toLocalEquiv {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (p : ) :
(chartAt () p).toLocalEquiv = LocalEquiv.trans (FiberBundleCore.localTrivAsLocalEquiv () (achart H p.proj)) (LocalEquiv.prod (chartAt H p.proj).toLocalEquiv ())
theorem TangentBundle.trivializationAt_eq_localTriv {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (x : M) :
@[simp]
theorem TangentBundle.trivializationAt_source {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (x : M) :
().toLocalHomeomorph.toLocalEquiv.source = Bundle.TotalSpace.proj ⁻¹' (chartAt H x).toLocalEquiv.source
@[simp]
theorem TangentBundle.trivializationAt_target {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (x : M) :
().toLocalHomeomorph.toLocalEquiv.target = (chartAt H x).toLocalEquiv.source ×ˢ Set.univ
@[simp]
theorem TangentBundle.trivializationAt_baseSet {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (x : M) :
().baseSet = (chartAt H x).toLocalEquiv.source
theorem TangentBundle.trivializationAt_apply {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (x : M) (z : ) :
↑() z = (z.proj, ↑(fderivWithin 𝕜 (↑() ↑(LocalEquiv.symm (LocalHomeomorph.extend (chartAt H z.proj) I))) () (↑(LocalHomeomorph.extend (chartAt H z.proj) I) z.proj)) z.snd)
@[simp]
theorem TangentBundle.trivializationAt_fst {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (x : M) (z : ) :
(↑() z).fst = z.proj
@[simp]
theorem TangentBundle.mem_chart_source_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (p : ) (q : ) :
p (chartAt () q).toLocalEquiv.source p.proj (chartAt H q.proj).toLocalEquiv.source
@[simp]
theorem TangentBundle.mem_chart_target_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (p : H × E) (q : ) :
p (chartAt () q).toLocalEquiv.target p.fst (chartAt H q.proj).toLocalEquiv.target
@[simp]
theorem TangentBundle.coe_chartAt_fst {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (p : ) (q : ) :
(↑(chartAt () q) p).fst = ↑(chartAt H q.proj) p.proj
@[simp]
theorem TangentBundle.coe_chartAt_symm_fst {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (p : H × E) (q : ) :
(↑(LocalHomeomorph.symm (chartAt () q)) p).proj = ↑(LocalHomeomorph.symm (chartAt H q.proj)) p.fst
@[simp]
theorem TangentBundle.trivializationAt_continuousLinearMapAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] {b₀ : M} {b : M} (hb : b (trivializationAt E () b₀).baseSet) :
@[simp]
theorem TangentBundle.trivializationAt_symmL {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] {b₀ : M} {b : M} (hb : b (trivializationAt E () b₀).baseSet) :
@[simp]
theorem TangentBundle.coordChange_model_space {𝕜 : Type u_1} {F : Type u_8} [] (b : F) (b' : F) (x : F) :
@[simp]
theorem TangentBundle.symmL_model_space {𝕜 : Type u_1} {F : Type u_8} [] (b : F) (b' : F) :
Trivialization.symmL 𝕜 () b' = 1
@[simp]
theorem TangentBundle.continuousLinearMapAt_model_space {𝕜 : Type u_1} {F : Type u_8} [] (b : F) (b' : F) :
= 1
instance tangentBundleCore.isSmooth {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] :
instance TangentBundle.smoothVectorBundle {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] :

## The tangent bundle to the model space #

@[simp]
theorem tangentBundle_model_space_chartAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (p : ) :
(chartAt () p).toLocalEquiv =

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. TotalSpace.toProd.

@[simp]
theorem tangentBundle_model_space_coe_chartAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (p : ) :
↑(chartAt () p) = ↑()
@[simp]
theorem tangentBundle_model_space_coe_chartAt_symm {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (p : ) :
↑(LocalHomeomorph.symm (chartAt () p)) = ().symm
theorem tangentBundleCore_coordChange_model_space {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (x : H) (x' : H) (z : H) :
def tangentBundleModelSpaceHomeomorph {𝕜 : Type u_1} {E : Type u_2} [] (H : Type u_4) [] (I : ) :

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

Instances For
@[simp]
theorem tangentBundleModelSpaceHomeomorph_coe {𝕜 : Type u_1} {E : Type u_2} [] (H : Type u_4) [] (I : ) :
@[simp]
theorem tangentBundleModelSpaceHomeomorph_coe_symm {𝕜 : Type u_1} {E : Type u_2} [] (H : Type u_4) [] (I : ) :
= ().symm
theorem inCoordinates_tangent_bundle_core_model_space {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_4} [] (I : ) {H' : Type u_5} [] (I' : ModelWithCorners 𝕜 E' H') (x₀ : H) (x : H) (y₀ : H') (y : H') (ϕ : E →L[𝕜] E') :
ContinuousLinearMap.inCoordinates E () E' () x₀ x y₀ y ϕ = ϕ

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

def inTangentCoordinates {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_4} [] (I : ) {H' : Type u_5} [] (I' : ModelWithCorners 𝕜 E' H') {M : Type u_6} [] [] {M' : Type u_7} [] [ChartedSpace H' M'] [] {N : Type u_9} (f : NM) (g : NM') (ϕ : NE →L[𝕜] E') :
NNE →L[𝕜] E'

When ϕ x is a continuous linear map that changes vectors in charts around f x to vectors in charts around g x, inTangentCoordinates 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, TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x). We are unfolding TangentSpace 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.

Instances For
theorem inTangentCoordinates_model_space {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_4} [] (I : ) {H' : Type u_5} [] (I' : ModelWithCorners 𝕜 E' H') {N : Type u_9} (f : NH) (g : NH') (ϕ : NE →L[𝕜] E') (x₀ : N) :
inTangentCoordinates I I' f g ϕ x₀ = ϕ
theorem inTangentCoordinates_eq {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_4} [] (I : ) {H' : Type u_5} [] (I' : ModelWithCorners 𝕜 E' H') {M : Type u_6} [] [] {M' : Type u_7} [] [ChartedSpace H' M'] [] {N : Type u_9} (f : NM) (g : NM') (ϕ : NE →L[𝕜] E') {x₀ : N} {x : N} (hx : f x (chartAt H (f x₀)).toLocalEquiv.source) (hy : g x (chartAt H' (g x₀)).toLocalEquiv.source) :
inTangentCoordinates I I' f g ϕ x₀ x = ContinuousLinearMap.comp (VectorBundleCore.coordChange () (achart H' (g x)) (achart H' (g x₀)) (g x)) (ContinuousLinearMap.comp (ϕ x) (VectorBundleCore.coordChange () (achart H (f x₀)) (achart H (f x)) (f x)))