mathlib documentation

geometry.manifold.cont_mdiff_mfderiv

Interactions between differentiability, smoothness and manifold derivatives #

We give the relation between mdifferentiable, cont_mdiff, mfderiv, tangent_map and related notions.

Main statements #

Definition of smooth functions between manifolds #

Deducing differentiability from smoothness #

theorem cont_mdiff_within_at.mdifferentiable_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} (hf : cont_mdiff_within_at I I' n f s x) (hn : 1 n) :
theorem cont_mdiff_at.mdifferentiable_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {n : ℕ∞} (hf : cont_mdiff_at I I' n f x) (hn : 1 n) :
theorem cont_mdiff_on.mdifferentiable_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s : set M} {n : ℕ∞} (hf : cont_mdiff_on I I' n f s) (hn : 1 n) :
theorem cont_mdiff.mdifferentiable {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {n : ℕ∞} (hf : cont_mdiff I I' n f) (hn : 1 n) :
theorem smooth_within_at.mdifferentiable_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s : set M} {x : M} (hf : smooth_within_at I I' f s x) :
theorem smooth_at.mdifferentiable_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} (hf : smooth_at I I' f x) :
theorem smooth_on.mdifferentiable_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s : set M} (hf : smooth_on I I' f s) :
theorem smooth.mdifferentiable {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} (hf : smooth I I' f) :
theorem smooth.mdifferentiable_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} (hf : smooth I I' f) :
theorem smooth.mdifferentiable_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s : set M} {x : M} (hf : smooth I I' f) :

The tangent map of a smooth function is smooth #

theorem cont_mdiff_on.continuous_on_tangent_map_within_aux {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {n : ℕ∞} {f : H H'} {s : set H} (hf : cont_mdiff_on I I' n f s) (hn : 1 n) (hs : unique_mdiff_on I s) :

If a function is C^n with 1 ≤ n on a domain with unique derivatives, then its bundled derivative is continuous. In this auxiliary lemma, we prove this fact when the source and target space are model spaces in models with corners. The general fact is proved in cont_mdiff_on.continuous_on_tangent_map_within

theorem cont_mdiff_on.cont_mdiff_on_tangent_map_within_aux {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {m n : ℕ∞} {f : H H'} {s : set H} (hf : cont_mdiff_on I I' n f s) (hmn : m + 1 n) (hs : unique_mdiff_on I s) :

If a function is C^n on a domain with unique derivatives, then its bundled derivative is C^m when m+1 ≤ n. In this auxiliary lemma, we prove this fact when the source and target space are model spaces in models with corners. The general fact is proved in cont_mdiff_on.cont_mdiff_on_tangent_map_within

theorem cont_mdiff_on.cont_mdiff_on_tangent_map_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M M'} {s : set M} {m n : ℕ∞} (hf : cont_mdiff_on I I' n f s) (hmn : m + 1 n) (hs : unique_mdiff_on I s) :

If a function is C^n on a domain with unique derivatives, then its bundled derivative is C^m when m+1 ≤ n.

theorem cont_mdiff_on.continuous_on_tangent_map_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M M'} {s : set M} {n : ℕ∞} (hf : cont_mdiff_on I I' n f s) (hmn : 1 n) (hs : unique_mdiff_on I s) :

If a function is C^n on a domain with unique derivatives, with 1 ≤ n, then its bundled derivative is continuous there.

theorem cont_mdiff.cont_mdiff_tangent_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M M'} {m n : ℕ∞} (hf : cont_mdiff I I' n f) (hmn : m + 1 n) :

If a function is C^n, then its bundled derivative is C^m when m+1 ≤ n.

theorem cont_mdiff.continuous_tangent_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M M'} {n : ℕ∞} (hf : cont_mdiff I I' n f) (hmn : 1 n) :

If a function is C^n, with 1 ≤ n, then its bundled derivative is continuous.

Smoothness of the projection in a basic smooth bundle #

A version of cont_mdiff_at_iff_target when the codomain is the total space of a basic_smooth_vector_bundle_core. The continuity condition in the RHS is weaker.

theorem basic_smooth_vector_bundle_core.smooth_const_section {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] (Z : basic_smooth_vector_bundle_core I M E') (v : E') (h : (i j : (charted_space.atlas H M)) (x : M), x i.val.to_local_equiv.source j.val.to_local_equiv.source (Z.coord_change i j ((i.val) x)) v = v) :
smooth I (I.prod (model_with_corners_self 𝕜 E')) (show M Z.to_vector_bundle_core.total_space, from λ (x : M), x, v⟩)

If an element of E' is invariant under all coordinate changes, then one can define a corresponding section of the fiber bundle, which is smooth. This applies in particular to the zero section of a vector bundle. Another example (not yet defined) would be the identity section of the endomorphism bundle of a vector bundle.

Smoothness of the tangent bundle projection #

The zero section of the tangent bundle

Equations

The derivative of the zero section of the tangent bundle maps ⟨x, v⟩ to ⟨⟨x, 0⟩, ⟨v, 0⟩⟩.

Note that, as currently framed, this is a statement in coordinates, thus reliant on the choice of the coordinate system we use on the tangent bundle.

However, the result itself is coordinate-dependent only to the extent that the coordinates determine a splitting of the tangent bundle. Moreover, there is a canonical splitting at each point of the zero section (since there is a canonical horizontal space there, the tangent space to the zero section, in addition to the canonical vertical space which is the kernel of the derivative of the projection), and this canonical splitting is also the one that comes from the coordinates on the tangent bundle in our definitions. So this statement is not as crazy as it may seem.

TODO define splittings of vector bundles; state this result invariantly.