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 xis the fiber of the tangent bundle atx : M, which is defined to beE. -
TangentBundle I Mis the total space ofTangentSpace I M, proven to be a smooth vector bundle.
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 : ↑(atlas H M))
(j : ↑(atlas H M))
:
ContDiffOn 𝕜 ⊤
(fderivWithin 𝕜 (↑(LocalHomeomorph.extend (↑j) I) ∘ ↑(LocalEquiv.symm (LocalHomeomorph.extend (↑i) I)))
(Set.range ↑I))
(LocalEquiv.trans (LocalEquiv.symm (LocalHomeomorph.extend (↑i) I)) (LocalHomeomorph.extend (↑j) I)).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}
[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)
:
VectorBundleCore.indexAt (tangentBundleCore I M) x = achart H x
@[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 : ↑(atlas H M))
(j : ↑(atlas H M))
(x : M)
:
VectorBundleCore.coordChange (tangentBundleCore I M) i j x = fderivWithin 𝕜 (↑(LocalHomeomorph.extend (↑j) I) ∘ ↑(LocalEquiv.symm (LocalHomeomorph.extend (↑i) I))) (Set.range ↑I)
(↑(LocalHomeomorph.extend (↑i) I) x)
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 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}
[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))
:
VectorBundleCore.baseSet (tangentBundleCore I M) 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 : M)
(x' : M)
(z : M)
:
VectorBundleCore.coordChange (tangentBundleCore I M) (achart H x) (achart H x') z = fderivWithin 𝕜 (↑(extChartAt I x') ∘ ↑(LocalEquiv.symm (extChartAt I x))) (Set.range ↑I) (↑(extChartAt I x) z)
def
TangentSpace
{𝕜 : Type u_10}
[NontriviallyNormedField 𝕜]
{E : Type u_9}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_11}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_12}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
(_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}
[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}
:
TopologicalSpace (TangentSpace I x)
instance
instAddCommGroupTangentSpace
{𝕜 : 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}
:
AddCommGroup (TangentSpace I x)
instance
instTopologicalAddGroupTangentSpaceInstTopologicalSpaceTangentSpaceToAddGroupInstAddCommGroupTangentSpace
{𝕜 : 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}
:
@[reducible]
def
TangentBundle
{𝕜 : 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]
:
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
instModuleTangentSpaceToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToAddCommMonoidInstAddCommGroupTangentSpace
{𝕜 : 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)
:
Module 𝕜 (TangentSpace I x)
instance
instInhabitedTangentSpace
{𝕜 : 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)
:
Inhabited (TangentSpace I x)
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]
:
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)
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 = LocalHomeomorph.trans
(FiberBundleCore.localTriv (VectorBundleCore.toFiberBundleCore (tangentBundleCore I M))
(achart H p.proj)).toLocalHomeomorph
(LocalHomeomorph.prod (chartAt H p.proj) (LocalHomeomorph.refl E))
theorem
TangentBundle.chartAt_toLocalEquiv
{𝕜 : 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).toLocalEquiv = LocalEquiv.trans
(FiberBundleCore.localTrivAsLocalEquiv (VectorBundleCore.toFiberBundleCore (tangentBundleCore I M))
(achart H p.proj))
(LocalEquiv.prod (chartAt H p.proj).toLocalEquiv (LocalEquiv.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 = FiberBundleCore.localTriv (VectorBundleCore.toFiberBundleCore (tangentBundleCore I M)) (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).toLocalHomeomorph.toLocalEquiv.source = Bundle.TotalSpace.proj ⁻¹' (chartAt H x).toLocalEquiv.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).toLocalHomeomorph.toLocalEquiv.target = (chartAt H x).toLocalEquiv.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).toLocalEquiv.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 𝕜
(↑(LocalHomeomorph.extend (chartAt H x) I) ∘ ↑(LocalEquiv.symm (LocalHomeomorph.extend (chartAt H z.proj) I)))
(Set.range ↑I) (↑(LocalHomeomorph.extend (chartAt H z.proj) 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).fst = 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 : TangentBundle I M)
(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 : TangentBundle I M)
(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)
:
(↑(LocalHomeomorph.symm (chartAt (ModelProd H E) q)) p).proj = ↑(LocalHomeomorph.symm (chartAt H q.proj)) p.fst
@[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₀ : M}
{b : M}
(hb : b ∈ (trivializationAt E (TangentSpace I) b₀).baseSet)
:
Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) b₀) b = VectorBundleCore.coordChange (tangentBundleCore I M) (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₀ : M}
{b : M}
(hb : b ∈ (trivializationAt E (TangentSpace I) b₀).baseSet)
:
Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) b₀) b = VectorBundleCore.coordChange (tangentBundleCore I M) (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 : F)
(b' : F)
(x : F)
:
VectorBundleCore.coordChange (tangentBundleCore (modelWithCornersSelf 𝕜 F) F) (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 : F)
(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 : F)
(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]
:
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
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).toLocalEquiv = Equiv.toLocalEquiv (Bundle.TotalSpace.toProd H E)
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)
:
↑(LocalHomeomorph.symm (chartAt (ModelProd H E) p)) = ↑(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 : H)
(x' : H)
(z : H)
:
VectorBundleCore.coordChange (tangentBundleCore I H) (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
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)
:
↑(tangentBundleModelSpaceHomeomorph H I) = ↑(Bundle.TotalSpace.toProd H E)
@[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)
:
↑(Homeomorph.symm (tangentBundleModelSpaceHomeomorph H I)) = ↑(Bundle.TotalSpace.toProd H E).symm
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₀ : H)
(x : H)
(y₀ : H')
(y : H')
(ϕ : E →L[𝕜] E')
:
ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ
The map in_coordinates 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.
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₀ : 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 (tangentBundleCore I' M') (achart H' (g x)) (achart H' (g x₀)) (g x))
(ContinuousLinearMap.comp (ϕ x)
(VectorBundleCore.coordChange (tangentBundleCore I M) (achart H (f x₀)) (achart H (f x)) (f x)))
instance
instPathConnectedSpaceTangentSpaceRealToNontriviallyNormedFieldDenselyNormedFieldInstTopologicalSpaceTangentSpace
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{x : M}
: