Tangent bundles #
This file defines the tangent bundle as a smooth vector bundle.
Let M be a manifold with model I on (E, H). The tangent space TangentSpace I (x : M) has
already been defined as a type synonym for E, and the tangent bundle TangentBundle I M as an
abbrev of Bundle.TotalSpace E (TangentSpace I : M → Type _).
In this file, when M is smooth, we construct a smooth vector bundle structure
on TangentBundle I 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 and results #
tangentBundleCore I Mis the vector bundle core for the tangent bundle overM.When
Mis a smooth manifold with corners,TangentBundle I Mhas a smooth vector bundle structure overM. In particular, it is a topological space, a vector bundle, a fiber bundle, and a smooth manifold.
theorem
contDiffOn_fderiv_coord_change
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(i j : ↑(atlas H M))
:
ContDiffOn 𝕜 (↑⊤) (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (Set.range ↑I))
(((↑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.
def
tangentBundleCore
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_6)
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
:
VectorBundleCore 𝕜 M E ↑(atlas H M)
Let M be a smooth manifold with corners with model I on (E, H).
Then tangentBundleCore 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_coordChange
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_6)
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(i j : ↑(atlas H M))
(x : M)
:
(tangentBundleCore I M).coordChange i j x = fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (Set.range ↑I) (↑((↑i).extend I) x)
@[simp]
theorem
tangentBundleCore_indexAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_6)
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(x : M)
:
(tangentBundleCore I M).indexAt x = achart H x
@[simp]
theorem
tangentBundleCore_baseSet
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(i : ↑(atlas H M))
:
(tangentBundleCore I M).baseSet i = (↑i).source
theorem
tangentBundleCore_coordChange_achart
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(x x' z : M)
:
(tangentBundleCore I M).coordChange (achart H x) (achart H x') z = fderivWithin 𝕜 (↑(extChartAt I x') ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) z)
@[reducible, inline]
abbrev
tangentCoordChange
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(x y : M)
:
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
- tangentCoordChange I x y = (tangentBundleCore I M).coordChange (achart H x) (achart H y)
Instances For
theorem
tangentCoordChange_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{x y z : M}
:
tangentCoordChange I x y z = fderivWithin 𝕜 (↑(extChartAt I y) ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) z)
theorem
tangentCoordChange_self
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{x z : M}
{v : E}
(h : z ∈ (extChartAt I x).source)
:
(tangentCoordChange I x x z) v = v
theorem
tangentCoordChange_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{w x y z : M}
{v : E}
(h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source)
:
(tangentCoordChange I x y z) ((tangentCoordChange I w x z) v) = (tangentCoordChange I w y z) v
theorem
hasFDerivWithinAt_tangentCoordChange
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{x y z : M}
(h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source)
:
HasFDerivWithinAt (↑(extChartAt I y) ∘ ↑(extChartAt I x).symm) (tangentCoordChange I x y z) (Set.range ↑I)
(↑(extChartAt I x) z)
theorem
continuousOn_tangentCoordChange
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(x y : M)
:
ContinuousOn (tangentCoordChange I x y) ((extChartAt I x).source ∩ (extChartAt I y).source)
instance
instTopologicalSpaceTangentBundle
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
:
Equations
- instTopologicalSpaceTangentBundle = (tangentBundleCore I M).toTopologicalSpace
instance
TangentSpace.fiberBundle
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
:
FiberBundle E (TangentSpace I)
Equations
- TangentSpace.fiberBundle = (tangentBundleCore I M).fiberBundle
instance
TangentSpace.vectorBundle
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
:
VectorBundle 𝕜 E (TangentSpace I)
theorem
TangentBundle.chartAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(p : TangentBundle I M)
:
chartAt (ModelProd H E) p = ((tangentBundleCore I M).toFiberBundleCore.localTriv (achart H p.proj)).trans
((chartAt H p.proj).prod (PartialHomeomorph.refl E))
theorem
TangentBundle.chartAt_toPartialEquiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(p : TangentBundle I M)
:
(chartAt (ModelProd H E) p).toPartialEquiv = ((tangentBundleCore I M).toFiberBundleCore.localTrivAsPartialEquiv (achart H p.proj)).trans
((chartAt H p.proj).prod (PartialEquiv.refl E))
theorem
TangentBundle.trivializationAt_eq_localTriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(x : M)
:
trivializationAt E (TangentSpace I) x = (tangentBundleCore I M).toFiberBundleCore.localTriv (achart H x)
@[simp]
theorem
TangentBundle.trivializationAt_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(x : M)
:
(trivializationAt E (TangentSpace I) x).source = Bundle.TotalSpace.proj ⁻¹' (chartAt H x).source
@[simp]
theorem
TangentBundle.trivializationAt_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(x : M)
:
(trivializationAt E (TangentSpace I) x).target = (chartAt H x).source ×ˢ Set.univ
@[simp]
theorem
TangentBundle.trivializationAt_baseSet
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(x : M)
:
(trivializationAt E (TangentSpace I) x).baseSet = (chartAt H x).source
theorem
TangentBundle.trivializationAt_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(x : M)
(z : TangentBundle I M)
:
↑(trivializationAt E (TangentSpace I) x) z = (z.proj,
(fderivWithin 𝕜 (↑((chartAt H x).extend I) ∘ ↑((chartAt H z.proj).extend I).symm) (Set.range ↑I)
(↑((chartAt H z.proj).extend I) z.proj))
z.snd)
@[simp]
theorem
TangentBundle.trivializationAt_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(x : M)
(z : TangentBundle I M)
:
(↑(trivializationAt E (TangentSpace I) x) z).1 = z.proj
@[simp]
theorem
TangentBundle.mem_chart_source_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(p q : TangentBundle I M)
:
@[simp]
theorem
TangentBundle.mem_chart_target_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(p : H × E)
(q : TangentBundle I M)
:
@[simp]
theorem
TangentBundle.coe_chartAt_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(p q : TangentBundle I M)
:
@[simp]
theorem
TangentBundle.coe_chartAt_symm_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(p : H × E)
(q : TangentBundle I M)
:
@[simp]
theorem
TangentBundle.trivializationAt_continuousLinearMapAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{b₀ b : M}
(hb : b ∈ (trivializationAt E (TangentSpace I) b₀).baseSet)
:
Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) b₀) b = (tangentBundleCore I M).coordChange (achart H b) (achart H b₀) b
@[simp]
theorem
TangentBundle.trivializationAt_symmL
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{b₀ b : M}
(hb : b ∈ (trivializationAt E (TangentSpace I) b₀).baseSet)
:
Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) b₀) b = (tangentBundleCore I M).coordChange (achart H b₀) (achart H b) b
@[simp]
theorem
TangentBundle.coordChange_model_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(b b' x : F)
:
(tangentBundleCore (modelWithCornersSelf 𝕜 F) F).coordChange (achart F b) (achart F b') x = 1
@[simp]
theorem
TangentBundle.symmL_model_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(b b' : F)
:
Trivialization.symmL 𝕜 (trivializationAt F (TangentSpace (modelWithCornersSelf 𝕜 F)) b) b' = 1
@[simp]
theorem
TangentBundle.continuousLinearMapAt_model_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(b b' : F)
:
Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F (TangentSpace (modelWithCornersSelf 𝕜 F)) b) b' = 1
instance
tangentBundleCore.isSmooth
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
:
(tangentBundleCore I M).IsSmooth I
instance
TangentBundle.smoothVectorBundle
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
:
SmoothVectorBundle E (TangentSpace I) I
The tangent bundle to the model space #
@[simp]
theorem
trivializationAt_model_space_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
(p : TangentBundle I H)
(x : H)
:
↑(trivializationAt E (TangentSpace I) x) p = (p.proj, p.snd)
@[simp]
theorem
tangentBundle_model_space_chartAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
(p : TangentBundle I H)
:
(chartAt (ModelProd H E) p).toPartialEquiv = (Bundle.TotalSpace.toProd H E).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}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
(p : TangentBundle I H)
:
↑(chartAt (ModelProd H E) p) = ⇑(Bundle.TotalSpace.toProd H E)
@[simp]
theorem
tangentBundle_model_space_coe_chartAt_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
(p : TangentBundle I H)
:
↑(chartAt (ModelProd H E) p).symm = ⇑(Bundle.TotalSpace.toProd H E).symm
theorem
tangentBundleCore_coordChange_model_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
(x x' z : H)
:
(tangentBundleCore I H).coordChange (achart H x) (achart H x') z = ContinuousLinearMap.id 𝕜 E
def
tangentBundleModelSpaceHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
:
TangentBundle I H ≃ₜ ModelProd H E
The canonical identification between the tangent bundle to the model space and the product,
as a homeomorphism. For the diffeomorphism version, see tangentBundleModelSpaceDiffeomorph.
Equations
- tangentBundleModelSpaceHomeomorph I = { toEquiv := Bundle.TotalSpace.toProd H E, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
@[simp]
theorem
tangentBundleModelSpaceHomeomorph_coe
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
:
@[simp]
theorem
tangentBundleModelSpaceHomeomorph_coe_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
:
⇑(tangentBundleModelSpaceHomeomorph I).symm = ⇑(Bundle.TotalSpace.toProd H E).symm
theorem
contMDiff_tangentBundleModelSpaceHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : ℕ∞}
:
ContMDiff I.tangent (I.prod (modelWithCornersSelf 𝕜 E)) n ⇑(tangentBundleModelSpaceHomeomorph I)
theorem
contMDiff_tangentBundleModelSpaceHomeomorph_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : ℕ∞}
:
ContMDiff (I.prod (modelWithCornersSelf 𝕜 E)) I.tangent n ⇑(tangentBundleModelSpaceHomeomorph I).symm
theorem
contMDiff_snd_tangentBundle_modelSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(H : Type u_4)
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{n : ℕ∞}
:
ContMDiff I.tangent (modelWithCornersSelf 𝕜 E) n fun (p : TangentBundle I H) => p.snd
In the tangent bundle to the model space, the second projection is smooth.
theorem
contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{V : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x}
{n : ℕ∞}
{s : Set E}
{x : E}
:
ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent n
(fun (x : E) => { proj := x, snd := V x }) s x ↔ ContDiffWithinAt 𝕜 (↑n) V s x
A vector field on a vector space is smooth in the manifold sense iff it is smooth in the vector space sense
theorem
contMDiffAt_vectorSpace_iff_contDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{V : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x}
{n : ℕ∞}
{x : E}
:
ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent n (fun (x : E) => { proj := x, snd := V x })
x ↔ ContDiffAt 𝕜 (↑n) V x
A vector field on a vector space is smooth in the manifold sense iff it is smooth in the vector space sense
theorem
contMDiffOn_vectorSpace_iff_contDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{V : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x}
{n : ℕ∞}
{s : Set E}
:
ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent n (fun (x : E) => { proj := x, snd := V x })
s ↔ ContDiffOn 𝕜 (↑n) V s
A vector field on a vector space is smooth in the manifold sense iff it is smooth in the vector space sense
theorem
contMDiff_vectorSpace_iff_contDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{V : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x}
{n : ℕ∞}
:
(ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent n fun (x : E) => { proj := x, snd := V x }) ↔ ContDiff 𝕜 (↑n) V
A vector field on a vector space is smooth in the manifold sense iff it is smooth in the vector space sense
theorem
inCoordinates_tangent_bundle_core_model_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
(x₀ x : H)
(y₀ y : H')
(ϕ : E →L[𝕜] E')
:
ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ
The map inCoordinates for the tangent bundle is trivial on the model spaces
def
inTangentCoordinates
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_5}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
[SmoothManifoldWithCorners I' M']
{N : Type u_9}
(f : N → M)
(g : N → M')
(ϕ : 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, 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
- inTangentCoordinates I I' f g ϕ x₀ x = ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (f x₀) (f x) (g x₀) (g x) (ϕ x)
Instances For
theorem
inTangentCoordinates_model_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{N : Type u_9}
(f : N → H)
(g : N → H')
(ϕ : N → E →L[𝕜] E')
(x₀ : N)
:
inTangentCoordinates I I' f g ϕ x₀ = ϕ
theorem
inTangentCoordinates_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
[SmoothManifoldWithCorners I' M']
{N : Type u_9}
(f : N → M)
(g : N → M')
(ϕ : N → E →L[𝕜] E')
{x₀ 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 = ((tangentBundleCore I' M').coordChange (achart H' (g x)) (achart H' (g x₀)) (g x)).comp
((ϕ x).comp ((tangentBundleCore I M).coordChange (achart H (f x₀)) (achart H (f x)) (f x)))
To write a linear map between tangent spaces in coordinates amounts to precomposing and
postcomposing it with suitable coordinate changes. For a concrete version expressing the
change of coordinates as derivatives of extended charts,
see inTangentCoordinates_eq_mfderiv_comp.