The inverse function theorem for manifolds

Mathlib knows that a C^n local diffeomorphism has invertible differentials (IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv) and lists the converse as a TODO in Mathlib/Geometry/Manifold/LocalDiffeomorph.lean. This file proves that converse at interior points of Banach manifolds: a map which is C^n on an open set, with 1 ≤ n, and whose mfderiv at a point of that set is a continuous linear equivalence, is a C^n local diffeomorphism there.

The interior-point form applies to maps between manifolds with boundary whenever the source point lies away from the boundary; invertibility of the differential then forces its image to be an interior point as well. On a boundaryless source manifold the source condition is automatic, even when either ambient model has boundary, yielding the usual global criterion from invertibility of every differential.

The file also records that maximal-atlas charts are local diffeomorphisms, and that being a local diffeomorphism at a point is an open condition: the partial diffeomorphism witnessing it at one point witnesses it at every nearby point.

Main results

• TauCeti.coe_diffeomorphOfBijective: the associated global diffeomorphism has the original forward map.
• TauCeti.extChartPartialDiffeomorph: an extended chart restricted to the interior of its target, as a partial diffeomorphism onto an open subset of the model space.
• TauCeti.PartialDiffeomorph.ofOpenPartialHomeomorph: an open partial homeomorphism between model spaces which is C^n in both directions, as a partial diffeomorphism.
• TauCeti.isLocalDiffeomorphAt_of_mfderiv_eq: the inverse function theorem for manifolds.
• TauCeti.isLocalDiffeomorphAt_iff_exists_mfderiv_eq: the resulting characterisation of IsLocalDiffeomorphAt at an interior point, for a map which is C^n on an open set.
• TauCeti.isLocalDiffeomorphAt_of_eqOn: a map agreeing with a partial diffeomorphism on its source is a local diffeomorphism there.
• OpenPartialHomeomorph.isLocalDiffeomorphAt_of_mem_maximalAtlas: a maximal-atlas chart is a local diffeomorphism at every point of its source.
• IsLocalDiffeomorphAt.eventually: being a local diffeomorphism at a point is an open condition.
• TauCeti.isLocalDiffeomorph_of_mfderiv_eq: the global version.

@[simp]

theorem TauCeti.coe_diffeomorphOfBijective {𝕂 : 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] {G : Type u_5} [TopologicalSpace G] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {I : ModelWithCorners 𝕂 E H} {J : ModelWithCorners 𝕂 F G} {n : WithTop ℕ∞} {f : M → N} {hf : IsLocalDiffeomorph I J n f} {hf' : Function.Bijective f} : ⇑(hf.diffeomorphOfBijective hf') = f

The diffeomorphism associated to a bijective local diffeomorphism has the given forward map. This computation rule lets callers use the constructor without unfolding its choice of inverse.

def TauCeti.extChartPartialDiffeomorph {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {H : Type u_4} [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners 𝕂 E H) (n : WithTop ℕ∞) [IsManifold I n M] (x : M) : PartialDiffeomorph I (modelWithCornersSelf 𝕂 E) M E n

The extended chart at x, restricted to the interior of its target and regarded as a partial diffeomorphism from M to the model space E.

Equations

• TauCeti.extChartPartialDiffeomorph I n x = { toPartialEquiv := ⋯.restr, open_source := ⋯, open_target := ⋯, contMDiffOn_toFun := ⋯, contMDiffOn_invFun := ⋯ }

theorem TauCeti.extChartPartialDiffeomorph_source {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {H : Type u_4} [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners 𝕂 E H) (n : WithTop ℕ∞) [IsManifold I n M] (x : M) : (extChartPartialDiffeomorph I n x).source = (extChartAt I x).source ∩ ↑(extChartAt I x) ⁻¹' interior (extChartAt I x).target

The source of the restricted extended chart consists of points in the original chart source whose chart coordinates lie in the interior of the chart target.

@[simp]

theorem TauCeti.mem_extChartPartialDiffeomorph_source {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {H : Type u_4} [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners 𝕂 E H) (n : WithTop ℕ∞) [IsManifold I n M] (x : M) : x ∈ (extChartPartialDiffeomorph I n x).source ↔ I.IsInteriorPoint x

The center of the restricted extended chart belongs to its source exactly when it is an interior point of the manifold.

@[simp]

theorem TauCeti.extChartPartialDiffeomorph_target {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {H : Type u_4} [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners 𝕂 E H) (n : WithTop ℕ∞) [IsManifold I n M] (x : M) : (extChartPartialDiffeomorph I n x).target = interior (extChartAt I x).target

The target of the restricted extended chart is the interior of the original chart target.

@[simp]

theorem TauCeti.coe_extChartPartialDiffeomorph {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {H : Type u_4} [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners 𝕂 E H) (n : WithTop ℕ∞) [IsManifold I n M] (x : M) : ↑(extChartPartialDiffeomorph I n x).toPartialEquiv = ↑(extChartAt I x)

The forward function of the restricted extended chart agrees with the original extended chart.

@[simp]

theorem TauCeti.extChartPartialDiffeomorph_symm_apply {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {H : Type u_4} [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners 𝕂 E H) (n : WithTop ℕ∞) [IsManifold I n M] (x : M) (y : E) : ↑(extChartPartialDiffeomorph I n x).symm y = ↑(extChartAt I x).symm y

The inverse of the restricted extended chart agrees pointwise with the inverse extended chart.

def TauCeti.PartialDiffeomorph.ofOpenPartialHomeomorph {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] {n : WithTop ℕ∞} (Θ : OpenPartialHomeomorph E F) (hΘ : ContDiffOn 𝕂 n (↑Θ) Θ.source) (hΘsymm : ContDiffOn 𝕂 n (↑Θ.symm) Θ.target) : PartialDiffeomorph (modelWithCornersSelf 𝕂 E) (modelWithCornersSelf 𝕂 F) E F n

An open partial homeomorphism between model spaces which is C^n in both directions is a partial diffeomorphism.

Equations

• TauCeti.PartialDiffeomorph.ofOpenPartialHomeomorph Θ hΘ hΘsymm = { toPartialEquiv := Θ.toPartialEquiv, open_source := ⋯, open_target := ⋯, contMDiffOn_toFun := ⋯, contMDiffOn_invFun := ⋯ }

@[simp]

theorem TauCeti.PartialDiffeomorph.ofOpenPartialHomeomorph_toPartialEquiv {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] {n : WithTop ℕ∞} (Θ : OpenPartialHomeomorph E F) (hΘ : ContDiffOn 𝕂 n (↑Θ) Θ.source) (hΘsymm : ContDiffOn 𝕂 n (↑Θ.symm) Θ.target) : (ofOpenPartialHomeomorph Θ hΘ hΘsymm).toPartialEquiv = Θ.toPartialEquiv

theorem TauCeti.isLocalDiffeomorphAt_of_eqOn {𝕂 : 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] {G : Type u_5} [TopologicalSpace G] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {I : ModelWithCorners 𝕂 E H} {J : ModelWithCorners 𝕂 F G} {n : WithTop ℕ∞} {Φ : PartialDiffeomorph I J M N n} {f : M → N} {x : M} (hx : x ∈ Φ.source) (hf : Set.EqOn f (↑Φ.toPartialEquiv) Φ.source) : IsLocalDiffeomorphAt I J n f x

A map agreeing with a partial diffeomorphism on its source is a C^n local diffeomorphism at every point of that source.

theorem OpenPartialHomeomorph.isLocalDiffeomorphAt_of_mem_maximalAtlas {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {H : Type u_4} [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners 𝕂 E H} {n : WithTop ℕ∞} (e : OpenPartialHomeomorph M H) (he : e ∈ IsManifold.maximalAtlas I n M) {x : M} (hx : x ∈ e.source) : IsLocalDiffeomorphAt I I n (↑e) x

A chart in the C^n maximal atlas is a local diffeomorphism at every point of its source.

theorem IsLocalDiffeomorphAt.eventually {𝕂 : 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] {G : Type u_5} [TopologicalSpace G] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {I : ModelWithCorners 𝕂 E H} {J : ModelWithCorners 𝕂 F G} {n : WithTop ℕ∞} {f : M → N} {x : M} (hf : IsLocalDiffeomorphAt I J n f x) : ∀ᶠ (y : M) in nhds x, IsLocalDiffeomorphAt I J n f y

Being a local diffeomorphism at a point is an open condition. A C^n local diffeomorphism at x is a C^n local diffeomorphism at every nearby point.

theorem TauCeti.isLocalDiffeomorphAt_of_mfderiv_eq {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [CompleteSpace E] {I : ModelWithCorners 𝕂 E H} {J : ModelWithCorners 𝕂 F G} {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] {f : M → N} {s : Set M} {x : M} (hf : ContMDiffOn I J n f s) (hs : IsOpen s) (hx : x ∈ s) (hIx : I.IsInteriorPoint x) (hn : 1 ≤ n) {e : TangentSpace I x ≃L[𝕂] TangentSpace J (f x)} (he : ↑e = mfderiv% f x) : IsLocalDiffeomorphAt I J n f x

The inverse function theorem for manifolds. If f is C^n on an open set s with 1 ≤ n, x belongs to s and is an interior point, and the differential at x is a continuous linear equivalence, then f is a C^n local diffeomorphism at x.

Mathlib's Mathlib/Geometry/Manifold/LocalDiffeomorph.lean lists this implication as a TODO.

theorem TauCeti.isLocalDiffeomorphAt_iff_exists_mfderiv_eq {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [CompleteSpace E] {I : ModelWithCorners 𝕂 E H} {J : ModelWithCorners 𝕂 F G} {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] {f : M → N} {s : Set M} {x : M} (hf : ContMDiffOn I J n f s) (hs : IsOpen s) (hx : x ∈ s) (hIx : I.IsInteriorPoint x) (hn : 1 ≤ n) : IsLocalDiffeomorphAt I J n f x ↔ ∃ (e : TangentSpace I x ≃L[𝕂] TangentSpace J (f x)), ↑e = mfderiv% f x

For a map which is C^n on an open set, with 1 ≤ n, being a C^n local diffeomorphism at an interior point is exactly invertibility of the differential there.

theorem TauCeti.isLocalDiffeomorph_of_mfderiv_eq {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [CompleteSpace E] {I : ModelWithCorners 𝕂 E H} {J : ModelWithCorners 𝕂 F G} {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] {f : M → N} [BoundarylessManifold I M] (hf : ContMDiff I J n f) (hn : 1 ≤ n) (he : ∀ (y : M), ∃ (e : TangentSpace I y ≃L[𝕂] TangentSpace J (f y)), ↑e = mfderiv% f y) : IsLocalDiffeomorph I J n f

The inverse function theorem for manifolds, global form: a C^n map (1 ≤ n) from a boundaryless source manifold, all of whose differentials are continuous linear equivalences, is a C^n local diffeomorphism.