tangentMap_chart
theorem tangentMap_chart :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
{p q : TangentBundle I M},
q.proj ∈ (chartAt H p.proj).source →
tangentMap I I (↑(chartAt H p.proj)) q = (Bundle.TotalSpace.toProd H E).symm (↑(chartAt (ModelProd H E) p) q)
This theorem states that for a given nontrivially normed field `𝕜`, a normed add commutative group `E` and a topological space `H` with a model with corners `I`, a charted space `H` over a topological space `M` which is also a smooth manifold with corners, and two points `p` and `q` in the tangent bundle of `I` and `M`; if the projection of `q` is in the source of the chart at the projection of `p`, then the derivative of the chart at `p` is equal to the reverse of the function that converts the total space of the bundle to the product space `H × E`, applied to the chart at `p` and `q` in the model product space `H × E`. In terms of mathematics, the theorem states that the derivative of the chart at a base point is equivalent to the chart of the tangent bundle, after identifying the tangent bundle of the model space with the product space.
More concisely: Given a smooth manifold with corners `M` over a topological space `M` with a charted space `H` over it, a nontrivially normed field `𝕜`, a normed add commutative group `E`, and their respective tangent bundles `TM` and `TE`; for any charts `c` of `H` and `d` of `M` at points `p` and `q` in `TM` and `TM` respectively, if `q` is in the image of `c` under the projection of `TM` and `p` is in the domain of `d`, then the derivative of `c` at `p` equals the reverse of the chart `d` evaluated at `q` combined with the product map from `H × E` to `TM` and `TE`.
|
tangentMap_chart_symm
theorem tangentMap_chart_symm :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
{p : TangentBundle I M} {q : TangentBundle I H},
q.proj ∈ (chartAt H p.proj).target →
tangentMap I I (↑(chartAt H p.proj).symm) q =
↑(chartAt (ModelProd H E) p).symm ((Bundle.TotalSpace.toProd H E) q)
This theorem states that, given a non-trivially normed field `𝕜`, a NormedAddCommGroup `E` over `𝕜`, a topological space `H`, a model with corners `I` between `𝕜`, `E`, and `H`, a topological space `M` with a charted space structure over `H` and a smooth manifold structure with corners `I`, and points `p` in the tangent bundle over `I` and `M`, `q` in the tangent bundle over `I` and `H` such that the projection of `q` is in the target of the chart at `p.proj` in `H`, the derivative of the inverse of the chart at `p.proj` applied to `q` is equal to the inverse of the chart at `p` in the product space of `H` and `E`, composed with the identification between the tangent bundle of the model space and the product space, applied to `q`. This theorem essentially describes a relationship between the derivative of the inverse of a chart in a manifold and the inverse of a chart in the tangent bundle of the manifold.
More concisely: Given a non-trivially normed field `𝕜`, a NormedAddCommGroup `E` over `𝕜`, a charted smooth manifold `M` with corners `I` between `𝕜`, `E`, and `H`, and points `p` in the tangent bundle of `M` over `I` and `q` in the tangent bundle of the model space over `I` and `H`, if the projection of `q` is in the target of the chart at `p.proj` in `H`, then the derivative of the inverse of the chart at `p.proj` and the inverse of the chart at `p` in the product space of `H` and `E`, composed with the identification between the tangent bundle and the product space, are equal at `q`.
|