feat(topology,geometry/manifold): continuous and smooth partition of …

…unity (#8281)

Fixes #6392

src/geometry/manifold/bump_function.lean

@@ -13,18 +13,18 @@ import geometry.manifold.instances.real
 In this file we define `smooth_bump_function I c` to be a bundled smooth "bump" function centered at
 `c`. It is a structure that consists of two real numbers `0 < r < R` with small enough `R`. We
 define a coercion to function for this type, and for `f : smooth_bump_function I c`, the function
-`⇑f` written in the extended chart at `f.c` has the following properties:
+`⇑f` written in the extended chart at `c` has the following properties:
 
-* `f x = 1` in the closed euclidean ball of radius `f.r` centered at `f.c`;
-* `f x = 0` outside of the euclidean ball of radius `f.R` centered at `f.c`;
+* `f x = 1` in the closed euclidean ball of radius `f.r` centered at `c`;
+* `f x = 0` outside of the euclidean ball of radius `f.R` centered at `c`;
 * `0 ≤ f x ≤ 1` for all `x`.
 
-The actual statements involve (pre)images under `ext_chart_at I f.c` and are given as lemmas in the
+The actual statements involve (pre)images under `ext_chart_at I f` and are given as lemmas in the
 `smooth_bump_function` namespace.
 
 ## Tags
 
-manifold, smooth bump function, partition of unity, Whitney theorem
+manifold, smooth bump function
 -/
 
 universes uE uF uH uM
@@ -54,7 +54,7 @@ In this section we define a structure for a bundled smooth bump function and pro
 
 The structure contains data required to construct a function with these properties. The function is
 available as `⇑f` or `f x`. Formal statements of the properties listed above involve some
-(pre)images under `ext_chart_at I f.c` and are given as lemmas in the `msmooth_bump_function`
+(pre)images under `ext_chart_at I f.c` and are given as lemmas in the `smooth_bump_function`
 namespace. -/
 structure smooth_bump_function (c : M) extends times_cont_diff_bump (ext_chart_at I c c) :=
 (closed_ball_subset :
@@ -307,6 +307,8 @@ end
 
 protected lemma smooth_at {x} : smooth_at I 𝓘(ℝ) f x := f.smooth.smooth_at
 
+protected lemma continuous : continuous f := f.smooth.continuous
+
 /-- If `f : smooth_bump_function I c` is a smooth bump function and `g : M → G` is a function smooth
 on the source of the chart at `c`, then `f • g` is smooth on the whole manifold. -/
 lemma smooth_smul {G} [normed_group G] [normed_space ℝ G]

src/geometry/manifold/times_cont_mdiff.lean

@@ -923,26 +923,59 @@ begin
   exact times_cont_diff_within_at_const,
 end
 
+@[to_additive]
+lemma times_cont_mdiff_one [has_one M'] : times_cont_mdiff I I' n (1 : M → M') :=
+by simp only [pi.one_def, times_cont_mdiff_const]
+
 lemma smooth_const : smooth I I' (λ (x : M), c) := times_cont_mdiff_const
 
+@[to_additive]
+lemma smooth_one [has_one M'] : smooth I I' (1 : M → M') :=
+by simp only [pi.one_def, smooth_const]
+
 lemma times_cont_mdiff_on_const : times_cont_mdiff_on I I' n (λ (x : M), c) s :=
 times_cont_mdiff_const.times_cont_mdiff_on
 
+@[to_additive]
+lemma times_cont_mdiff_on_one [has_one M'] : times_cont_mdiff_on I I' n (1 : M → M') s :=
+times_cont_mdiff_one.times_cont_mdiff_on
+
 lemma smooth_on_const : smooth_on I I' (λ (x : M), c) s :=
 times_cont_mdiff_on_const
 
+@[to_additive]
+lemma smooth_on_one [has_one M'] : smooth_on I I' (1 : M → M') s :=
+times_cont_mdiff_on_one
+
 lemma times_cont_mdiff_at_const : times_cont_mdiff_at I I' n (λ (x : M), c) x :=
 times_cont_mdiff_const.times_cont_mdiff_at
 
+@[to_additive]
+lemma times_cont_mdiff_at_one [has_one M'] : times_cont_mdiff_at I I' n (1 : M → M') x :=
+times_cont_mdiff_one.times_cont_mdiff_at
+
 lemma smooth_at_const : smooth_at I I' (λ (x : M), c) x :=
 times_cont_mdiff_at_const
 
+@[to_additive]
+lemma smooth_at_one [has_one M'] : smooth_at I I' (1 : M → M') x :=
+times_cont_mdiff_at_one
+
 lemma times_cont_mdiff_within_at_const : times_cont_mdiff_within_at I I' n (λ (x : M), c) s x :=
 times_cont_mdiff_at_const.times_cont_mdiff_within_at
 
+@[to_additive]
+lemma times_cont_mdiff_within_at_one [has_one M'] :
+  times_cont_mdiff_within_at I I' n (1 : M → M') s x :=
+times_cont_mdiff_at_const.times_cont_mdiff_within_at
+
 lemma smooth_within_at_const : smooth_within_at I I' (λ (x : M), c) s x :=
 times_cont_mdiff_within_at_const
 
+@[to_additive]
+lemma smooth_within_at_one [has_one M'] : smooth_within_at I I' (1 : M → M') s x :=
+times_cont_mdiff_within_at_one
+
 end id
 
 lemma times_cont_mdiff_of_support {f : M → F}

src/geometry/manifold/times_cont_mdiff_map.lean

@@ -56,6 +56,10 @@ attribute [to_additive_ignore_args 21] times_cont_mdiff_map
   times_cont_mdiff_map.has_coe_to_fun times_cont_mdiff_map.continuous_map.has_coe
 variables {f g : C^n⟮I, M; I', M'⟯}
 
+@[simp] lemma coe_fn_mk (f : M → M') (hf : times_cont_mdiff I I' n f) :
+  (mk f hf : M → M') = f :=
+rfl
+
 protected lemma times_cont_mdiff (f : C^n⟮I, M; I', M'⟯) :
   times_cont_mdiff I I' n f := f.times_cont_mdiff_to_fun
 

src/geometry/manifold/whitney_embedding.lean

@@ -23,8 +23,8 @@ for sufficiently large `n` there exists a smooth embedding `M → ℝ^n`.
 partition of unity, smooth bump function, whitney theorem
 -/
 
-universes uE uF uH uM
-variables
+universes uι uE uH uM
+variables {ι : Type uι}
 {E : Type uE} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E]
 {H : Type uH} [topological_space H] {I : model_with_corners ℝ E H}
 {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
@@ -36,78 +36,81 @@ noncomputable theory
 
 namespace smooth_bump_covering
 
-variables {s : set M} {U : M → set M} (fs : smooth_bump_covering I s)
+/-!
+### Whitney embedding theorem
+
+In this section we prove a version of the Whitney embedding theorem: for any compact real manifold
+`M`, for sufficiently large `n` there exists a smooth embedding `M → ℝ^n`.
+-/
 
-variables [t2_space M] [fintype fs.ι] (f : smooth_bump_covering I (univ : set M))
-  [fintype f.ι]
+variables [t2_space M] [fintype ι] {s : set M} (f : smooth_bump_covering ι I M s)
 
-/-- Smooth embedding of `M` into `(E × ℝ) ^ f.ι`. -/
-def embedding_pi_tangent : C^∞⟮I, M; 𝓘(ℝ, fs.ι → (E × ℝ)), fs.ι → (E × ℝ)⟯ :=
-{ to_fun := λ x i, (fs i x • ext_chart_at I (fs.c i) x, fs i x),
+/-- Smooth embedding of `M` into `(E × ℝ) ^ ι`. -/
+def embedding_pi_tangent : C^∞⟮I, M; 𝓘(ℝ, ι → (E × ℝ)), ι → (E × ℝ)⟯ :=
+{ to_fun := λ x i, (f i x • ext_chart_at I (f.c i) x, f i x),
   times_cont_mdiff_to_fun := times_cont_mdiff_pi_space.2 $ λ i,
-    ((fs i).smooth_smul times_cont_mdiff_on_ext_chart_at).prod_mk_space ((fs i).smooth) }
+    ((f i).smooth_smul times_cont_mdiff_on_ext_chart_at).prod_mk_space ((f i).smooth) }
 
 local attribute [simp] lemma embedding_pi_tangent_coe :
-  ⇑fs.embedding_pi_tangent = λ x i, (fs i x • ext_chart_at I (fs.c i) x, fs i x) :=
+  ⇑f.embedding_pi_tangent = λ x i, (f i x • ext_chart_at I (f.c i) x, f i x) :=
 rfl
 
-lemma embedding_pi_tangent_inj_on : inj_on fs.embedding_pi_tangent s :=
+lemma embedding_pi_tangent_inj_on : inj_on f.embedding_pi_tangent s :=
 begin
   intros x hx y hy h,
   simp only [embedding_pi_tangent_coe, funext_iff] at h,
-  obtain ⟨h₁, h₂⟩ := prod.mk.inj_iff.1 (h (fs.ind x hx)),
-  rw [fs.apply_ind x hx] at h₂,
-  rw [← h₂, fs.apply_ind x hx, one_smul, one_smul] at h₁,
-  have := fs.mem_ext_chart_at_source_of_eq_one h₂.symm,
-  exact (ext_chart_at I (fs.c _)).inj_on (fs.mem_ext_chart_at_ind_source x hx) this h₁
+  obtain ⟨h₁, h₂⟩ := prod.mk.inj_iff.1 (h (f.ind x hx)),
+  rw [f.apply_ind x hx] at h₂,
+  rw [← h₂, f.apply_ind x hx, one_smul, one_smul] at h₁,
+  have := f.mem_ext_chart_at_source_of_eq_one h₂.symm,
+  exact (ext_chart_at I (f.c _)).inj_on (f.mem_ext_chart_at_ind_source x hx) this h₁
 end
 
-lemma embedding_pi_tangent_injective :
+lemma embedding_pi_tangent_injective (f : smooth_bump_covering ι I M) :
   injective f.embedding_pi_tangent :=
 injective_iff_inj_on_univ.2 f.embedding_pi_tangent_inj_on
 
 lemma comp_embedding_pi_tangent_mfderiv (x : M) (hx : x ∈ s) :
   ((continuous_linear_map.fst ℝ E ℝ).comp
-    (@continuous_linear_map.proj ℝ _ fs.ι (λ _, E × ℝ) _ _
-      (λ _, infer_instance) (fs.ind x hx))).comp
-      (mfderiv I 𝓘(ℝ, fs.ι → (E × ℝ)) fs.embedding_pi_tangent x) =
-  mfderiv I I (chart_at H (fs.c (fs.ind x hx))) x :=
+    (@continuous_linear_map.proj ℝ _ ι (λ _, E × ℝ) _ _
+      (λ _, infer_instance) (f.ind x hx))).comp
+      (mfderiv I 𝓘(ℝ, ι → (E × ℝ)) f.embedding_pi_tangent x) =
+  mfderiv I I (chart_at H (f.c (f.ind x hx))) x :=
 begin
   set L := ((continuous_linear_map.fst ℝ E ℝ).comp
-    (@continuous_linear_map.proj ℝ _ fs.ι (λ _, E × ℝ) _ _ (λ _, infer_instance) (fs.ind x hx))),
-  have := (L.has_mfderiv_at.comp x (fs.embedding_pi_tangent.mdifferentiable_at.has_mfderiv_at)),
+    (@continuous_linear_map.proj ℝ _ ι (λ _, E × ℝ) _ _ (λ _, infer_instance) (f.ind x hx))),
+  have := L.has_mfderiv_at.comp x f.embedding_pi_tangent.mdifferentiable_at.has_mfderiv_at,
   convert has_mfderiv_at_unique this _,
-  refine (has_mfderiv_at_ext_chart_at I (fs.mem_chart_at_ind_source x hx)).congr_of_eventually_eq _,
-  refine (fs.eventually_eq_one x hx).mono (λ y hy, _),
+  refine (has_mfderiv_at_ext_chart_at I (f.mem_chart_at_ind_source x hx)).congr_of_eventually_eq _,
+  refine (f.eventually_eq_one x hx).mono (λ y hy, _),
   simp only [embedding_pi_tangent_coe, continuous_linear_map.coe_comp', (∘),
     continuous_linear_map.coe_fst', continuous_linear_map.proj_apply],
   rw [hy, pi.one_apply, one_smul]
 end
 
 lemma embedding_pi_tangent_ker_mfderiv (x : M) (hx : x ∈ s) :
-  (mfderiv I 𝓘(ℝ, fs.ι → (E × ℝ)) fs.embedding_pi_tangent x).ker = ⊥ :=
+  (mfderiv I 𝓘(ℝ, ι → (E × ℝ)) f.embedding_pi_tangent x).ker = ⊥ :=
 begin
   apply bot_unique,
-  rw [← (mdifferentiable_chart I (fs.c (fs.ind x hx))).ker_mfderiv_eq_bot
-    (fs.mem_chart_at_ind_source x hx), ← comp_embedding_pi_tangent_mfderiv],
+  rw [← (mdifferentiable_chart I (f.c (f.ind x hx))).ker_mfderiv_eq_bot
+    (f.mem_chart_at_ind_source x hx), ← comp_embedding_pi_tangent_mfderiv],
   exact linear_map.ker_le_ker_comp _ _
 end
 
 lemma embedding_pi_tangent_injective_mfderiv (x : M) (hx : x ∈ s) :
-  injective (mfderiv I 𝓘(ℝ, fs.ι → (E × ℝ)) fs.embedding_pi_tangent x) :=
-linear_map.ker_eq_bot.1 (fs.embedding_pi_tangent_ker_mfderiv x hx)
+  injective (mfderiv I 𝓘(ℝ, ι → (E × ℝ)) f.embedding_pi_tangent x) :=
+linear_map.ker_eq_bot.1 (f.embedding_pi_tangent_ker_mfderiv x hx)
 
 /-- Baby version of the Whitney weak embedding theorem: if `M` admits a finite covering by
 supports of bump functions, then for some `n` it can be immersed into the `n`-dimensional
 Euclidean space. -/
-lemma exists_immersion_finrank (f : smooth_bump_covering I (univ : set M))
-  [fintype f.ι] :
+lemma exists_immersion_euclidean (f : smooth_bump_covering ι I M) :
   ∃ (n : ℕ) (e : M → euclidean_space ℝ (fin n)), smooth I (𝓡 n) e ∧
     injective e ∧ ∀ x : M, injective (mfderiv I (𝓡 n) e x) :=
 begin
-  set F := euclidean_space ℝ (fin $ finrank ℝ (f.ι → (E × ℝ))),
+  set F := euclidean_space ℝ (fin $ finrank ℝ (ι → (E × ℝ))),
   letI : finite_dimensional ℝ (E × ℝ) := by apply_instance,
-  set eEF : (f.ι → (E × ℝ)) ≃L[ℝ] F :=
+  set eEF : (ι → (E × ℝ)) ≃L[ℝ] F :=
     continuous_linear_equiv.of_finrank_eq finrank_euclidean_space_fin.symm,
   refine ⟨_, eEF ∘ f.embedding_pi_tangent,
     eEF.to_diffeomorph.smooth.comp f.embedding_pi_tangent.smooth,
@@ -122,11 +125,13 @@ end smooth_bump_covering
 /-- Baby version of the Whitney weak embedding theorem: if `M` admits a finite covering by
 supports of bump functions, then for some `n` it can be embedded into the `n`-dimensional
 Euclidean space. -/
-lemma exists_embedding_finrank_of_compact [t2_space M] [compact_space M] :
+lemma exists_embedding_euclidean_of_compact [t2_space M] [compact_space M] :
   ∃ (n : ℕ) (e : M → euclidean_space ℝ (fin n)), smooth I (𝓡 n) e ∧
     closed_embedding e ∧ ∀ x : M, injective (mfderiv I (𝓡 n) e x) :=
 begin
-  rcases (smooth_bump_covering.choice I M).exists_immersion_finrank
-    with ⟨n, e, hsmooth, hinj, hinj_mfderiv⟩,
+  rcases smooth_bump_covering.exists_is_subordinate I is_closed_univ (λ (x : M) _, univ_mem_sets)
+    with ⟨ι, f, -⟩,
+  haveI := f.fintype,
+  rcases f.exists_immersion_euclidean with ⟨n, e, hsmooth, hinj, hinj_mfderiv⟩,
   exact ⟨n, e, hsmooth, hsmooth.continuous.closed_embedding hinj, hinj_mfderiv⟩
 end

src/topology/paracompact.lean

@@ -38,9 +38,7 @@ We also prove the following facts.
 
 ## TODO
 
-* Define partition of unity.
-
-* Prove (some of) [Michael's theorems](https://ncatlab.org/nlab/show/Michael%27s+theorem).
+Prove (some of) [Michael's theorems](https://ncatlab.org/nlab/show/Michael%27s+theorem).
 
 ## Tags