Tangent-bundle trivializations, coordinate changes on T(TM), and open submanifolds

The canonical tangent-bundle trivialization at a point x is built from the chart at x, so on the fibre over x itself it is the identity. This file records that fact in both directions, and notes that reading a tangent vector through the preferred trivializations of two charts is the tangent coordinate change between them, which is C^n in the base point.

It then computes the coordinate changes of the tangent bundle of the tangent bundle: a tangent vector (u, w) to TM at a point with x-coordinates u, read in the tangent-bundle chart centred at the zero vector over x₀, has base component the tangent coordinate change of u, and fibre component the product-rule sum of the derivative of that coordinate change in the base point and the coordinate change applied to w. This is the transformation law obeyed by a second-order vector field on TM, such as a geodesic spray, when it is carried between tangent-bundle charts.

It then identifies the tangent spaces of an open submanifold with those of its ambient manifold and shows that, near each point, the inverse tangent-bundle trivializations agree under that identification.

Finally it identifies the tangent space of a product manifold with the product of the tangent spaces of the factors, and shows that under this identification tangent coordinate changes and inverse tangent-bundle trivializations act componentwise.

Main results

• TauCeti.Manifold.continuousLinearMapAt_trivializationAt_self and TauCeti.Manifold.symmL_trivializationAt_self: the canonical trivialization at x and its inverse act as the identity on the fibre over x.
• TauCeti.Manifold.localFrame_trivializationAt_self: consequently its local frame at x is the chosen basis of the model space.
• TauCeti.Manifold.inverse_mfderiv_extChartAt: the inverse of the differential of an extended chart is the inverse of the canonical tangent-bundle trivialization at its centre.
• TauCeti.Manifold.contDiffOn_tangentCoordChange: the tangent coordinate change between the charts at two points is C^n on the overlap of their sources, read in the chart at the first point.
• TauCeti.Manifold.contMDiffAt_tangentCoordChange: that coordinate change is C^n at the base point of its first chart, as a map of manifolds into the linear endomorphisms of the model space.
• TauCeti.Manifold.tangentCoordChange_tangent_apply: the coordinate-change formula on the tangent bundle of the tangent bundle.
• TauCeti.Manifold.continuousLinearMapAt_symmL_coordChange: reading a tangent vector through the preferred trivializations of two charts is the tangent coordinate change between them.
• TauCeti.Manifold.tangentCoordChange_toMatrix: in a finite basis, this coordinate change is the change-of-basis matrix between the corresponding chart-local frames.
• TauCeti.Manifold.tangentSpaceOpenEquiv: the canonical continuous linear equivalence between the tangent space of an open submanifold and the ambient tangent space.
• TauCeti.Manifold.mfderiv_subtype_val: the differential of the inclusion is the canonical tangent-space equivalence.
• TauCeti.Manifold.tangentMap_subtype_val: the tangent map of the inclusion under this equivalence.
• TauCeti.Manifold.tangentSpaceOpenEquiv_mfderiv_apply: under this equivalence, the differential of a map between open submanifolds is that of any ambient map it restricts.
• TauCeti.Manifold.instT2SpaceTangentBundleModelSpace: a model space has a Hausdorff tangent bundle. It is an instance in the TauCeti scope, for model spaces H whose Hausdorffness is not already an instance; over a Hausdorff manifold the tangent bundle is Hausdorff by the general instance TauCeti.FiberBundle.t2Space_totalSpace.
• TauCeti.Manifold.eventually_tangentSpaceOpenEquiv_symmL_trivializationAt_eq: near a point, the inverse tangent-bundle trivializations agree through this equivalence.
• TauCeti.Manifold.tangentSpaceProdEquiv: the canonical continuous linear equivalence between the tangent space of a product and the product of the tangent spaces.
• TauCeti.Manifold.tangentCoordChange_prod: the tangent coordinate change of a product is the product of the tangent coordinate changes of the factors.
• TauCeti.Manifold.tangentSpaceProdEquiv_symmL_trivializationAt: the inverse tangent-bundle trivialization of a product is the product of those of the factors.

@[simp]

theorem TauCeti.Manifold.continuousLinearMapAt_trivializationAt_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (x : M) (v : TangentSpace I x) : (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x) x) v = v

Read in the canonical trivialization at x, a tangent vector at x itself is its own coordinate vector: the trivialization is built from the chart at x, whose transition function with itself has derivative the identity.

@[simp]

theorem TauCeti.Manifold.symmL_trivializationAt_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (x : M) (v : E) : (Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x) x) v = v

The inverse form of TauCeti.Manifold.continuousLinearMapAt_trivializationAt_self: over its own base point, the inverse of the canonical trivialization is the identity.

theorem TauCeti.Manifold.inverse_mfderiv_extChartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (x₀ : M) {x : M} (hx : x ∈ (extChartAt I x₀).source) : (mfderiv% ↑(extChartAt I x₀) x).inverse = Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x₀) x

The differential of the extended chart at x₀, at a point x of its source, is inverted by the inverse of the canonical tangent-bundle trivialization at x₀. This is the inverse form of TangentBundle.symmL_trivializationAt.

@[simp]

theorem TauCeti.Manifold.TangentBundle.coe_chartAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {p q : TangentBundle I M} : (↑(chartAt (ModelProd H E) q) p).2 = (tangentCoordChange I p.proj q.proj p.proj) p.snd

The second component of the chart of a tangent bundle at q, read at a point with base point in the chart source. Together with TangentBundle.coe_chartAt_fst this describes the tangent-bundle charts completely.

theorem TauCeti.Manifold.contDiffOn_tangentCoordChange {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (x y : M) : ContDiffOn 𝕜 n (fun (a : E) => tangentCoordChange I x y (↑(extChartAt I x).symm a)) ((extChartAt I x).symm.trans (extChartAt I y)).source

The tangent coordinate change between the charts at x and y is C^n on the overlap of the two chart sources, read in the chart at x. This is Mathlib's contDiffOn_fderiv_coord_change for the preferred charts at two points.

theorem TauCeti.Manifold.contMDiffAt_tangentCoordChange {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] {x y : M} (hy : x ∈ (extChartAt I y).source) : ContMDiffAt I (modelWithCornersSelf 𝕜 (E →L[𝕜] E)) n (tangentCoordChange I x y) x

The tangent coordinate change between the charts at x and y is C^n at x, as a map of manifolds into the continuous linear endomorphisms of the model space.

Coordinate changes on the tangent of the tangent bundle

theorem TauCeti.Manifold.tangentCoordChange_tangent_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {x x₀ : M} (hx₀ : x ∈ (extChartAt I x₀).source) (u : TangentSpace I x) (w : E) : have v := (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x) x) u; (tangentCoordChange I.tangent ⟨x, u⟩ ⟨x₀, 0⟩ ⟨x, u⟩) (v, w) = ((tangentCoordChange I x x₀ x) v, ((d% fun (y : M) => (tangentCoordChange I x x₀ y) v) x) u + (tangentCoordChange I x x₀ x) w)

The tangent coordinate change on TM sends the tangent vector (v, w) at u ∈ TₓM to the derivative of the base coordinate change together with the product-rule expression for the fibre coordinate, where v is the coordinate of u in the preferred trivialization at x. The target chart is centred at the zero vector over x₀.

theorem TauCeti.Manifold.continuousLinearMapAt_symmL_coordChange {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {x x₀ y : M} (hyx : y ∈ (chartAt H x).source) (hyx₀ : y ∈ (chartAt H x₀).source) (u : E) : (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x₀) y) ((Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x) y) u) = (tangentCoordChange I x x₀ y) u

The reading map of the preferred trivialization centred at x₀ sends the tangent vector at y whose x-coordinates are u to its x₀-coordinates.

theorem TauCeti.Manifold.tangentCoordChange_toMatrix {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (α β : M) (b : Module.Basis ι 𝕜 E) {x : M} (hα : x ∈ (trivializationAt E (TangentSpace I) α).baseSet) (hβ : x ∈ (trivializationAt E (TangentSpace I) β).baseSet) : (LinearMap.toMatrix b b) ↑(tangentCoordChange I α β x) = ((trivializationAt E (TangentSpace I) β).basisAt b hβ).toMatrix ⇑((trivializationAt E (TangentSpace I) α).basisAt b hα)

The matrix of a tangent coordinate change in a finite basis of the model space is the change-of-basis matrix between the corresponding chart-local frames.

@[simp]

theorem TauCeti.Manifold.localFrame_trivializationAt_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {ι : Type u_5} (b : Module.Basis ι 𝕜 E) (x : M) (i : ι) : (trivializationAt E (TangentSpace I) x).localFrame b i x = b i

Over its own base point, the local frame attached to the canonical trivialization at x is the given basis of the model space.

noncomputable def TauCeti.Manifold.tangentSpaceOpenEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} (x : ↥U) : TangentSpace I x ≃L[𝕜] TangentSpace I ↑x

The canonical identification between the tangent space of an open submanifold and the ambient tangent space. Both are Mathlib's type synonym for the common model vector space.

This is deliberately a named equivalence rather than ContinuousLinearEquiv.refl 𝕜 E: because TangentSpace is not reducible, a statement phrased with refl is type-correct only after unfolding it, so rw and simp fail on such statements. Mathlib introduces NormedSpace.fromTangentSpace for the analogous identification for the same reason.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Manifold.tangentSpaceOpenEquiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} (x : ↥U) (v : TangentSpace I x) : (tangentSpaceOpenEquiv x) v = v

@[simp]

theorem TauCeti.Manifold.tangentSpaceOpenEquiv_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} (x : ↥U) (v : TangentSpace I ↑x) : (tangentSpaceOpenEquiv x).symm v = v

@[simp]

theorem TauCeti.Manifold.mfderiv_subtype_val {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} (x : ↥U) : mfderiv% Subtype.val x = ↑(tangentSpaceOpenEquiv x)

The differential of the inclusion of an open submanifold is the canonical tangent-space identification.

@[simp]

theorem TauCeti.Manifold.tangentMap_subtype_val {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} (p : TangentBundle I ↥U) : tangentMap I I Subtype.val p = ⟨↑p.proj, (tangentSpaceOpenEquiv p.proj) p.snd⟩

The tangent map of an open submanifold's inclusion identifies its tangent vectors with ambient tangent vectors through tangentSpaceOpenEquiv.

theorem TauCeti.Manifold.tangentSpaceOpenEquiv_mfderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {U : TopologicalSpace.Opens M} {V : TopologicalSpace.Opens M'} {f : ↥U → ↥V} {A : M → M'} {x : ↥U} (hf : MDiffAt f x) (hA : MDiffAt A ↑x) (hcomp : Subtype.val ∘ f = A ∘ Subtype.val) (v : TangentSpace I x) : (tangentSpaceOpenEquiv (f x)) ((mfderiv% f x) v) = (mfderiv% A ↑x) ((tangentSpaceOpenEquiv x) v)

If a differentiable map f between open submanifolds is the restriction of a map A of the ambient manifolds, then under the canonical tangent-space identifications the differential of f at x is the differential of A at x.

theorem TauCeti.Manifold.instT2SpaceTangentBundleModelSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} : T2Space (TangentBundle I H)

The tangent bundle of a model space is Hausdorff.

theorem TauCeti.Manifold.eventually_tangentSpaceOpenEquiv_symmL_trivializationAt_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {U : TopologicalSpace.Opens M} (x : ↥U) : ∀ᶠ (y : ↥U) in nhds x, ∀ (z : E), (tangentSpaceOpenEquiv y) ((Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x) y) z) = (Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) ↑x) ↑y) z

Near a point of an open submanifold, its inverse tangent-bundle trivialization agrees with the ambient inverse trivialization under the canonical tangent-space identification.

noncomputable def TauCeti.Manifold.tangentSpaceProdEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (p : M × N) : TangentSpace (I.prod J) p ≃L[𝕜] TangentSpace I p.1 × TangentSpace J p.2

The canonical identification of the tangent space of a product manifold with the product of the tangent spaces of the factors. Both are Mathlib's type synonym for the product of the model vector spaces; as for tangentSpaceOpenEquiv, the identification is named so that statements using it are type-correct without unfolding TangentSpace.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Manifold.tangentSpaceProdEquiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (p : M × N) (v : TangentSpace (I.prod J) p) : (tangentSpaceProdEquiv p) v = v

@[simp]

theorem TauCeti.Manifold.tangentSpaceProdEquiv_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (p : M × N) (v : TangentSpace I p.1 × TangentSpace J p.2) : (tangentSpaceProdEquiv p).symm v = v

theorem TauCeti.Manifold.tangentCoordChange_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I 1 M] [IsManifold J 1 N] {p q z : M × N} (hz : z ∈ (extChartAt (I.prod J) p).source ∩ (extChartAt (I.prod J) q).source) : tangentCoordChange (I.prod J) p q z = (tangentCoordChange I p.1 q.1 z.1).prodMap (tangentCoordChange J p.2 q.2 z.2)

On the common domain of two product charts, the tangent coordinate change of a product manifold is the product of the tangent coordinate changes of the factors.

theorem TauCeti.Manifold.tangentSpaceProdEquiv_symmL_trivializationAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I 1 M] [IsManifold J 1 N] {p q : M × N} (hq : q ∈ (chartAt (ModelProd H G) p).source) (v : E × F) : (tangentSpaceProdEquiv q) ((Bundle.Trivialization.symmL 𝕜 (trivializationAt (E × F) (TangentSpace (I.prod J)) p) q) v) = ((Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) p.1) q.1) v.1, (Bundle.Trivialization.symmL 𝕜 (trivializationAt F (TangentSpace J) p.2) q.2) v.2)

Over the domain of the chart at p, the inverse of the canonical tangent-bundle trivialization of a product manifold at p is the product of the inverse trivializations of the factors.