Tangent bundles #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 vector_bundle_core construction indexed by the charts of M with fibers E.
Given two charts i, j : local_homeomorph 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 tangent_bundle with fibers tangent_space.
Main definitions #
-
tangent_space I M xis the fiber of the tangent bundle atx : M, which is defined to beE. -
tangent_bundle I Mis the total space oftangent_space I M, proven to be a smooth vector bundle.
theorem
cont_diff_on_fderiv_coord_change
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_6}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(i j : ↥(charted_space.atlas H M)) :
Auxiliary lemma for tangent spaces: the derivative of a coordinate change between two charts is smooth on its source.
@[simp]
theorem
tangent_bundle_core_base_set
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(i : ↥(charted_space.atlas H M)) :
(tangent_bundle_core I M).base_set i = i.val.to_local_equiv.source
noncomputable
def
tangent_bundle_core
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
vector_bundle_core 𝕜 M E ↥(charted_space.atlas H M)
Let M be a smooth manifold with corners with model I on (E, H).
Then vector_bundle_core 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
- tangent_bundle_core I M = {base_set := λ (i : ↥(charted_space.atlas H M)), i.val.to_local_equiv.source, is_open_base_set := _, index_at := achart H _inst_9, mem_base_set_at := _, coord_change := λ (i j : ↥(charted_space.atlas H M)) (x : M), fderiv_within 𝕜 (⇑(j.val.extend I) ∘ ⇑((i.val.extend I).symm)) (set.range ⇑I) (⇑(i.val.extend I) x), coord_change_self := _, continuous_on_coord_change := _, coord_change_comp := _}
Instances for tangent_bundle_core
@[simp]
theorem
tangent_bundle_core_coord_change
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(i j : ↥(charted_space.atlas H M))
(x : M) :
@[simp]
theorem
tangent_bundle_core_index_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
(tangent_bundle_core I M).index_at x = achart H x
theorem
tangent_bundle_core_coord_change_achart
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_6}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x x' z : M) :
(tangent_bundle_core I M).coord_change (achart H x) (achart H x') z = fderiv_within 𝕜 (⇑(ext_chart_at I x') ∘ ⇑((ext_chart_at I x).symm)) (set.range ⇑I) (⇑(ext_chart_at I x) z)
@[protected, instance]
def
tangent_space.topological_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_6}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
@[protected, instance]
def
tangent_space.topological_add_group
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_6}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
@[nolint]
def
tangent_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_6}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
Type u_2
The tangent space at a point of the manifold M. It is just E. We could use instead
(tangent_bundle_core I M).to_topological_vector_bundle_core.fiber x, but we use E to help the
kernel.
Equations
- tangent_space I x = E
Instances for tangent_space
- tangent_space.topological_space
- tangent_space.add_comm_group
- tangent_space.topological_add_group
- tangent_space.module
- tangent_space.inhabited
- tangent_space.has_continuous_add
- tangent_space.fiber_bundle
- tangent_space.vector_bundle
- tangent_bundle.smooth_vector_bundle
- tangent_space.path_connected_space
@[protected, instance]
def
tangent_space.add_comm_group
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_6}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
add_comm_group (tangent_space I x)
@[nolint, reducible]
def
tangent_bundle
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
Type (max u_6 u_2)
The tangent bundle to a smooth manifold, as a Sigma type. Defined in terms of
bundle.total_space to be able to put a suitable topology on it.
Equations
- tangent_bundle I M = bundle.total_space E (tangent_space I)
@[protected, instance]
def
tangent_space.module
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_6}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
module 𝕜 (tangent_space I x)
Equations
@[protected, instance]
def
tangent_space.inhabited
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_6}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
inhabited (tangent_space I x)
Equations
- tangent_space.inhabited I x = {default := 0}
@[protected, instance]
def
tangent_space.has_continuous_add
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_6}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
{x : M} :
@[protected, instance]
noncomputable
def
tangent_bundle.topological_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
Equations
@[protected, instance]
noncomputable
def
tangent_space.fiber_bundle
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
fiber_bundle E (tangent_space I)
Equations
@[protected, instance]
def
tangent_space.vector_bundle
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
vector_bundle 𝕜 E (tangent_space I)
@[protected]
theorem
tangent_bundle.chart_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(p : tangent_bundle I M) :
charted_space.chart_at (model_prod H E) p = ((tangent_bundle_core I M).to_fiber_bundle_core.local_triv (achart H p.proj)).to_local_homeomorph.trans ((charted_space.chart_at H p.proj).prod (local_homeomorph.refl E))
theorem
tangent_bundle.chart_at_to_local_equiv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(p : tangent_bundle I M) :
(charted_space.chart_at (model_prod H E) p).to_local_equiv = ((tangent_bundle_core I M).to_fiber_bundle_core.local_triv_as_local_equiv (achart H p.proj)).trans ((charted_space.chart_at H p.proj).to_local_equiv.prod (local_equiv.refl E))
theorem
tangent_bundle.trivialization_at_eq_local_triv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
fiber_bundle.trivialization_at E (tangent_space I) x = (tangent_bundle_core I M).to_fiber_bundle_core.local_triv (achart H x)
@[simp]
theorem
tangent_bundle.trivialization_at_source
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
@[simp]
theorem
tangent_bundle.trivialization_at_target
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
@[simp]
theorem
tangent_bundle.trivialization_at_base_set
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M) :
theorem
tangent_bundle.trivialization_at_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M)
(z : tangent_bundle I M) :
⇑(fiber_bundle.trivialization_at E (tangent_space I) x) z = (z.proj, ⇑(fderiv_within 𝕜 (⇑((charted_space.chart_at H x).extend I) ∘ ⇑(((charted_space.chart_at H z.proj).extend I).symm)) (set.range ⇑I) (⇑((charted_space.chart_at H z.proj).extend I) z.proj)) z.snd)
@[simp]
theorem
tangent_bundle.trivialization_at_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(x : M)
(z : tangent_bundle I M) :
(⇑(fiber_bundle.trivialization_at E (tangent_space I) x) z).fst = z.proj
@[simp]
theorem
tangent_bundle.mem_chart_source_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(p q : tangent_bundle I M) :
p ∈ (charted_space.chart_at (model_prod H E) q).to_local_equiv.source ↔ p.proj ∈ (charted_space.chart_at H q.proj).to_local_equiv.source
@[simp]
theorem
tangent_bundle.mem_chart_target_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(p : H × E)
(q : tangent_bundle I M) :
p ∈ (charted_space.chart_at (model_prod H E) q).to_local_equiv.target ↔ p.fst ∈ (charted_space.chart_at H q.proj).to_local_equiv.target
@[simp]
theorem
tangent_bundle.coe_chart_at_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(p q : tangent_bundle I M) :
(⇑(charted_space.chart_at (model_prod H E) q) p).fst = ⇑(charted_space.chart_at H q.proj) p.proj
@[simp]
theorem
tangent_bundle.coe_chart_at_symm_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
(p : H × E)
(q : tangent_bundle I M) :
(⇑((charted_space.chart_at (model_prod H E) q).symm) p).proj = ⇑((charted_space.chart_at H q.proj).symm) p.fst
@[simp]
theorem
tangent_bundle.trivialization_at_continuous_linear_map_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
{b₀ b : M}
(hb : b ∈ (fiber_bundle.trivialization_at E (tangent_space I) b₀).base_set) :
trivialization.continuous_linear_map_at 𝕜 (fiber_bundle.trivialization_at E (tangent_space I) b₀) b = (tangent_bundle_core I M).coord_change (achart H b) (achart H b₀) b
@[simp]
theorem
tangent_bundle.trivialization_at_symmL
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
{b₀ b : M}
(hb : b ∈ (fiber_bundle.trivialization_at E (tangent_space I) b₀).base_set) :
trivialization.symmL 𝕜 (fiber_bundle.trivialization_at E (tangent_space I) b₀) b = (tangent_bundle_core I M).coord_change (achart H b₀) (achart H b) b
@[simp]
theorem
tangent_bundle.coord_change_model_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{F : Type u_8}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(b b' x : F) :
(tangent_bundle_core (model_with_corners_self 𝕜 F) F).coord_change (achart F b) (achart F b') x = 1
@[simp]
theorem
tangent_bundle.symmL_model_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{F : Type u_8}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(b b' : F) :
trivialization.symmL 𝕜 (fiber_bundle.trivialization_at F (tangent_space (model_with_corners_self 𝕜 F)) b) b' = 1
@[simp]
theorem
tangent_bundle.continuous_linear_map_at_model_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{F : Type u_8}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(b b' : F) :
@[protected, instance]
def
tangent_bundle_core.is_smooth
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
(tangent_bundle_core I M).is_smooth I
@[protected, instance]
def
tangent_bundle.smooth_vector_bundle
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_6)
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M] :
smooth_vector_bundle E (tangent_space I) I
The tangent bundle to the model space #
@[simp]
theorem
tangent_bundle_model_space_chart_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(p : tangent_bundle I H) :
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. equiv.sigma_equiv_prod.
@[simp]
theorem
tangent_bundle_model_space_coe_chart_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(p : tangent_bundle I H) :
⇑(charted_space.chart_at (model_prod H E) p) = ⇑(bundle.total_space.to_prod H E)
@[simp]
theorem
tangent_bundle_model_space_coe_chart_at_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(p : tangent_bundle I H) :
⇑((charted_space.chart_at (model_prod H E) p).symm) = ⇑((bundle.total_space.to_prod H E).symm)
theorem
tangent_bundle_core_coord_change_model_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(x x' z : H) :
(tangent_bundle_core I H).coord_change (achart H x) (achart H x') z = continuous_linear_map.id 𝕜 E
def
tangent_bundle_model_space_homeomorph
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
(H : Type u_4)
[topological_space H]
(I : model_with_corners 𝕜 E H) :
tangent_bundle I H ≃ₜ model_prod H E
The canonical identification between the tangent bundle to the model space and the product, as a homeomorphism
Equations
- tangent_bundle_model_space_homeomorph H I = {to_equiv := {to_fun := (bundle.total_space.to_prod H E).to_fun, inv_fun := (bundle.total_space.to_prod H E).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
tangent_bundle_model_space_homeomorph_coe
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
(H : Type u_4)
[topological_space H]
(I : model_with_corners 𝕜 E H) :
@[simp]
theorem
tangent_bundle_model_space_homeomorph_coe_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
(H : Type u_4)
[topological_space H]
(I : model_with_corners 𝕜 E H) :
⇑((tangent_bundle_model_space_homeomorph H I).symm) = ⇑((bundle.total_space.to_prod H E).symm)
theorem
in_coordinates_tangent_bundle_core_model_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{H' : Type u_5}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
(x₀ x : H)
(y₀ y : H')
(ϕ : E →L[𝕜] E') :
continuous_linear_map.in_coordinates E (tangent_space I) E' (tangent_space I') x₀ x y₀ y ϕ = ϕ
The map in_coordinates for the tangent bundle is trivial on the model spaces
noncomputable
def
in_tangent_coordinates
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{H' : Type u_5}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M : Type u_6}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners 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, in_tangent_coordinates 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, tangent_space I (f x) →L[𝕜] tangent_space I' (g x).
We are unfolding tangent_space 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
- in_tangent_coordinates I I' f g ϕ = λ (x₀ x : N), continuous_linear_map.in_coordinates E (tangent_space I) E' (tangent_space I') (f x₀) (f x) (g x₀) (g x) (ϕ x)
theorem
in_tangent_coordinates_model_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{H' : Type u_5}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{N : Type u_9}
(f : N → H)
(g : N → H')
(ϕ : N → (E →L[𝕜] E'))
(x₀ : N) :
in_tangent_coordinates I I' f g ϕ x₀ = ϕ
theorem
in_tangent_coordinates_eq
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{H' : Type u_5}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M : Type u_6}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' M']
{N : Type u_9}
(f : N → M)
(g : N → M')
(ϕ : N → (E →L[𝕜] E'))
{x₀ x : N}
(hx : f x ∈ (charted_space.chart_at H (f x₀)).to_local_equiv.source)
(hy : g x ∈ (charted_space.chart_at H' (g x₀)).to_local_equiv.source) :
in_tangent_coordinates I I' f g ϕ x₀ x = ((tangent_bundle_core I' M').coord_change (achart H' (g x)) (achart H' (g x₀)) (g x)).comp ((ϕ x).comp ((tangent_bundle_core I M).coord_change (achart H (f x₀)) (achart H (f x)) (f x)))
@[protected, instance]
def
tangent_space.path_connected_space
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{H : Type u_2}
[topological_space H]
{I : model_with_corners ℝ E H}
{M : Type u_3}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
{x : M} :