Differentials of diffeomorphisms

The differentials of a diffeomorphism and its inverse undo each other, and the differential of a diffeomorphism undoes the pullback of vector fields along it. Differentiability at a point is also preserved by precomposition and postcomposition with a diffeomorphism, and the tangent images of a map, the ranges of its differentials, are unchanged by precomposition with a diffeomorphism and are mapped by the differential under postcomposition. These facts support inverse isometries and transport of curve differentiability through diffeomorphisms. The underlying equivalence of a diffeomorphism viewed as a partial diffeomorphism is also characterized, for composition with partial coordinates.

@[simp]

theorem Diffeomorph.toPartialDiffeomorph_toPartialEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) : h.toPartialDiffeomorph.toPartialEquiv = h.toPartialEquiv

The partial equivalence underlying a diffeomorphism viewed as a partial diffeomorphism is its everywhere-defined equivalence.

@[simp]

theorem Diffeomorph.mfderiv_apply_mfderiv_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (hn : n ≠ 0) (x : M) (v : TangentSpace J (h x)) : (mfderiv% ⇑h x) ((mfderiv% ⇑h.symm (h x)) v) = v

The differentials of a diffeomorphism and its inverse compose to the identity.

@[simp]

theorem Diffeomorph.mfderiv_symm_apply_mfderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (hn : n ≠ 0) (x : M) (v : TangentSpace I x) : (mfderiv% ⇑h.symm (h x)) ((mfderiv% ⇑h x) v) = v

The differential of the inverse undoes the differential of a diffeomorphism.

@[simp]

theorem Diffeomorph.mfderiv_apply_mpullback {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (hn : n ≠ 0) (V : (y : N) → TangentSpace J y) (x : M) : (mfderiv% ⇑h x) (VectorField.mpullback I J (⇑h) V x) = V (h x)

The differential of a diffeomorphism maps the pullback of a vector field at x to the value of the field at h x.

@[simp]

theorem Diffeomorph.tangentMap_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (hn : n ≠ 0) (z : TangentBundle I M) : tangentMap J I (⇑h.symm) (tangentMap I J (⇑h) z) = z

Applying the tangent map of a diffeomorphism and then that of its inverse returns the original tangent vector.

@[simp]

theorem Diffeomorph.tangentMap_apply_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (hn : n ≠ 0) (z : TangentBundle J N) : tangentMap I J (⇑h) (tangentMap J I (⇑h.symm) z) = z

Applying the tangent map of the inverse of a diffeomorphism and then that of the diffeomorphism returns the original tangent vector.

theorem Diffeomorph.tangentMap_symm_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (hn : n ≠ 0) (x : M) (w : TangentSpace J (h x)) : tangentMap J I ⇑h.symm ⟨h x, w⟩ = ⟨x, (mfderiv% ⇑h x).inverse w⟩

The tangent map of the inverse acts on a fibre by the inverse differential. This holds for every nonzero differentiability order, including finite orders.

theorem Diffeomorph.mdifferentiableAt_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (hn : n ≠ 0) {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H'' : Type u_9} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 E' H''} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] {f : P → M} {x : P} : MDiffAt (⇑h ∘ f) x ↔ MDiffAt f x

Postcomposition with a diffeomorphism preserves differentiability at a point.

theorem Diffeomorph.mdifferentiableAt_comp_diffeomorph_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (hn : n ≠ 0) {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H'' : Type u_9} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 E' H''} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] {f : N → P} {x : M} : MDiffAt (f ∘ ⇑h) x ↔ MDiffAt f (h x)

Precomposition with a diffeomorphism preserves differentiability at the corresponding point.

theorem Diffeomorph.range_mfderiv_diffeomorph_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H'' : Type u_9} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 E' H''} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] (h : Diffeomorph I J M N n) (hn : n ≠ 0) (f : P → M) (x : P) : (↑(mfderiv% (⇑h ∘ f) x)).range = Submodule.map (↑↑(h.mfderivToContinuousLinearEquiv hn (f x))) (↑(mfderiv% f x)).range

Postcomposition with a diffeomorphism maps tangent images by its differential: the range of the differential of h ∘ f at x is the image of the range of the differential of f under the linear equivalence dh, Diffeomorph.mfderivToContinuousLinearEquiv. No differentiability of f is assumed: when f is not differentiable at x, neither is h ∘ f, and both ranges are zero.

theorem Diffeomorph.range_mfderiv_comp_diffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H'' : Type u_9} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 E' H''} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] (h : Diffeomorph I J M N n) (hn : n ≠ 0) (f : N → P) (x : M) : (↑(mfderiv% (f ∘ ⇑h) x)).range = (↑(mfderiv% f (h x))).range

Precomposition with a diffeomorphism does not change tangent images: the range of the differential of f ∘ h at x is the range of the differential of f at h x. No differentiability of f is assumed.