# 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 : PartialHomeomorph 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 𝕜 (((j).extend I) ((i).extend I).symm) ()) (((i).extend I).symm.trans ((j).extend I)).source

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

@[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) :
().coordChange i j x = fderivWithin 𝕜 (((j).extend I) ((i).extend I).symm) () (((i).extend I) x)
@[simp]
theorem tangentBundleCore_indexAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (x : M) :
().indexAt x = achart H 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.

Equations
• One or more equations did not get rendered due to their size.
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)) :
().baseSet i = (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) :
().coordChange (achart H x) (achart H x') z = fderivWithin 𝕜 ((extChartAt I x') ().symm) () (() z)
@[reducible, inline]
abbrev tangentCoordChange {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] (x : M) (y : M) :
ME →L[𝕜] E

In a manifold M, given two preferred charts indexed by x y : M, tangentCoordChange I x y is the family of derivatives of the corresponding change-of-coordinates map. It takes junk values outside the intersection of the sources of the two charts.

Note that this definition takes advantage of the fact that tangentBundleCore has the same base sets as the preferred charts of the base manifold.

Equations
Instances For
theorem tangentCoordChange_def {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {x : M} {y : M} {z : M} :
= fderivWithin 𝕜 (() ().symm) () (() z)
theorem tangentCoordChange_self {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {x : M} {z : M} {v : E} (h : z ().source) :
() v = v
theorem tangentCoordChange_comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {w : M} {x : M} {y : M} {z : M} {v : E} (h : z ().source ().source ().source) :
() (() v) = () v
theorem hasFDerivWithinAt_tangentCoordChange {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {x : M} {y : M} {z : M} (h : z ().source ().source) :
HasFDerivWithinAt (() ().symm) () () (() z)
theorem continuousOn_tangentCoordChange {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] (x : M) (y : M) :
ContinuousOn () (().source ().source)
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.

Equations
Instances For
instance instTopologicalSpaceTangentSpace {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] {x : M} :
Equations
instance instAddCommGroupTangentSpace {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] {x : M} :
Equations
instance instTopologicalAddGroupTangentSpace {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] {x : M} :
Equations
• =
@[reducible, inline]
abbrev 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.

Equations
Instances For
instance instModuleTangentSpace {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] (x : M) :
Module 𝕜 ()
Equations
instance instInhabitedTangentSpace {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] (x : M) :
Equations
• = { default := 0 }
instance instTopologicalSpaceTangentBundle {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] :
Equations
• = ().toTopologicalSpace
instance TangentSpace.fiberBundle {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] :
Equations
• = ().fiberBundle
instance TangentSpace.vectorBundle {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] :
VectorBundle 𝕜 E ()
Equations
• =
theorem TangentBundle.chartAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (p : ) :
chartAt () p = (().toFiberBundleCore.localTriv (achart H p.proj)).trans ((chartAt H p.proj).prod )
theorem TangentBundle.chartAt_toPartialEquiv {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (p : ) :
(chartAt () p).toPartialEquiv = (().toFiberBundleCore.localTrivAsPartialEquiv (achart H p.proj)).trans ((chartAt H p.proj).prod )
theorem TangentBundle.trivializationAt_eq_localTriv {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (x : M) :
= ().toFiberBundleCore.localTriv (achart H x)
@[simp]
theorem TangentBundle.trivializationAt_source {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (x : M) :
().source = Bundle.TotalSpace.proj ⁻¹' (chartAt H x).source
@[simp]
theorem TangentBundle.trivializationAt_target {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] (x : M) :
().target = (chartAt H x).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).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 𝕜 (((chartAt H x).extend I) ((chartAt H z.proj).extend I).symm) () (((chartAt H z.proj).extend 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).1 = 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).source p.proj (chartAt H q.proj).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).target p.1 (chartAt H q.proj).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).1 = (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 : ) :
((chartAt () q).symm p).proj = (chartAt H q.proj).symm p.1
@[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) :
= ().coordChange (achart H b) (achart H b₀) b
@[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) :
Trivialization.symmL 𝕜 (trivializationAt E () b₀) b = ().coordChange (achart H b₀) (achart H b) b
@[simp]
theorem TangentBundle.coordChange_model_space {𝕜 : Type u_1} {F : Type u_8} [] (b : F) (b' : F) (x : F) :
().coordChange (achart F b) (achart F b') x = 1
@[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) [] [] :
().IsSmooth I
Equations
• =
instance TangentBundle.smoothVectorBundle {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (M : Type u_6) [] [] :
Equations
• =

## 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).toPartialEquiv = ().toPartialEquiv

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 : ) :
(chartAt () p).symm = ().symm
theorem tangentBundleCore_coordChange_model_space {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) (x : H) (x' : H) (z : H) :
().coordChange (achart H x) (achart H x') z =
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

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
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 = ().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.

Equations
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₀)).source) (hy : g x (chartAt H' (g x₀)).source) :
inTangentCoordinates I I' f g ϕ x₀ x = (().coordChange (achart H' (g x)) (achart H' (g x₀)) (g x)).comp ((ϕ x).comp (().coordChange (achart H (f x₀)) (achart H (f x)) (f x)))
instance instPathConnectedSpaceTangentSpaceReal {E : Type u_1} [] {H : Type u_2} [] {I : } {M : Type u_3} [] [] {x : M} :
Equations
• =