Constructions of partial diffeomorphisms

Basic ways of producing a PartialDiffeomorph include lowering the regularity of a given one and reading a continuous linear equivalence as one at any regularity. Mathlib's ContinuousLinearEquiv.toDiffeomorph gives the latter at regularity ∞ only, so it does not cover the analytic regularity ω. A transition between charts taking specified points to the same coordinate gives a local change of parameters intertwining those charts. The file also records that the coordinate axes of a partial diffeomorphism into a real Euclidean space, centred at a point, pull back to curves through that point.

It also records the source, target, forward map and inverse map of Mathlib's composition PartialDiffeomorph.trans, so that callers need not unfold it through OpenPartialHomeomorph.

Main definitions

• PartialDiffeomorph.ofLE: a C^n partial diffeomorphism as a C^m one, for m ≤ n.
• ContinuousLinearEquiv.toPartialDiffeomorph: a continuous linear equivalence as a C^n partial diffeomorphism defined everywhere, for any n.
• PartialDiffeomorph.trans_source, PartialDiffeomorph.trans_target, PartialDiffeomorph.coe_trans, PartialDiffeomorph.coe_trans_symm: the composition of partial diffeomorphisms, computed componentwise.

Main results

• PartialDiffeomorph.exists_transition: charts with a common coordinate induce a local change of parameters carrying the specified points to one another.
• PartialDiffeomorph.exists_curve_single_axis: pulling a coordinate axis back through a partial diffeomorphism into EuclideanSpace ℝ ι gives a curve through the centre point, C^n near 0.

def PartialDiffeomorph.ofLE {𝕜 : 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] {m n : WithTop ℕ∞} (Φ : PartialDiffeomorph I J M N n) (hmn : m ≤ n) : PartialDiffeomorph I J M N m

A C^n partial diffeomorphism as a C^m one, for m ≤ n.

@[simp]

theorem PartialDiffeomorph.ofLE_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] {m n : WithTop ℕ∞} (Φ : PartialDiffeomorph I J M N n) (hmn : m ≤ n) : (Φ.ofLE hmn).toPartialEquiv = Φ.toPartialEquiv

Lowering the regularity keeps the underlying partial equivalence.

theorem PartialDiffeomorph.trans_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 ℕ∞} {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H'' : Type u_9} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 F' H''} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] (Φ : PartialDiffeomorph I J M N n) (Ψ : PartialDiffeomorph J K N P n) : (Φ.trans Ψ).source = Φ.source ∩ ↑Φ.toPartialEquiv ⁻¹' Ψ.source

The source of a composition of partial diffeomorphisms.

theorem PartialDiffeomorph.trans_target {𝕜 : 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 ℕ∞} {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H'' : Type u_9} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 F' H''} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] (Φ : PartialDiffeomorph I J M N n) (Ψ : PartialDiffeomorph J K N P n) : (Φ.trans Ψ).target = Ψ.target ∩ ↑Ψ.symm.toPartialEquiv ⁻¹' Φ.target

The target of a composition of partial diffeomorphisms.

theorem PartialDiffeomorph.coe_trans {𝕜 : 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 ℕ∞} {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H'' : Type u_9} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 F' H''} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] (Φ : PartialDiffeomorph I J M N n) (Ψ : PartialDiffeomorph J K N P n) : ↑(Φ.trans Ψ).toPartialEquiv = ↑Ψ.toPartialEquiv ∘ ↑Φ.toPartialEquiv

The forward map of a composition of partial diffeomorphisms is the composition of the forward maps.

theorem PartialDiffeomorph.coe_trans_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 ℕ∞} {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H'' : Type u_9} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 F' H''} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] (Φ : PartialDiffeomorph I J M N n) (Ψ : PartialDiffeomorph J K N P n) : ↑(Φ.trans Ψ).symm.toPartialEquiv = ↑Φ.symm.toPartialEquiv ∘ ↑Ψ.symm.toPartialEquiv

The inverse map of a composition of partial diffeomorphisms is the composition of the inverse maps, in the opposite order.

theorem PartialDiffeomorph.exists_transition {𝕜 : 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 ℕ∞} {G : Type u_8} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H'' : Type u_9} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 G H''} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] (c : PartialDiffeomorph I K M P n) (d : PartialDiffeomorph J K N P n) {x : M} {y : N} (hx : x ∈ c.source) (hy : y ∈ d.source) (hxy : ↑c.toPartialEquiv x = ↑d.toPartialEquiv y) : ∃ (e : PartialDiffeomorph I J M N n), x ∈ e.source ∧ ↑e.toPartialEquiv x = y ∧ e.source ⊆ c.source ∧ Set.MapsTo (↑e.toPartialEquiv) e.source d.source ∧ ∀ z ∈ e.source, ↑d.toPartialEquiv (↑e.toPartialEquiv z) = ↑c.toPartialEquiv z

Two charts taking specified source points to the same coordinate induce a local change of parameters. The transition sends x to y, stays in both chart domains, and intertwines the coordinate maps.

theorem PartialDiffeomorph.exists_curve_single_axis {n : WithTop ℕ∞} {E : Type u_11} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_12} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_13} [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_14} [Fintype ι] [DecidableEq ι] {x : M} (ψ : PartialDiffeomorph I (modelWithCornersSelf ℝ (EuclideanSpace ℝ ι)) M (EuclideanSpace ℝ ι) n) (hxψ : x ∈ ψ.source) (hψx : ↑ψ.toPartialEquiv x = 0) (i : ι) : ∃ (γ : ℝ → M), (∀ᶠ (t : ℝ) in nhds 0, ContMDiffAt (modelWithCornersSelf ℝ ℝ) I n γ t) ∧ γ 0 = x ∧ ∀ᶠ (t : ℝ) in nhds 0, γ t ∈ ψ.source ∧ ↑ψ.toPartialEquiv (γ t) = EuclideanSpace.single i t

Pulling a coordinate axis of a C^n partial diffeomorphism ψ into EuclideanSpace ℝ ι with ψ x = 0 back through the inverse chart gives a curve through x, C^n near the parameter 0, which at every parameter near 0 lies in the chart source and maps to the point of the axis with that coordinate.

def ContinuousLinearEquiv.toPartialDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (A : E ≃L[𝕜] F) : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n

A continuous linear equivalence as a C^n partial diffeomorphism defined everywhere, for any regularity n, including the analytic regularity ω not reached by ContinuousLinearEquiv.toDiffeomorph.

@[simp]

theorem ContinuousLinearEquiv.toPartialDiffeomorph_toPartialEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (A : E ≃L[𝕜] F) : A.toPartialDiffeomorph.toPartialEquiv = (↑A).toEquiv.toPartialEquiv

The partial equivalence underlying ContinuousLinearEquiv.toPartialDiffeomorph is the underlying equivalence, on the whole space.