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 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 𝕜 (↑(PartialHomeomorph.extend (↑j) I) ∘ ↑(PartialEquiv.symm (PartialHomeomorph.extend (↑i) I)))
(Set.range ↑I))
(PartialEquiv.trans (PartialEquiv.symm (PartialHomeomorph.extend (↑i) I)) (PartialHomeomorph.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)
:
(tangentBundleCore I M).indexAt 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)
:
(tangentBundleCore I M).coordChange i j x = fderivWithin 𝕜 (↑(PartialHomeomorph.extend (↑j) I) ∘ ↑(PartialEquiv.symm (PartialHomeomorph.extend (↑i) I)))
(Set.range ↑I) (↑(PartialHomeomorph.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.
Equations
- One or more equations did not get rendered due to their size.
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))
:
(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 : M)
(x' : M)
(z : M)
:
(tangentBundleCore I M).coordChange (achart H x) (achart H x') z = fderivWithin 𝕜 (↑(extChartAt I x') ∘ ↑(PartialEquiv.symm (extChartAt I x))) (Set.range ↑I) (↑(extChartAt I x) z)
@[inline, reducible]
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 : M)
(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 : M}
{y : M}
{z : M}
:
tangentCoordChange I x y z = fderivWithin 𝕜 (↑(extChartAt I y) ∘ ↑(PartialEquiv.symm (extChartAt I x))) (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 : M}
{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 : M}
{x : M}
{y : M}
{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 : M}
{y : M}
{z : M}
(h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source)
:
HasFDerivWithinAt (↑(extChartAt I y) ∘ ↑(PartialEquiv.symm (extChartAt I x))) (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 : M)
(y : M)
:
ContinuousOn (tangentCoordChange I x y) ((extChartAt I x).source ∩ (extChartAt I y).source)
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.
Equations
- TangentSpace I _x = E
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)
Equations
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)
Equations
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}
:
Equations
- (_ : TopologicalAddGroup (TangentSpace I x)) = (_ : TopologicalAddGroup E)
@[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.
Equations
- TangentBundle I M = Bundle.TotalSpace E (TangentSpace I)
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)
Equations
- instInhabitedTangentSpace I x = { default := 0 }
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
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
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)
Equations
- (_ : VectorBundle 𝕜 E (TangentSpace I)) = (_ : VectorBundle 𝕜 E (VectorBundleCore.Fiber (tangentBundleCore I M)))
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 = PartialHomeomorph.trans
(FiberBundleCore.localTriv (VectorBundleCore.toFiberBundleCore (tangentBundleCore I M))
(achart H p.proj)).toPartialHomeomorph
(PartialHomeomorph.prod (chartAt H p.proj) (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 = PartialEquiv.trans
(FiberBundleCore.localTrivAsPartialEquiv (VectorBundleCore.toFiberBundleCore (tangentBundleCore I M))
(achart H p.proj))
(PartialEquiv.prod (chartAt H p.proj).toPartialEquiv (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 = 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).toPartialHomeomorph.toPartialEquiv.source = Bundle.TotalSpace.proj ⁻¹' (chartAt H x).toPartialEquiv.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).toPartialHomeomorph.toPartialEquiv.target = (chartAt H x).toPartialEquiv.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).toPartialEquiv.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 𝕜
(↑(PartialHomeomorph.extend (chartAt H x) I) ∘ ↑(PartialEquiv.symm (PartialHomeomorph.extend (chartAt H z.proj) I)))
(Set.range ↑I) (↑(PartialHomeomorph.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).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 : 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)
:
(↑(PartialHomeomorph.symm (chartAt (ModelProd H E) q)) p).proj = ↑(PartialHomeomorph.symm (chartAt H q.proj)) p.1
@[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 = (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₀ : M}
{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 : F)
(b' : F)
(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 : 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]
:
Equations
- (_ : VectorBundleCore.IsSmooth (tangentBundleCore I M) I) = (_ : VectorBundleCore.IsSmooth (tangentBundleCore I M) 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
Equations
- (_ : SmoothVectorBundle E (TangentSpace I) I) = (_ : SmoothVectorBundle E (VectorBundleCore.Fiber (tangentBundleCore I M)) 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).toPartialEquiv = Equiv.toPartialEquiv (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)
:
↑(PartialHomeomorph.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)
:
(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
Equations
- tangentBundleModelSpaceHomeomorph H I = let src := Bundle.TotalSpace.toProd H E; Homeomorph.mk src
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.
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₀ : N}
{x : N}
(hx : f x ∈ (chartAt H (f x₀)).toPartialEquiv.source)
(hy : g x ∈ (chartAt H' (g x₀)).toPartialEquiv.source)
:
inTangentCoordinates I I' f g ϕ x₀ x = ContinuousLinearMap.comp ((tangentBundleCore I' M').coordChange (achart H' (g x)) (achart H' (g x₀)) (g x))
(ContinuousLinearMap.comp (ϕ x) ((tangentBundleCore I M).coordChange (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}
:
Equations
- (_ : PathConnectedSpace (TangentSpace I x)) = (_ : PathConnectedSpace (TangentSpace I x))