feat(geometry/manifold/times_cont_mdiff): smooth functions between ma…

…nifolds (#3387)

We define smooth functions between smooth manifolds, and prove their basic properties (including the facts that a composition of smooth functions is smooth, and that the tangent map of a smooth map is smooth).

To avoid reproving always the same stuff in manifolds, we build a general theory of local invariant properties in the model space (i.e., properties which are local, and invariant under the structure groupoids) and show that the lift of such properties to charted spaces automatically inherit all the good behavior of the original property. We apply this general machinery to prove most basic properties of smooth functions between manifolds.

src/analysis/calculus/fderiv.lean

@@ -682,7 +682,7 @@ end
 lemma filter.eventually_eq.fderiv_eq (hL : f₁ =ᶠ[𝓝 x] f) :
   fderiv 𝕜 f₁ x = fderiv 𝕜 f x :=
 begin
-  have A : f₁ x = f x := (mem_of_nhds hL : _),
+  have A : f₁ x = f x := hL.eq_of_nhds,
   rw [← fderiv_within_univ, ← fderiv_within_univ],
   rw ← nhds_within_univ at hL,
   exact hL.fderiv_within_eq unique_diff_within_at_univ A

src/data/equiv/local_equiv.lean

@@ -70,6 +70,37 @@ its output. The list of lemmas should be reasonable (contrary to the output of
 enough.
 "
 
+-- register in the simpset `mfld_simps` several lemmas that are often useful when dealing
+-- with manifolds
+attribute [mfld_simps] id.def function.comp.left_id set.mem_set_of_eq set.image_eq_empty
+set.univ_inter set.preimage_univ set.prod_mk_mem_set_prod_eq and_true set.mem_univ
+set.mem_image_of_mem true_and set.mem_inter_eq set.mem_preimage function.comp_app
+set.inter_subset_left set.mem_prod set.range_id and_self set.mem_range_self
+eq_self_iff_true forall_const forall_true_iff set.inter_univ set.preimage_id function.comp.right_id
+not_false_iff and_imp set.prod_inter_prod set.univ_prod_univ true_or or_true
+
+namespace tactic.interactive
+
+/-- A very basic tactic to show that sets showing up in manifolds coincide or are included in
+one another. -/
+meta def mfld_set_tac : tactic unit := do
+  goal ← tactic.target,
+  match goal with
+  | `(%%e₁ = %%e₂) :=
+      `[ext my_y,
+        split;
+        { assume h_my_y,
+          try { simp only [*, -h_my_y] with mfld_simps at h_my_y },
+          simp only [*] with mfld_simps }]
+  | `(%%e₁ ⊆ %%e₂) :=
+      `[assume my_y h_my_y,
+        try { simp only [*, -h_my_y] with mfld_simps at h_my_y },
+        simp only [*] with mfld_simps]
+  | _ := tactic.fail "goal should be an equality or an inclusion"
+  end
+
+end tactic.interactive
+
 open function set
 
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
@@ -202,7 +233,7 @@ e.symm.image_inter_source_eq' _
 lemma source_inter_preimage_inv_preimage (s : set α) :
   e.source ∩ e ⁻¹' (e.symm ⁻¹' s) = e.source ∩ s :=
 begin
-  ext, split,
+  ext x, split,
   { rintros ⟨hx, xs⟩,
     simp only [mem_preimage, hx, e.left_inv, mem_preimage] at xs,
     exact ⟨hx, xs⟩ },
@@ -247,18 +278,12 @@ protected def restr (s : set α) : local_equiv α β :=
   source  := e.source ∩ s,
   target  := e.target ∩ e.symm⁻¹' s,
   map_source'  := λx hx, begin
-    apply mem_inter,
-    { apply e.map_source,
-      exact hx.1 },
-    { rw [mem_preimage, e.left_inv],
-      exact hx.2,
-      exact hx.1 },
+    simp only with mfld_simps at hx,
+    simp only [hx] with mfld_simps,
   end,
   map_target' := λy hy, begin
-    apply mem_inter,
-    { apply e.map_target,
-      exact hy.1 },
-    { exact hy.2 },
+    simp only with mfld_simps at hy,
+    simp only [hy] with mfld_simps,
   end,
   left_inv'  := λx hx, e.left_inv hx.1,
   right_inv' := λy hy, e.right_inv hy.1 }
@@ -332,15 +357,7 @@ by cases e; cases e'; refl
 @[simp, mfld_simps] lemma trans_source : (e.trans e').source = e.source ∩ e ⁻¹' e'.source := rfl
 
 lemma trans_source' : (e.trans e').source = e.source ∩ e ⁻¹' (e.target ∩ e'.source) :=
-begin
-  symmetry, calc
-    e.source ∩ e ⁻¹' (e.target ∩ e'.source) =
-    (e.source ∩ e ⁻¹' (e.target)) ∩ e ⁻¹' (e'.source) :
-      by rw [preimage_inter, inter_assoc]
-    ... = e.source ∩ e ⁻¹' (e'.source) :
-      by { congr' 1, apply inter_eq_self_of_subset_left e.source_subset_preimage_target }
-    ... = (e.trans e').source : rfl
-end
+by mfld_set_tac
 
 lemma trans_source'' : (e.trans e').source = e.symm '' (e.target ∩ e'.source) :=
 by rw [e.trans_source', inter_comm e.target, e.symm_image_inter_target_eq]
@@ -461,11 +478,10 @@ to the source -/
 lemma trans_self_symm :
   e.trans e.symm ≈ local_equiv.of_set e.source :=
 begin
-  have A : (e.trans e.symm).source = e.source,
-    by simp [trans_source, inter_eq_self_of_subset_left (source_subset_preimage_target _)],
+  have A : (e.trans e.symm).source = e.source, by mfld_set_tac,
   refine ⟨by simp [A], λx hx, _⟩,
   rw A at hx,
-  simp [hx]
+  simp only [hx] with mfld_simps
 end
 
 /-- Composition of the inverse of a local equiv and this local equiv is equivalent to the

src/geometry/manifold/basic_smooth_bundle.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import topology.topological_fiber_bundle
 import geometry.manifold.smooth_manifold_with_corners
+
 /-!
 # Basic smooth bundles
 
@@ -82,6 +83,7 @@ noncomputable theory
 universe u
 
 open topological_space set
+open_locale manifold
 
 /-- Core structure used to create a smooth bundle above `M` (a manifold over the model with
 corner `I`) with fiber the normed vector space `F` over `𝕜`, which is trivial in the chart domains
@@ -101,7 +103,7 @@ structure basic_smooth_bundle_core {𝕜 : Type*} [nondiscrete_normed_field 𝕜
   ∀ x ∈ ((i.1.symm.trans j.1).trans (j.1.symm.trans k.1)).source, ∀ v,
   (coord_change j k ((i.1.symm.trans j.1) x)) (coord_change i j x v) = coord_change i k x v)
 (coord_change_smooth : ∀ i j : atlas H M,
-  times_cont_diff_on 𝕜 ⊤ (λp : E × F, coord_change i j (I.symm p.1) p.2)
+  times_cont_diff_on 𝕜 ∞ (λp : E × F, coord_change i j (I.symm p.1) p.2)
   ((I '' (i.1.symm.trans j.1).source).prod (univ : set F)))
 
 
@@ -177,16 +179,11 @@ def chart {e : local_homeomorph M H} (he : e ∈ atlas H M) :
 
 @[simp, mfld_simps] lemma chart_source (e : local_homeomorph M H) (he : e ∈ atlas H M) :
   (Z.chart he).source = Z.to_topological_fiber_bundle_core.proj ⁻¹' e.source :=
-by { ext p, simp only [chart, mem_prod, and_self] with mfld_simps }
+by { simp only [chart, mem_prod], mfld_set_tac }
 
 @[simp, mfld_simps] lemma chart_target (e : local_homeomorph M H) (he : e ∈ atlas H M) :
   (Z.chart he).target = e.target.prod univ :=
-begin
-  simp only [chart] with mfld_simps,
-  ext p,
-  split;
-  simp {contextual := tt}
-end
+by { simp only [chart], mfld_set_tac }
 
 /-- The total space of a basic smooth bundle is endowed with a charted space structure, where the
 charts are in bijection with the charts of the basis. -/
@@ -229,32 +226,28 @@ begin
   suffices to prove the first statement in A below, and then glue back the pieces at the end. -/
   let J := model_with_corners.to_local_equiv (I.prod (model_with_corners_self 𝕜 F)),
   have A : ∀ (e e' : local_homeomorph M H) (he : e ∈ atlas H M) (he' : e' ∈ atlas H M),
-    times_cont_diff_on 𝕜 ⊤
+    times_cont_diff_on 𝕜 ∞
     (J ∘ ((Z.chart he).symm.trans (Z.chart he')) ∘ J.symm)
     (J.symm ⁻¹' ((Z.chart he).symm.trans (Z.chart he')).source ∩ range J),
   { assume e e' he he',
     have : J.symm ⁻¹' ((chart Z he).symm.trans (chart Z he')).source ∩ range J =
       (I.symm ⁻¹' (e.symm.trans e').source ∩ range I).prod univ,
-    { ext p,
-      simp only [J, chart, model_with_corners.prod] with mfld_simps,
-      split,
-      { tauto },
-      { exact λ⟨⟨hx1, hx2⟩, hx3⟩, ⟨⟨⟨hx1, e.map_target hx1⟩, hx2⟩, hx3⟩ } },
+      by { simp only [J, chart, model_with_corners.prod], mfld_set_tac },
     rw this,
     -- check separately that the two components of the coordinate change are smooth
     apply times_cont_diff_on.prod,
-    show times_cont_diff_on 𝕜 ⊤ (λ (p : E × F), (I ∘ e' ∘ e.symm ∘ I.symm) p.1)
+    show times_cont_diff_on 𝕜 ∞ (λ (p : E × F), (I ∘ e' ∘ e.symm ∘ I.symm) p.1)
          ((I.symm ⁻¹' (e.symm.trans e').source ∩ range I).prod (univ : set F)),
     { -- the coordinate change on the base is just a coordinate change for `M`, smooth since
       -- `M` is smooth
-      have A : times_cont_diff_on 𝕜 ⊤ (I ∘ (e.symm.trans e') ∘ I.symm)
+      have A : times_cont_diff_on 𝕜 ∞ (I ∘ (e.symm.trans e') ∘ I.symm)
         (I.symm ⁻¹' (e.symm.trans e').source ∩ range I) :=
-      (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) he he').1,
-      have B : times_cont_diff_on 𝕜 ⊤ (λp : E × F, p.1)
+      (has_groupoid.compatible (times_cont_diff_groupoid ∞ I) he he').1,
+      have B : times_cont_diff_on 𝕜 ∞ (λp : E × F, p.1)
         ((I.symm ⁻¹' (e.symm.trans e').source ∩ range I).prod univ) :=
       times_cont_diff_fst.times_cont_diff_on,
       exact times_cont_diff_on.comp A B (prod_subset_preimage_fst _ _) },
-    show times_cont_diff_on 𝕜 ⊤ (λ (p : E × F),
+    show times_cont_diff_on 𝕜 ∞ (λ (p : E × F),
       Z.coord_change ⟨chart_at H (e.symm (I.symm p.1)), _⟩ ⟨e', he'⟩
          ((chart_at H (e.symm (I.symm p.1)) : M → H) (e.symm (I.symm p.1)))
       (Z.coord_change ⟨e, he⟩ ⟨chart_at H (e.symm (I.symm p.1)), _⟩
@@ -276,7 +269,7 @@ begin
       have := Z.coord_change_comp ⟨e, he⟩ ⟨f, chart_mem_atlas _ _⟩ ⟨e', he'⟩ (I.symm x) A v,
       simpa only [] using this } },
   haveI : has_groupoid Z.to_topological_fiber_bundle_core.total_space
-         (times_cont_diff_groupoid ⊤ (I.prod (model_with_corners_self 𝕜 F))) :=
+         (times_cont_diff_groupoid ∞ (I.prod (model_with_corners_self 𝕜 F))) :=
   begin
     split,
     assume e₀ e₀' he₀ he₀',
@@ -307,13 +300,13 @@ def tangent_bundle_core : basic_smooth_bundle_core I M E :=
     /- To check that the coordinate change of the bundle is smooth, one should just use the
     smoothness of the charts, and thus the smoothness of their derivatives. -/
     rw model_with_corners.image,
-    have A : times_cont_diff_on 𝕜 ⊤
+    have A : times_cont_diff_on 𝕜 ∞
       (I ∘ (i.1.symm.trans j.1) ∘ I.symm)
       (I.symm ⁻¹' (i.1.symm.trans j.1).source ∩ range I) :=
-      (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) i.2 j.2).1,
+      (has_groupoid.compatible (times_cont_diff_groupoid ∞ I) i.2 j.2).1,
     have B : unique_diff_on 𝕜 (I.symm ⁻¹' (i.1.symm.trans j.1).source ∩ range I) :=
       I.unique_diff_preimage_source,
-    have C : times_cont_diff_on 𝕜 ⊤
+    have C : times_cont_diff_on 𝕜 ∞
       (λ (p : E × E), (fderiv_within 𝕜 (I ∘ j.1 ∘ i.1.symm ∘ I.symm)
             (I.symm ⁻¹' (i.1.symm.trans j.1).source ∩ range I) p.1 : E → E) p.2)
       ((I.symm ⁻¹' (i.1.symm.trans j.1).source ∩ range I).prod univ) :=
@@ -390,10 +383,10 @@ def tangent_bundle_core : basic_smooth_bundle_core I M E :=
       show differentiable_within_at 𝕜 (I ∘ j.1 ∘ i.1.symm ∘ I.symm)
         (I.symm ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I)
         (I x),
-      { have A : times_cont_diff_on 𝕜 ⊤
+      { have A : times_cont_diff_on 𝕜 ∞
           (I ∘ (i.1.symm.trans j.1) ∘ I.symm)
           (I.symm ⁻¹' (i.1.symm.trans j.1).source ∩ range I) :=
-        (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) i.2 j.2).1,
+        (has_groupoid.compatible (times_cont_diff_groupoid ∞ I) i.2 j.2).1,
         have B : differentiable_on 𝕜 (I ∘ j.1 ∘ i.1.symm ∘ I.symm)
           (I.symm ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I),
         { apply (A.differentiable_on le_top).mono,
@@ -405,10 +398,10 @@ def tangent_bundle_core : basic_smooth_bundle_core I M E :=
       show differentiable_within_at 𝕜 (I ∘ u.1 ∘ j.1.symm ∘ I.symm)
         (I.symm ⁻¹' (j.1.symm.trans u.1).source ∩ range I)
         ((I ∘ j.1 ∘ i.1.symm ∘ I.symm) (I x)),
-      { have A : times_cont_diff_on 𝕜 ⊤
+      { have A : times_cont_diff_on 𝕜 ∞
           (I ∘ (j.1.symm.trans u.1) ∘ I.symm)
           (I.symm ⁻¹' (j.1.symm.trans u.1).source ∩ range I) :=
-        (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) j.2 u.2).1,
+        (has_groupoid.compatible (times_cont_diff_groupoid ∞ I) j.2 u.2).1,
         apply A.differentiable_on le_top,
         rw [local_homeomorph.trans_source] at hx,
         simp only with mfld_simps,
@@ -528,8 +521,7 @@ topological_fiber_bundle_core.is_open_map_proj _
 @[simp, mfld_simps] lemma tangent_bundle_model_space_chart_at (p : tangent_bundle I H) :
   (chart_at (model_prod H E) p).to_local_equiv = local_equiv.refl (model_prod H E) :=
 begin
-  have A : ∀ x_fst, fderiv_within 𝕜 (I ∘ I.symm) (range I) (I x_fst)
-           = continuous_linear_map.id 𝕜 E,
+  have A : ∀ x_fst, fderiv_within 𝕜 (I ∘ I.symm) (range I) (I x_fst) = continuous_linear_map.id 𝕜 E,
   { assume x_fst,
     have : fderiv_within 𝕜 (I ∘ I.symm) (range I) (I x_fst)
          = fderiv_within 𝕜 id (range I) (I x_fst),
@@ -540,8 +532,8 @@ begin
   show (chart_at (model_prod H E) p : tangent_bundle I H → model_prod H E) x = (local_equiv.refl (model_prod H E)) x,
   { cases x,
     simp only [chart_at, basic_smooth_bundle_core.chart, topological_fiber_bundle_core.local_triv,
-      topological_fiber_bundle_core.local_triv', tangent_bundle_core, A, continuous_linear_map.coe_id',
-      basic_smooth_bundle_core.to_topological_fiber_bundle_core] with mfld_simps },
+      topological_fiber_bundle_core.local_triv', tangent_bundle_core, continuous_linear_map.coe_id',
+      basic_smooth_bundle_core.to_topological_fiber_bundle_core, A] with mfld_simps },
   show ∀ x, ((chart_at (model_prod H E) p).to_local_equiv).symm x = (local_equiv.refl (model_prod H E)).symm x,
   { rintros ⟨x_fst, x_snd⟩,
     simp only [chart_at, basic_smooth_bundle_core.chart, topological_fiber_bundle_core.local_triv,

src/geometry/manifold/charted_space.lean

@@ -107,14 +107,6 @@ In the locale `manifold`, we denote the composition of local homeomorphisms with
 composition of local equivs with `≫`.
 -/
 
--- register in the simpset `mfld_simps` several lemmas that are often useful
-attribute [mfld_simps] id.def function.comp.left_id set.mem_set_of_eq set.image_eq_empty
-set.univ_inter set.preimage_univ set.prod_mk_mem_set_prod_eq and_true set.mem_univ
-set.mem_image_of_mem true_and set.mem_inter_eq set.mem_preimage function.comp_app
-set.inter_subset_left set.mem_prod set.range_id and_self set.mem_range_self
-eq_self_iff_true forall_const forall_true_iff set.inter_univ set.preimage_id function.comp.right_id
-not_false_iff and_imp
-
 noncomputable theory
 open_locale classical
 universes u
@@ -233,12 +225,12 @@ def id_groupoid (H : Type u) [topological_space H] : structure_groupoid H :=
         exact ⟨hx, xs⟩ },
       cases hs,
       { replace hs : local_homeomorph.restr e s = local_homeomorph.refl H,
-          by simpa using hs,
+          by simpa only using hs,
         have : (e.restr s).source = univ, by { rw hs, simp },
         change (e.to_local_equiv).source ∩ interior s = univ at this,
         have : univ ⊆ interior s, by { rw ← this, exact inter_subset_right _ _ },
         have : s = univ, by rwa [interior_eq_of_open open_s, univ_subset_iff] at this,
-        simpa [this, restr_univ] using hs },
+        simpa only [this, restr_univ] using hs },
       { exfalso,
         rw mem_set_of_eq at hs,
         rwa hs at x's } },
@@ -326,7 +318,7 @@ def pregroupoid.groupoid (PG : pregroupoid H) : structure_groupoid H :=
       refl }
   end }
 
-lemma mem_groupoid_of_pregroupoid (PG : pregroupoid H) (e : local_homeomorph H H) :
+lemma mem_groupoid_of_pregroupoid {PG : pregroupoid H} {e : local_homeomorph H H} :
   e ∈ PG.groupoid ↔ PG.property e e.source ∧ PG.property e.symm e.target :=
 iff.rfl
 
@@ -471,20 +463,21 @@ attribute [simp, mfld_simps] mem_chart_source chart_mem_atlas
 section charted_space
 
 /-- Any space is a charted_space modelled over itself, by just using the identity chart -/
-instance manifold_model_space (H : Type*) [topological_space H] : charted_space H H :=
+instance charted_space_self (H : Type*) [topological_space H] : charted_space H H :=
 { atlas            := {local_homeomorph.refl H},
   chart_at         := λx, local_homeomorph.refl H,
   mem_chart_source := λx, mem_univ x,
   chart_mem_atlas  := λx, mem_singleton _ }
 
 /-- In the trivial charted_space structure of a space modelled over itself through the identity, the
 atlas members are just the identity -/
-@[simp, mfld_simps] lemma model_space_atlas {H : Type*} [topological_space H] {e : local_homeomorph H H} :
+@[simp, mfld_simps] lemma charted_space_self_atlas
+  {H : Type*} [topological_space H] {e : local_homeomorph H H} :
   e ∈ atlas H H ↔ e = local_homeomorph.refl H :=
 by simp [atlas, charted_space.atlas]
 
 /-- In the model space, chart_at is always the identity -/
-@[simp, mfld_simps] lemma chart_at_model_space_eq {H : Type*} [topological_space H] {x : H} :
+@[simp, mfld_simps] lemma chart_at_self_eq {H : Type*} [topological_space H] {x : H} :
   chart_at H x = local_homeomorph.refl H :=
 by simpa using chart_mem_atlas H x
 
@@ -673,15 +666,15 @@ lemma has_groupoid_of_pregroupoid (PG : pregroupoid H)
   (h : ∀{e e' : local_homeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M
     → PG.property (e.symm ≫ₕ e') (e.symm ≫ₕ e').source) :
   has_groupoid M (PG.groupoid) :=
-⟨assume e e' he he', (mem_groupoid_of_pregroupoid PG _).mpr ⟨h he he', h he' he⟩⟩
+⟨assume e e' he he', mem_groupoid_of_pregroupoid.mpr ⟨h he he', h he' he⟩⟩
 
 /-- The trivial charted space structure on the model space is compatible with any groupoid -/
 instance has_groupoid_model_space (H : Type*) [topological_space H] (G : structure_groupoid H) :
   has_groupoid H G :=
 { compatible := λe e' he he', begin
     replace he : e ∈ atlas H H := he,
     replace he' : e' ∈ atlas H H := he',
-    rw model_space_atlas at he he',
+    rw charted_space_self_atlas at he he',
     simp [he, he', structure_groupoid.id_mem]
   end }
 
@@ -745,6 +738,12 @@ begin
   exact G.eq_on_source C (setoid.symm D),
 end
 
+variable (G)
+
+/-- In the model space, the identity is in any maximal atlas. -/
+lemma structure_groupoid.id_mem_maximal_atlas : local_homeomorph.refl H ∈ G.maximal_atlas H :=
+G.mem_maximal_atlas_of_mem_atlas (by simp)
+
 end maximal_atlas
 
 section singleton