feat(geometry/manifold): The preimage straightening theorem

src/analysis/calculus/implicit.lean

@@ -360,6 +360,12 @@ variables {f f'}
   (hf.implicit_to_local_homeomorph f f' hf' x).fst = f x :=
 rfl
 
+@[simp] lemma implicit_to_local_homeomorph_right_inv (hf : has_strict_fderiv_at f f' a)
+  (hf' : f'.range = ⊤) {x : f'.ker} {y : F}
+  (hy : (y, x) ∈ (hf.implicit_to_local_homeomorph f f' hf').target) :
+  f ((hf.implicit_to_local_homeomorph f f' hf').symm (y, x)) = y :=
+by rw [←(implicit_to_local_homeomorph_fst hf hf'), local_homeomorph.right_inv _ hy]
+
 @[simp] lemma implicit_to_local_homeomorph_apply_ker
   (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ⊤) (y : f'.ker) :
   hf.implicit_to_local_homeomorph f f' hf' (y + a) = (f (y + a), y) :=

src/geometry/manifold/mfderiv.lean

@@ -1393,6 +1393,10 @@ lemma mdifferentiable_at_ext_chart_at (h : y ∈ (chart_at H x).source) :
   mdifferentiable_at I 𝓘(𝕜, E) (ext_chart_at I x) y :=
 (has_mfderiv_at_ext_chart_at I h).mdifferentiable_at
 
+lemma mdifferentiable_at_ext_chart_at' :
+  mdifferentiable_at I 𝓘(𝕜, E) (ext_chart_at I x) x :=
+mdifferentiable_at_ext_chart_at _ (mem_chart_source H x)
+
 lemma mdifferentiable_on_ext_chart_at :
   mdifferentiable_on I 𝓘(𝕜, E) (ext_chart_at I x) (chart_at H x).source :=
 λ y hy, (has_mfderiv_within_at_ext_chart_at I hy).mdifferentiable_within_at

src/geometry/manifold/preimage_theorem.lean

@@ -0,0 +1,80 @@
+/-
+Copyright © 2021 Nicolò Cavalleri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nicolò Cavalleri
+-/
+
+import analysis.calculus.implicit
+import geometry.manifold.times_cont_mdiff
+
+noncomputable theory
+
+open function classical set
+
+local attribute [instance] prop_decidable
+
+variables {𝕜 : Type*} [is_R_or_C 𝕜] -- to have that smooth implies strictly differentiable
+{E : Type*} [normed_group E] [normed_space 𝕜 E] [complete_space E] -- do we really need this?
+{F : Type*} [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F] -- do we really need this?
+{H : Type*} [topological_space H]
+{G : Type*} [topological_space G]
+(I : model_with_corners 𝕜 E H)
+(J : model_with_corners 𝕜 F G)
+
+variables {M : Type*} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
+{N : Type*} [topological_space N] [charted_space G N] [smooth_manifold_with_corners J N]
+
+@[reducible] def regular_point (f : M → N) (p : M) := (mfderiv I J f p).range = ⊤
+
+@[reducible] def regular_value (f : M → N) (q : N) := ∀ p : f⁻¹' {q}, regular_point I J f p
+
+@[reducible] def regular_point.F' (f : M → N) (p : M) : E →L[𝕜] F :=
+(fderiv 𝕜 (written_in_ext_chart_at I J p f) ((ext_chart_at I p) p))
+
+variables {I J}
+
+lemma smooth_at.has_strict_fderiv_at [I.boundaryless] {f : M → N} {p : M} (h : smooth_at I J f p) :
+  has_strict_fderiv_at (written_in_ext_chart_at I J p f) (fderiv 𝕜 (written_in_ext_chart_at I J p f)
+  ((ext_chart_at I p) p)) ((ext_chart_at I p) p) :=
+sorry -- missing boundaryless API
+
+lemma regular_point.written_in_ext_chart_at_range_univ [I.boundaryless] {f : M → N} {p : M}
+  (hf : mdifferentiable_at I J f p) (h : regular_point I J f p) :
+  (fderiv 𝕜 (written_in_ext_chart_at I J p f) ((ext_chart_at I p) p)).range = ⊤ :=
+begin
+  rw [←mfderiv_eq_fderiv, written_in_ext_chart_at],
+  sorry -- missing boundaryless API
+end
+
+@[simp, reducible] def regular_point.pre_chart [I.boundaryless] {f : M → N} {p : M}
+  (h1 : smooth_at I J f p) (h2 : regular_point I J f p) :
+  local_homeomorph E (F × _) :=
+(h1.has_strict_fderiv_at).implicit_to_local_homeomorph (written_in_ext_chart_at I J p f) _
+  (h2.written_in_ext_chart_at_range_univ (h1.mdifferentiable_at le_top))
+
+@[simp, reducible] def regular_point.straighted_chart [I.boundaryless] {f : M → N} {p : M}
+  (h1 : smooth_at I J f p) (h2 : regular_point I J f p) :
+  local_equiv M (F × _) :=
+(ext_chart_at I p).trans (h2.pre_chart h1.smooth_at).to_local_equiv
+
+lemma regular_point.straighten_preimage [I.boundaryless] {f : M → N} {p : M}
+  (h1 : smooth_at I J f p)
+  (h2 : regular_point I J f p) {v : F} {k : (regular_point.F' I J f p).ker}
+  (hv : (v, k) ∈ (h2.straighted_chart h1.smooth_at).target) :
+  ((ext_chart_at J (f p)) ∘ f ∘ (h2.straighted_chart h1.smooth_at).symm) (v, k) = v :=
+begin
+  simp only [local_homeomorph.coe_coe_symm, local_equiv.coe_trans_symm],
+  rw [←comp.assoc, ←comp.assoc, comp.assoc _ f (ext_chart_at I p).symm, ←written_in_ext_chart_at,
+    comp_app, (h1.has_strict_fderiv_at.implicit_to_local_homeomorph_right_inv
+    (h2.written_in_ext_chart_at_range_univ (h1.mdifferentiable_at le_top)) hv.1)],
+end
+
+lemma regular_point.straighten_preimage' [I.boundaryless] {f : M → N} {p : M}
+  (h1 : smooth_at I J f p)
+  (h2 : regular_point I J f p) {q : N} {k : (regular_point.F' I J f p).ker}
+  (hq1 : ((ext_chart_at J (f p)) q, k) ∈ (regular_point.straighted_chart h1 h2).target)
+  (hq2 : (f (((regular_point.straighted_chart h1 h2).symm) ((ext_chart_at J (f p)) q, k))) ∈
+    (ext_chart_at J (f p)).source)
+  (hq3 : q ∈ (ext_chart_at J (f p)).source) : --probably hq1 → hq2 ∧ hq3
+  (f ∘ (h2.straighted_chart h1.smooth_at).symm) ((ext_chart_at J (f p)) q, k) = q :=
+(ext_chart_at J (f p)).inj_on hq2 hq3 (h2.straighten_preimage h1 hq1)

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -353,6 +353,12 @@ class model_with_corners.boundaryless {𝕜 : Type*} [nondiscrete_normed_field 
   (I : model_with_corners 𝕜 E H) : Prop :=
 (range_eq_univ : range I = univ)
 
+@[simp, mfld_simps] lemma model_with_corners.boundaryless_range_uni
+  {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+  {E : Type*} [normed_group E] [normed_space 𝕜 E] {H : Type*} [topological_space H]
+  {I : model_with_corners 𝕜 E H} [I.boundaryless] : range I = univ :=
+model_with_corners.boundaryless.range_eq_univ
+
 /-- The trivial model with corners has no boundary -/
 instance model_with_corners_self_boundaryless (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
   (E : Type*) [normed_group E] [normed_space 𝕜 E] : (model_with_corners_self 𝕜 E).boundaryless :=
@@ -720,6 +726,14 @@ begin
   exact (chart_at H x).continuous_on
 end
 
+lemma ext_chart_at_symm_continuous_on :
+  continuous_on (ext_chart_at I x).symm (ext_chart_at I x).target :=
+begin
+  refine continuous_on.comp (chart_at H x).continuous_on_symm I.continuous_symm.continuous_on _,
+  simp only [local_equiv.restr_coe_symm, ext_chart_at, inter_subset_right,
+    local_equiv.trans_target],
+end
+
 lemma ext_chart_at_continuous_at' {x' : M} (h : x' ∈ (ext_chart_at I x).source) :
   continuous_at (ext_chart_at I x) x' :=
 (ext_chart_at_continuous_on I x).continuous_at $ ext_chart_at_source_mem_nhds' I x h