feat(geometry/manifold/smooth_manifold_with_corners): properties to p…

…rove smoothness of mfderiv (#15523)

* Define `achart`
* Rename and reformulate `mem_maximal_atlas_of_mem_atlas -> subset_maximal_atlas`
* Used to prove smoothness of `mfderiv` (that result still has to be generalized to `mfderiv_within`, so is not included yet)
* From the sphere eversion project

src/geometry/manifold/charted_space.lean

@@ -503,6 +503,16 @@ lemma chart_source_mem_nhds (x : M) : (chart_at H x).source ∈ 𝓝 x :=
 lemma chart_target_mem_nhds (x : M) : (chart_at H x).target ∈ 𝓝 (chart_at H x x) :=
 (chart_at H x).open_target.mem_nhds $ mem_chart_target H x
 
+/-- `achart H x` is the chart at `x`, considered as an element of the atlas.
+Especially useful for working with `basic_smooth_vector_bundle_core` -/
+def achart (x : M) : atlas H M := ⟨chart_at H x, chart_mem_atlas H x⟩
+
+lemma achart_def (x : M) : achart H x = ⟨chart_at H x, chart_mem_atlas H x⟩ := rfl
+@[simp, mfld_simps]
+lemma coe_achart (x : M) : (achart H x : local_homeomorph M H) = chart_at H x := rfl
+@[simp, mfld_simps]
+lemma achart_val (x : M) : (achart H x).1 = chart_at H x := rfl
+
 open topological_space
 
 lemma charted_space.second_countable_of_countable_cover [second_countable_topology H]
@@ -792,13 +802,13 @@ def structure_groupoid.maximal_atlas : set (local_homeomorph M H) :=
 variable {M}
 
 /-- The elements of the atlas belong to the maximal atlas for any structure groupoid -/
-lemma structure_groupoid.mem_maximal_atlas_of_mem_atlas [has_groupoid M G]
-  {e : local_homeomorph M H} (he : e ∈ atlas H M) : e ∈ G.maximal_atlas M :=
-λ e' he', ⟨G.compatible he he', G.compatible he' he⟩
+lemma structure_groupoid.subset_maximal_atlas [has_groupoid M G] :
+  atlas H M ⊆ G.maximal_atlas M :=
+λ e he e' he', ⟨G.compatible he he', G.compatible he' he⟩
 
 lemma structure_groupoid.chart_mem_maximal_atlas [has_groupoid M G]
   (x : M) : chart_at H x ∈ G.maximal_atlas M :=
-G.mem_maximal_atlas_of_mem_atlas (chart_mem_atlas H x)
+G.subset_maximal_atlas (chart_mem_atlas H x)
 
 variable {G}
 
@@ -835,7 +845,7 @@ 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)
+G.subset_maximal_atlas $ by simp
 
 end maximal_atlas
 

src/geometry/manifold/cont_mdiff.lean

@@ -719,6 +719,18 @@ lemma cont_mdiff_at_iff_cont_mdiff_on_nhds {n : ℕ} :
 by simp [← cont_mdiff_within_at_univ, cont_mdiff_within_at_iff_cont_mdiff_on_nhds,
   nhds_within_univ]
 
+/-- Note: This does not hold for `n = ∞`. `f` being `C^∞` at `x` means that for every `n`, `f` is
+`C^n` on some neighborhood of `x`, but this neighborhood can depend on `n`. -/
+lemma cont_mdiff_at_iff_cont_mdiff_at_nhds {n : ℕ} :
+  cont_mdiff_at I I' n f x ↔ ∀ᶠ x' in 𝓝 x, cont_mdiff_at I I' n f x' :=
+begin
+  refine ⟨_, λ h, h.self_of_nhds⟩,
+  rw [cont_mdiff_at_iff_cont_mdiff_on_nhds],
+  rintro ⟨u, hu, h⟩,
+  refine (eventually_mem_nhds.mpr hu).mono (λ x' hx', _),
+  exact (h x' $ mem_of_mem_nhds hx').cont_mdiff_at hx'
+end
+
 omit Is I's
 
 /-! ### Congruence lemmas -/

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -113,12 +113,11 @@ noncomputable theory
 
 universes u v w u' v' w'
 
-open set filter
+open set filter function
 open_locale manifold filter topological_space
 
 localized "notation `∞` := (⊤ : with_top ℕ)" in manifold
 
-section model_with_corners
 /-! ### Models with corners. -/
 
 /-- A structure containing informations on the way a space `H` embeds in a
@@ -213,7 +212,10 @@ protected lemma unique_diff : unique_diff_on 𝕜 (range I) := I.target_eq ▸ I
 @[simp, mfld_simps] protected lemma left_inv (x : H) : I.symm (I x) = x :=
 by { refine I.left_inv' _, simp }
 
-protected lemma left_inverse : function.left_inverse I.symm I := I.left_inv
+protected lemma left_inverse : left_inverse I.symm I := I.left_inv
+
+lemma injective : injective I :=
+I.left_inverse.injective
 
 @[simp, mfld_simps] lemma symm_comp_self : I.symm ∘ I = id :=
 I.left_inverse.comp_eq_id
@@ -542,8 +544,6 @@ end
 
 end cont_diff_groupoid
 
-end model_with_corners
-
 section smooth_manifold_with_corners
 
 /-! ### Smooth manifolds with corners -/
@@ -603,9 +603,9 @@ def maximal_atlas := (cont_diff_groupoid ∞ I).maximal_atlas M
 
 variable {M}
 
-lemma mem_maximal_atlas_of_mem_atlas [smooth_manifold_with_corners I M]
-  {e : local_homeomorph M H} (he : e ∈ atlas H M) : e ∈ maximal_atlas I M :=
-structure_groupoid.mem_maximal_atlas_of_mem_atlas _ he
+lemma subset_maximal_atlas [smooth_manifold_with_corners I M] :
+  atlas H M ⊆ maximal_atlas I M :=
+structure_groupoid.subset_maximal_atlas _
 
 lemma chart_mem_maximal_atlas [smooth_manifold_with_corners I M] (x : M) :
   chart_at H x ∈ maximal_atlas I M :=
@@ -708,6 +708,11 @@ by { rw ext_chart_at_source, exact (chart_at H x).open_source }
 lemma mem_ext_chart_source : x ∈ (ext_chart_at I x).source :=
 by simp only [ext_chart_at_source, mem_chart_source]
 
+lemma ext_chart_at_target (x : M) : (ext_chart_at I x).target =
+  I.symm ⁻¹' (chart_at H x).target ∩ range I :=
+by simp_rw [ext_chart_at, local_equiv.trans_target, I.target_eq, I.to_local_equiv_coe_symm,
+  inter_comm]
+
 lemma ext_chart_at_to_inv :
   (ext_chart_at I x).symm ((ext_chart_at I x) x) = x :=
 (ext_chart_at I x).left_inv (mem_ext_chart_source I x)
@@ -873,6 +878,13 @@ lemma ext_chart_preimage_mem_nhds_within (ht : t ∈ 𝓝[s] x) :
     𝓝[(ext_chart_at I x).symm ⁻¹' s ∩ range I] ((ext_chart_at I x) x) :=
 ext_chart_preimage_mem_nhds_within' I x (mem_ext_chart_source I x) ht
 
+lemma ext_chart_preimage_mem_nhds' {x' : M} (h : x' ∈ (ext_chart_at I x).source) (ht : t ∈ 𝓝 x') :
+  (ext_chart_at I x).symm ⁻¹' t ∈ 𝓝 (ext_chart_at I x x') :=
+begin
+  apply (ext_chart_continuous_at_symm' I x h).preimage_mem_nhds,
+  rwa (ext_chart_at I x).left_inv h
+end
+
 /-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point
 is a neighborhood of the preimage. -/
 lemma ext_chart_preimage_mem_nhds (ht : t ∈ 𝓝 x) :
@@ -889,11 +901,41 @@ lemma ext_chart_preimage_inter_eq :
   = ((ext_chart_at I x).symm ⁻¹' s ∩ range I) ∩ ((ext_chart_at I x).symm ⁻¹' t) :=
 by mfld_set_tac
 
-end extended_charts
+/-! We use the name `ext_coord_change` for `(ext_chart_at I x').symm ≫ ext_chart_at I x`. -/
+
+lemma ext_coord_change_source (x x' : M) :
+  ((ext_chart_at I x').symm ≫ ext_chart_at I x).source =
+  I '' ((chart_at H x').symm ≫ₕ (chart_at H x)).source :=
+by { simp_rw [local_equiv.trans_source, I.image_eq, ext_chart_at_source, local_equiv.symm_source,
+      ext_chart_at_target, inter_right_comm _ (range I)], refl }
+
+lemma cont_diff_on_ext_coord_change [smooth_manifold_with_corners I M] (x x' : M) :
+  cont_diff_on 𝕜 ⊤ (ext_chart_at I x ∘ (ext_chart_at I x').symm)
+  ((ext_chart_at I x').symm ≫ ext_chart_at I x).source :=
+by { rw [ext_coord_change_source, I.image_eq], exact (has_groupoid.compatible
+  (cont_diff_groupoid ⊤ I) (chart_mem_atlas H x') (chart_mem_atlas H x)).1 }
+
+lemma cont_diff_within_at_ext_coord_change [smooth_manifold_with_corners I M] (x x' : M) {y : E}
+  (hy : y ∈ ((ext_chart_at I x').symm ≫ ext_chart_at I x).source) :
+  cont_diff_within_at 𝕜 ⊤ (ext_chart_at I x ∘ (ext_chart_at I x').symm) (range I) y :=
+begin
+  apply (cont_diff_on_ext_coord_change I x x' y hy).mono_of_mem,
+  rw [ext_coord_change_source] at hy ⊢,
+  obtain ⟨z, hz, rfl⟩ := hy,
+  exact I.image_mem_nhds_within ((local_homeomorph.open_source _).mem_nhds hz)
+end
+
+variable (𝕜)
+
+lemma ext_chart_self_eq {x : H} : ⇑(ext_chart_at I x) = I := rfl
+lemma ext_chart_self_apply {x y : H} : ext_chart_at I x y = I y := rfl
 
 /-- In the case of the manifold structure on a vector space, the extended charts are just the
 identity.-/
-lemma ext_chart_model_space_eq_id (𝕜 : Type*) [nontrivially_normed_field 𝕜]
-  {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E] (x : E) :
-  ext_chart_at (model_with_corners_self 𝕜 E) x = local_equiv.refl E :=
+lemma ext_chart_model_space_eq_id (x : E) : ext_chart_at 𝓘(𝕜, E) x = local_equiv.refl E :=
 by simp only with mfld_simps
+
+lemma ext_chart_model_space_apply {x y : E} : ext_chart_at 𝓘(𝕜, E) x y = y := rfl
+
+
+end extended_charts

src/geometry/manifold/tangent_bundle.lean

@@ -153,7 +153,7 @@ end
 def to_topological_vector_bundle_core : topological_vector_bundle_core 𝕜 M F (atlas H M) :=
 { base_set := λ i, i.1.source,
   is_open_base_set := λ i, i.1.open_source,
-  index_at := λ x, ⟨chart_at H x, chart_mem_atlas H x⟩,
+  index_at := achart H,
   mem_base_set_at := λ x, mem_chart_source H x,
   coord_change := λ i j x, Z.coord_change i j (i.1 x),
   coord_change_self := λ i x hx v, Z.coord_change_self i (i.1 x) (i.1.map_source hx) v,