feat(geometry/manifold/smooth_manifold_with_corners): product of smoo…

…th manifolds with corners (#3250)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/analysis/calculus/times_cont_diff.lean

@@ -1248,12 +1248,26 @@ The first projection in a product is `C^∞`.
 lemma times_cont_diff_fst {n : with_top ℕ} : times_cont_diff 𝕜 n (prod.fst : E × F → E) :=
 is_bounded_linear_map.times_cont_diff is_bounded_linear_map.fst
 
+/--
+The first projection on a domain in a product is `C^∞`.
+-/
+lemma times_cont_diff_on_fst {s : set (E×F)} {n : with_top ℕ} :
+  times_cont_diff_on 𝕜 n (prod.fst : E × F → E) s :=
+times_cont_diff.times_cont_diff_on times_cont_diff_fst
+
 /--
 The second projection in a product is `C^∞`.
 -/
 lemma times_cont_diff_snd {n : with_top ℕ} : times_cont_diff 𝕜 n (prod.snd : E × F → F) :=
 is_bounded_linear_map.times_cont_diff is_bounded_linear_map.snd
 
+/--
+The second projection on a domain in a product is `C^∞`.
+-/
+lemma times_cont_diff_on_snd {s : set (E×F)} {n : with_top ℕ} :
+  times_cont_diff_on 𝕜 n (prod.snd : E × F → F) s :=
+times_cont_diff.times_cont_diff_on times_cont_diff_snd
+
 /--
 The identity is `C^∞`.
 -/
@@ -1574,6 +1588,18 @@ lemma times_cont_diff.comp {n : with_top ℕ} {g : F → G} {f : E → F}
 times_cont_diff_on_univ.1 $ times_cont_diff_on.comp (times_cont_diff_on_univ.2 hg)
   (times_cont_diff_on_univ.2 hf) (subset_univ _)
 
+/-- The product map of two `C^n` functions is `C^n`. -/
+lemma times_cont_diff_on.map_prod {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
+  {F' : Type*} [normed_group F'] [normed_space 𝕜 F']
+  {s : set E} {t : set E'} {n : with_top ℕ} {f : E → F} {g : E' → F'}
+  (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g t) :
+  times_cont_diff_on 𝕜 n (prod.map f g) (set.prod s t) :=
+begin
+  have hs : s.prod t ⊆ (prod.fst) ⁻¹' s := by { rintros x ⟨h_x_1, h_x_2⟩, exact h_x_1, },
+  have ht : s.prod t ⊆ (prod.snd) ⁻¹' t := by { rintros x ⟨h_x_1, h_x_2⟩, exact h_x_2, },
+  exact (hf.comp (times_cont_diff_on_fst) hs).prod (hg.comp (times_cont_diff_on_snd) ht),
+end
+
 /-- The bundled derivative of a `C^{n+1}` function is `C^n`. -/
 lemma times_cont_diff_on_fderiv_within_apply {m n : with_top  ℕ} {s : set E}
   {f : E → F} (hf : times_cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hmn : m + 1 ≤ n) :

src/data/prod.lean

@@ -19,18 +19,20 @@ variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 @[simp] theorem prod.exists {p : α × β → Prop} : (∃ x, p x) ↔ (∃ a b, p (a, b)) :=
 ⟨assume ⟨⟨a, b⟩, h⟩, ⟨a, b, h⟩, assume ⟨a, b, h⟩, ⟨⟨a, b⟩, h⟩⟩
 
+@[simp] lemma prod_map (f : α → γ) (g : β → δ) (p : α × β) : prod.map f g p = (f p.1, g p.2) := rfl
+
 namespace prod
 
 @[simp] lemma map_mk (f : α → γ) (g : β → δ) (a : α) (b : β) : map f g (a, b) = (f a, g b) := rfl
 
-@[simp] lemma map_fst (f : α → γ) (g : β → δ) (p : α × β) : (map f g p).1 = f (p.1) := rfl
+lemma map_fst (f : α → γ) (g : β → δ) (p : α × β) : (map f g p).1 = f (p.1) := rfl
 
-@[simp] lemma map_snd (f : α → γ) (g : β → δ) (p : α × β) : (map f g p).2 = g (p.2) := rfl
+lemma map_snd (f : α → γ) (g : β → δ) (p : α × β) : (map f g p).2 = g (p.2) := rfl
 
-@[simp] lemma map_fst' (f : α → γ) (g : β → δ) : (prod.fst ∘ map f g) = f ∘ prod.fst :=
+lemma map_fst' (f : α → γ) (g : β → δ) : (prod.fst ∘ map f g) = f ∘ prod.fst :=
 funext $ map_fst f g
 
-@[simp] lemma map_snd' (f : α → γ) (g : β → δ) : (prod.snd ∘ map f g) = g ∘ prod.snd :=
+lemma map_snd' (f : α → γ) (g : β → δ) : (prod.snd ∘ map f g) = g ∘ prod.snd :=
 funext $ map_snd f g
 
 @[simp] theorem mk.inj_iff {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ (a₁ = a₂ ∧ b₁ = b₂) :=

src/geometry/manifold/basic_smooth_bundle.lean

@@ -171,7 +171,7 @@ def to_topological_fiber_bundle_core : topological_fiber_bundle_core (atlas H M)
 
 /-- Local chart for the total space of a basic smooth bundle -/
 def chart {e : local_homeomorph M H} (he : e ∈ atlas H M) :
-  local_homeomorph (Z.to_topological_fiber_bundle_core.total_space) (H × F) :=
+  local_homeomorph (Z.to_topological_fiber_bundle_core.total_space) (model_prod H F) :=
 (Z.to_topological_fiber_bundle_core.local_triv ⟨e, he⟩).trans
   (local_homeomorph.prod e (local_homeomorph.refl F))
 
@@ -190,7 +190,7 @@ end
 
 /-- 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. -/
-instance to_charted_space : charted_space (H × F) Z.to_topological_fiber_bundle_core.total_space :=
+instance to_charted_space : charted_space (model_prod H F) Z.to_topological_fiber_bundle_core.total_space :=
 { atlas := ⋃(e : local_homeomorph M H) (he : e ∈ atlas H M), {Z.chart he},
   chart_at := λp, Z.chart (chart_mem_atlas H p.1),
   mem_chart_source := λp, by simp [mem_chart_source],
@@ -199,24 +199,24 @@ instance to_charted_space : charted_space (H × F) Z.to_topological_fiber_bundle
     exact ⟨chart_at H p.1, chart_mem_atlas H p.1, rfl⟩
   end }
 
-lemma mem_atlas_iff (f : local_homeomorph Z.to_topological_fiber_bundle_core.total_space (H × F)) :
-  f ∈ atlas (H × F) Z.to_topological_fiber_bundle_core.total_space ↔
+lemma mem_atlas_iff (f : local_homeomorph Z.to_topological_fiber_bundle_core.total_space (model_prod H F)) :
+  f ∈ atlas (model_prod H F) Z.to_topological_fiber_bundle_core.total_space ↔
   ∃(e : local_homeomorph M H) (he : e ∈ atlas H M), f = Z.chart he :=
 by simp only [atlas, mem_Union, mem_singleton_iff]
 
 @[simp, mfld_simps] lemma mem_chart_source_iff (p q : Z.to_topological_fiber_bundle_core.total_space) :
-  p ∈ (chart_at (H × F) q).source ↔ p.1 ∈ (chart_at H q.1).source :=
+  p ∈ (chart_at (model_prod H F) q).source ↔ p.1 ∈ (chart_at H q.1).source :=
 by simp only [chart_at] with mfld_simps
 
 @[simp, mfld_simps] lemma mem_chart_target_iff (p : H × F) (q : Z.to_topological_fiber_bundle_core.total_space) :
-  p ∈ (chart_at (H × F) q).target ↔ p.1 ∈ (chart_at H q.1).target :=
+  p ∈ (chart_at (model_prod H F) q).target ↔ p.1 ∈ (chart_at H q.1).target :=
 by simp only [chart_at] with mfld_simps
 
 @[simp, mfld_simps] lemma coe_chart_at_fst (p q : Z.to_topological_fiber_bundle_core.total_space) :
-  (((chart_at (H × F) q) : _ → H × F) p).1 = (chart_at H q.1 : _ → H) p.1 := rfl
+  (((chart_at (model_prod H F) q) : _ → model_prod H F) p).1 = (chart_at H q.1 : _ → H) p.1 := rfl
 
 @[simp, mfld_simps] lemma coe_chart_at_symm_fst (p : H × F) (q : Z.to_topological_fiber_bundle_core.total_space) :
-  (((chart_at (H × F) q).symm : H × F → Z.to_topological_fiber_bundle_core.total_space) p).1
+  (((chart_at (model_prod H F) q).symm : model_prod H F → Z.to_topological_fiber_bundle_core.total_space) p).1
   = ((chart_at H q.1).symm : H → M) p.1 := rfl
 
 /-- Smooth manifold structure on the total space of a basic smooth bundle -/
@@ -235,11 +235,8 @@ begin
   { 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,
-    { have : range (λ (p : H × F), (I (p.fst), id p.snd)) =
-             (range I).prod (range (id : F → F)) := prod_range_range_eq.symm,
-      simp only [id.def, range_id] with mfld_simps at this,
-      ext p,
-      simp only [J, chart, model_with_corners.prod, this] with mfld_simps,
+    { 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⟩ } },
@@ -497,7 +494,7 @@ variable (M)
 local attribute [reducible] tangent_bundle
 
 instance : topological_space (tangent_bundle I M) := by apply_instance
-instance : charted_space (H × E) (tangent_bundle I M) := by apply_instance
+instance : charted_space (model_prod H E) (tangent_bundle I M) := by apply_instance
 instance : smooth_manifold_with_corners I.tangent (tangent_bundle I M) := by apply_instance
 
 local attribute [reducible] tangent_space topological_fiber_bundle_core.fiber
@@ -529,7 +526,7 @@ topological_fiber_bundle_core.is_open_map_proj _
 
 /-- In the tangent bundle to the model space, the charts are just the identity-/
 @[simp, mfld_simps] lemma tangent_bundle_model_space_chart_at (p : tangent_bundle I H) :
-  (chart_at (H × E) p).to_local_equiv = local_equiv.refl (H × E) :=
+  (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,
@@ -540,26 +537,26 @@ begin
       exact model_with_corners.right_inv _ hy },
     rwa fderiv_within_id I.unique_diff_at_image at this },
   ext x : 1,
-  show (chart_at (H × E) p : tangent_bundle I H → H × E) x = (local_equiv.refl (H × E)) x,
+  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 },
-  show ∀ x, ((chart_at (H × E) p).to_local_equiv).symm x = (local_equiv.refl (H × E)).symm x,
+  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,
       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},
-  show ((chart_at (H × E) p).to_local_equiv).source = (local_equiv.refl (H × E)).source,
+  show ((chart_at (model_prod H E) p).to_local_equiv).source = (local_equiv.refl (model_prod H E)).source,
     by simp only [chart_at] with mfld_simps,
 end
 
 @[simp, mfld_simps] lemma tangent_bundle_model_space_coe_chart_at (p : tangent_bundle I H) :
-  (chart_at (H × E) p : tangent_bundle I H → H × E) = id :=
+  (chart_at (model_prod H E) p : tangent_bundle I H → model_prod H E) = id :=
 by { unfold_coes, simp only with mfld_simps }
 
 @[simp, mfld_simps] lemma tangent_bundle_model_space_coe_chart_at_symm (p : tangent_bundle I H) :
-  ((chart_at (H × E) p).symm : H × E → tangent_bundle I H) = id :=
+  ((chart_at (model_prod H E) p).symm : model_prod H E → tangent_bundle I H) = id :=
 by { unfold_coes, simp only with mfld_simps, refl }
 
 variable (H)
@@ -570,7 +567,7 @@ lemma tangent_bundle_model_space_topology_eq_prod :
 begin
   ext o,
   let x : tangent_bundle I H := (I.symm (0 : E), (0 : E)),
-  let e := chart_at (H × E) x,
+  let e := chart_at (model_prod H E) x,
   have e_source : e.source = univ, by { simp only with mfld_simps, refl },
   have e_target : e.target = univ, by { simp only with mfld_simps, refl },
   let e' := e.to_homeomorph_of_source_eq_univ_target_eq_univ e_source e_target,

src/geometry/manifold/charted_space.lean

@@ -11,7 +11,7 @@ import topology.local_homeomorph
 A smooth manifold is a topological space `M` locally modelled on a euclidean space (or a euclidean
 half-space for manifolds with boundaries, or an infinite dimensional vector space for more general
 notions of manifolds), i.e., the manifold is covered by open subsets on which there are local
-homeomorphisms (the charts) going to a model space`H`, and the changes of charts should be smooth
+homeomorphisms (the charts) going to a model space `H`, and the changes of charts should be smooth
 maps.
 
 In this file, we introduce a general framework describing these notions, where the model space is an
@@ -119,7 +119,7 @@ noncomputable theory
 open_locale classical
 universes u
 
-variables {H : Type u} {M : Type*} {M' : Type*} {M'' : Type*}
+variables {H : Type u} {H' : Type*} {M : Type*} {M' : Type*} {M'' : Type*}
 
 /- Notational shortcut for the composition of local homeomorphisms and local equivs, i.e.,
 `local_homeomorph.trans` and `local_equiv.trans`.
@@ -407,7 +407,71 @@ by simp [atlas, charted_space.atlas]
   chart_at H x = local_homeomorph.refl H :=
 by simpa using chart_mem_atlas H x
 
+/-- Same thing as `H × H'`. We introduce it for technical reasons: a charted space `M` with model `H`
+is a set of local charts from `M` to `H` covering the space. Every space is registered as a charted
+space over itself, using the only chart `id`, in `manifold_model_space`. You can also define a product
+of charted space `M` and `M'` (with model space `H × H'`) by taking the products of the charts. Now,
+on `H × H'`, there are two charted space structures with model space `H × H'` itself, the one coming
+from `manifold_model_space`, and the one coming from the product of the two `manifold_model_space` on
+each component. They are equal, but not defeq (because the product of `id` and `id` is not defeq to
+`id`), which is bad as we know. This expedient of renaming `H × H'` solves this problem. -/
+def model_prod (H : Type*) (H' : Type*) := H × H'
+
+section
+local attribute [reducible] model_prod
+
+instance model_prod_inhabited {α β : Type*} [inhabited α] [inhabited β] :
+  inhabited (model_prod α β) :=
+⟨(default α, default β)⟩
+
+instance (H : Type*) [topological_space H] (H' : Type*) [topological_space H'] :
+  topological_space (model_prod H H') :=
+by apply_instance
+
+/- Next lemma shows up often when dealing with derivatives, register it as simp. -/
+@[simp, mfld_simps] lemma model_prod_range_prod_id
+  {H : Type*} {H' : Type*} {α : Type*} (f : H → α) :
+  range (λ (p : model_prod H H'), (f p.1, p.2)) = set.prod (range f) univ :=
+by rw prod_range_univ_eq
+
+end
+
+/-- The product of two charted spaces is naturally a charted space, with the canonical
+construction of the atlas of product maps. -/
+instance prod_charted_space (H : Type*) [topological_space H]
+  (M : Type*) [topological_space M] [charted_space H M]
+  (H' : Type*) [topological_space H']
+  (M' : Type*) [topological_space M'] [charted_space H' M'] :
+  charted_space (model_prod H H') (M × M') :=
+{ atlas            :=
+    {f : (local_homeomorph (M×M') (model_prod H H')) |
+      ∃ g ∈ charted_space.atlas H M, ∃ h ∈ (charted_space.atlas H' M'),
+        f = local_homeomorph.prod g h},
+  chart_at         := λ x: (M × M'),
+    (charted_space.chart_at H x.1).prod (charted_space.chart_at H' x.2),
+  mem_chart_source :=
+  begin
+    intro x,
+    simp only with mfld_simps,
+  end,
+  chart_mem_atlas  :=
+  begin
+    intro x,
+    use (charted_space.chart_at H x.1),
+    split,
+    { apply chart_mem_atlas _, },
+    { use (charted_space.chart_at H' x.2), simp only [chart_mem_atlas, eq_self_iff_true, and_self], }
+  end }
+
+section prod_charted_space
+
 variables [topological_space H] [topological_space M] [charted_space H M]
+[topological_space H'] [topological_space M'] [charted_space H' M'] {x : M×M'}
+
+@[simp, mfld_simps] lemma prod_charted_space_chart_at :
+  (chart_at (model_prod H H') x) = (chart_at H x.fst).prod (chart_at H' x.snd) := rfl
+
+end prod_charted_space
 
 end charted_space
 

src/geometry/manifold/mfderiv.lean

@@ -1012,7 +1012,7 @@ mdifferentiable_of_mem_atlas _ (chart_mem_atlas _ _)
 
 /-- The derivative of the chart at a base point is the chart of the tangent bundle. -/
 lemma tangent_map_chart {p q : tangent_bundle I M} (h : q.1 ∈ (chart_at H p.1).source) :
-  tangent_map I I (chart_at H p.1) q = (chart_at (H × E) p : tangent_bundle I M → H × E) q :=
+  tangent_map I I (chart_at H p.1) q = (chart_at (model_prod H E) p : tangent_bundle I M → model_prod H E) q :=
 begin
   dsimp [tangent_map],
   rw mdifferentiable_at.mfderiv,
@@ -1022,10 +1022,10 @@ end
 
 /-- The derivative of the inverse of the chart at a base point is the inverse of the chart of the
 tangent bundle. -/
-lemma tangent_map_chart_symm {p : tangent_bundle I M} {q : H × E}
+lemma tangent_map_chart_symm {p : tangent_bundle I M} {q : model_prod H E}
   (h : q.1 ∈ (chart_at H p.1).target) :
   tangent_map I I (chart_at H p.1).symm q =
-  ((chart_at (H × E) p).symm : H × E → tangent_bundle I M) q :=
+  ((chart_at (model_prod H E) p).symm : model_prod H E → tangent_bundle I M) q :=
 begin
   dsimp only [tangent_map],
   rw mdifferentiable_at.mfderiv (mdifferentiable_at_atlas_symm _ (chart_mem_atlas _ _) h),
@@ -1358,7 +1358,7 @@ begin
   assume p hp,
   replace hp : p.fst ∈ s, by simpa only [] with mfld_simps using hp,
   let e₀ := chart_at H p.1,
-  let e := chart_at (H × F) p,
+  let e := chart_at (model_prod H F) p,
   -- It suffices to prove unique differentiability in a chart
   suffices h : unique_mdiff_on (I.prod (model_with_corners_self 𝕜 F))
     (e.target ∩ e.symm⁻¹' (Z.to_topological_fiber_bundle_core.proj ⁻¹' s)),
@@ -1377,13 +1377,13 @@ begin
   -- rewrite the relevant set in the chart as a direct product
   have : (λ (p : E × F), (I.symm p.1, p.snd)) ⁻¹' e.target ∩
          (λ (p : E × F), (I.symm p.1, p.snd)) ⁻¹' (e.symm ⁻¹' (prod.fst ⁻¹' s)) ∩
-         range (λ (p : H × F), (I p.1, p.snd))
+         ((range I).prod univ)
     = set.prod (I.symm ⁻¹' (e₀.target ∩ e₀.symm⁻¹' s) ∩ range I) univ,
   { ext q,
     split;
     { assume hq,
-      simp only [prod_range_univ_eq.symm] with mfld_simps at hq,
-      simp only [hq, prod_range_univ_eq.symm] with mfld_simps } },
+      simp only with mfld_simps at hq,
+      simp only [hq] with mfld_simps } },
   assume q hq,
   replace hq : q.1 ∈ (chart_at H p.1).target ∧ ((chart_at H p.1).symm : H → M) q.1 ∈ s,
     by simpa only [] with mfld_simps using hq,