Differentials of a partial diffeomorphism

The differentials of a partial diffeomorphism and of its inverse are mutually inverse at corresponding points, as for a global diffeomorphism (Diffeomorph.mfderiv_symm_apply_mfderiv_apply), and on the open source of a partial diffeomorphism the differential within the source is the differential. More generally, this holds at any point of an open partial homeomorphism where it and its inverse are differentiable.

For partial diffeomorphisms ψ, χ, φ into normed spaces, such as charts, the transitions ψ ∘ φ⁻¹ are differentiable, and their derivatives compose by the chain rule.

Main results

• OpenPartialHomeomorph.mfderiv_symm_apply_mfderiv_apply, OpenPartialHomeomorph.mfderiv_apply_mfderiv_symm_apply: where an open partial homeomorphism and its inverse are differentiable, their differentials are mutually inverse.
• PartialDiffeomorph.mfderivWithin_source: the differential within the source is the differential.
• PartialDiffeomorph.mfderiv_symm_apply_mfderiv_apply: the differential of the inverse undoes the differential.
• PartialDiffeomorph.mfderiv_apply_mfderiv_symm_apply: the differential undoes the differential of the inverse.
• PartialDiffeomorph.differentiableAt_comp_symm: for partial diffeomorphisms into normed spaces, the transition ψ ∘ φ⁻¹ is differentiable.
• PartialDiffeomorph.fderiv_comp_symm_eq_comp: the derivatives of transitions compose, the chain rule D(ψ ∘ φ⁻¹) = D(ψ ∘ χ⁻¹) ∘ D(χ ∘ φ⁻¹).

theorem OpenPartialHomeomorph.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] (Φ : OpenPartialHomeomorph M N) {x : M} (hx : x ∈ Φ.source) (hΦ : MDiffAt ↑Φ x) (hΦs : MDiffAt ↑Φ.symm (↑Φ x)) (v : TangentSpace I x) : (mfderiv% ↑Φ.symm (↑Φ x)) ((mfderiv% ↑Φ x) v) = v

The differential of the inverse of an open partial homeomorphism undoes its differential at a point of the source where both are differentiable.

theorem OpenPartialHomeomorph.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] (Φ : OpenPartialHomeomorph M N) {y : N} (hy : y ∈ Φ.target) (hΦ : MDiffAt ↑Φ (↑Φ.symm y)) (hΦs : MDiffAt ↑Φ.symm y) (v : TangentSpace J y) : (mfderiv% ↑Φ (↑Φ.symm y)) ((mfderiv% ↑Φ.symm y) v) = v

The differential of an open partial homeomorphism undoes the differential of its inverse at a point of the target where both are differentiable.

theorem PartialDiffeomorph.mfderivWithin_source {𝕜 : 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 ℕ∞} (Φ : PartialDiffeomorph I J M N n) {x : M} (hx : x ∈ Φ.source) : mfderiv[Φ.source] ↑Φ.toPartialEquiv x = mfderiv% ↑Φ.toPartialEquiv x

On the open source of a partial diffeomorphism the differential within the source is the differential.

theorem PartialDiffeomorph.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 ℕ∞} (Φ : PartialDiffeomorph I J M N n) (hn : n ≠ 0) {x : M} (hx : x ∈ Φ.source) (v : TangentSpace I x) : (mfderiv% ↑Φ.symm.toPartialEquiv (↑Φ.toPartialEquiv x)) ((mfderiv% ↑Φ.toPartialEquiv x) v) = v

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

theorem PartialDiffeomorph.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 ℕ∞} (Φ : PartialDiffeomorph I J M N n) (hn : n ≠ 0) {y : N} (hy : y ∈ Φ.target) (v : TangentSpace J y) : (mfderiv% ↑Φ.toPartialEquiv (↑Φ.symm.toPartialEquiv y)) ((mfderiv% ↑Φ.symm.toPartialEquiv y) v) = v

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

theorem PartialDiffeomorph.differentiableAt_comp_symm {𝕜 : 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] {n : WithTop ℕ∞} {G : Type u_8} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {G' : Type u_9} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (ψ : PartialDiffeomorph I (modelWithCornersSelf 𝕜 G') M G' n) (φ : PartialDiffeomorph I (modelWithCornersSelf 𝕜 G) M G n) (hn : n ≠ 0) {x : M} (hψ : x ∈ ψ.source) (hφ : x ∈ φ.source) : DifferentiableAt 𝕜 (fun (z : G) => ↑ψ.toPartialEquiv (↑φ.symm.toPartialEquiv z)) (↑φ.toPartialEquiv x)

The transition ψ ∘ φ⁻¹ between two partial diffeomorphisms into normed spaces is differentiable at the image under φ of every point of both sources.

theorem PartialDiffeomorph.fderiv_comp_symm_eq_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] {n : WithTop ℕ∞} {G : Type u_8} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {G' : Type u_9} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {G'' : Type u_10} [NormedAddCommGroup G''] [NormedSpace 𝕜 G''] (ψ : PartialDiffeomorph I (modelWithCornersSelf 𝕜 G'') M G'' n) (χ : PartialDiffeomorph I (modelWithCornersSelf 𝕜 G') M G' n) (φ : PartialDiffeomorph I (modelWithCornersSelf 𝕜 G) M G n) (hn : n ≠ 0) {x : M} (hψ : x ∈ ψ.source) (hχ : x ∈ χ.source) (hφ : x ∈ φ.source) : fderiv 𝕜 (fun (z : G) => ↑ψ.toPartialEquiv (↑φ.symm.toPartialEquiv z)) (↑φ.toPartialEquiv x) = fderiv 𝕜 (fun (z : G') => ↑ψ.toPartialEquiv (↑χ.symm.toPartialEquiv z)) (↑χ.toPartialEquiv x) ∘SL fderiv 𝕜 (fun (z : G) => ↑χ.toPartialEquiv (↑φ.symm.toPartialEquiv z)) (↑φ.toPartialEquiv x)

The chain rule for transitions. For partial diffeomorphisms ψ, χ, φ into normed spaces whose sources contain x, the derivative of the transition ψ ∘ φ⁻¹ at φ x is the derivative of χ ∘ φ⁻¹ at φ x followed by that of ψ ∘ χ⁻¹ at χ x.