feat(geometry/manifold): add charted_space and model_with_corners…

… for pi types (#6578)

Also use `set.image2` in the `charted_space` instance for `model_prod`.

src/data/equiv/local_equiv.lean

@@ -81,7 +81,7 @@ enough.
 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
+set.inter_subset_left set.mem_prod set.range_id set.range_prod_map 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 prod.map_mk
 set.preimage_inter heq_iff_eq equiv.sigma_equiv_prod_apply equiv.sigma_equiv_prod_symm_apply

src/geometry/manifold/charted_space.lean

@@ -542,27 +542,40 @@ end
 
 end
 
-/-- 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. -/
+/-- For technical reasons we introduce two type tags:
+
+* `model_prod H H'` is the same as `H × H'`;
+* `model_pi H` is the same as `Π i, H i`, where `H : ι → Type*` and `ι` is a finite type.
+
+In both cases the reason is the same, so we explain it only in the case of the product. 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. -/
+library_note "Manifold type tags"
+
+/-- Same thing as `H × H'` We introduce it for technical reasons,
+see note [Manifold type tags]. -/
 def model_prod (H : Type*) (H' : Type*) := H × H'
 
+/-- Same thing as `Π i, H i` We introduce it for technical reasons,
+see note [Manifold type tags]. -/
+def model_pi {ι : Type*} (H : ι → Type*) := Π i, H i
+
 section
 local attribute [reducible] model_prod
 
-instance model_prod_inhabited {α β : Type*} [inhabited α] [inhabited β] :
-  inhabited (model_prod α β) :=
-⟨(default α, default β)⟩
+instance model_prod_inhabited [inhabited H] [inhabited H'] :
+  inhabited (model_prod H H') :=
+prod.inhabited
 
 instance (H : Type*) [topological_space H] (H' : Type*) [topological_space H'] :
   topological_space (model_prod H H') :=
-by apply_instance
+prod.topological_space
 
 /- Next lemma shows up often when dealing with derivatives, register it as simp. -/
 @[simp, mfld_simps] lemma model_prod_range_prod_id
@@ -572,32 +585,31 @@ by rw prod_range_univ_eq
 
 end
 
+section
+
+variables {ι : Type*} {Hi : ι → Type*}
+
+instance model_pi_inhabited [Π i, inhabited (Hi i)] :
+  inhabited (model_pi Hi) :=
+pi.inhabited _
+
+instance [Π i, topological_space (Hi i)] :
+  topological_space (model_pi Hi) :=
+Pi.topological_space
+
+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, and_self, true_and] }
-  end }
+{ atlas            := image2 local_homeomorph.prod (atlas H M) (atlas H' M'),
+  chart_at         := λ x : M × M', (chart_at H x.1).prod (chart_at H' x.2),
+  mem_chart_source := λ x, ⟨mem_chart_source _ _, mem_chart_source _ _⟩,
+  chart_mem_atlas  := λ x, mem_image2_of_mem (chart_mem_atlas _ _) (chart_mem_atlas _ _) }
 
 section prod_charted_space
 
@@ -609,6 +621,21 @@ variables [topological_space H] [topological_space M] [charted_space H M]
 
 end prod_charted_space
 
+/-- The product of a finite family of charted spaces is naturally a charted space, with the
+canonical construction of the atlas of finite product maps. -/
+instance pi_charted_space {ι : Type*} [fintype ι] (H : ι → Type*) [Π i, topological_space (H i)]
+  (M : ι → Type*) [Π i, topological_space (M i)] [Π i, charted_space (H i) (M i)] :
+  charted_space (model_pi H) (Π i, M i) :=
+{ atlas := local_homeomorph.pi '' (set.pi univ $ λ i, atlas (H i) (M i)),
+  chart_at := λ f, local_homeomorph.pi $ λ i, chart_at (H i) (f i),
+  mem_chart_source := λ f i hi, mem_chart_source (H i) (f i),
+  chart_mem_atlas := λ f, mem_image_of_mem _ $ λ i hi, chart_mem_atlas (H i) (f i) }
+
+@[simp, mfld_simps] lemma pi_charted_space_chart_at {ι : Type*} [fintype ι] (H : ι → Type*)
+  [Π i, topological_space (H i)] (M : ι → Type*) [Π i, topological_space (M i)]
+  [Π i, charted_space (H i) (M i)] (f : Π i, M i) :
+  chart_at (model_pi H) f = local_homeomorph.pi (λ i, chart_at (H i) (f i)) := rfl
+
 end charted_space
 
 /-! ### Constructing a topology from an atlas -/

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -302,6 +302,20 @@ def model_with_corners.prod
   continuous_inv_fun := I.continuous_inv_fun.prod_map I'.continuous_inv_fun,
   .. I.to_local_equiv.prod I'.to_local_equiv }
 
+/-- Given a finite family of `model_with_corners` `I i` on `(E i, H i)`, we define the model with
+corners `pi I` on `(Π i, E i, model_pi H)`. See note [Manifold type tags] for explanation about
+`model_pi H`. -/
+def model_with_corners.pi
+  {𝕜 : Type u} [nondiscrete_normed_field 𝕜] {ι : Type v} [fintype ι]
+  {E : ι → Type w} [Π i, normed_group (E i)] [Π i, normed_space 𝕜 (E i)]
+  {H : ι → Type u'} [Π i, topological_space (H i)] (I : Π i, model_with_corners 𝕜 (E i) (H i)) :
+  model_with_corners 𝕜 (Π i, E i) (model_pi H) :=
+{ to_local_equiv := local_equiv.pi (λ i, (I i).to_local_equiv),
+  source_eq := by simp only [set.pi_univ] with mfld_simps,
+  unique_diff' := unique_diff_on.pi ι E _ _ (λ i _, (I i).unique_diff'),
+  continuous_to_fun := continuous_pi $ λ i, (I i).continuous.comp (continuous_apply i),
+  continuous_inv_fun := continuous_pi $ λ i, (I i).continuous_symm.comp (continuous_apply i) }
+
 /-- Special case of product model with corners, which is trivial on the second factor. This shows up
 as the model to tangent bundles. -/
 @[reducible] def model_with_corners.tangent
@@ -602,8 +616,8 @@ instance prod {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
   smooth_manifold_with_corners (I.prod I') (M×M') :=
 { compatible :=
   begin
-    rintros f g ⟨f1, hf1, f2, hf2, hf⟩ ⟨g1, hg1, g2, hg2, hg⟩,
-    rw [hf, hg, local_homeomorph.prod_symm, local_homeomorph.prod_trans],
+    rintros f g ⟨f1, f2, hf1, hf2, rfl⟩ ⟨g1, g2, hg1, hg2, rfl⟩,
+    rw [local_homeomorph.prod_symm, local_homeomorph.prod_trans],
     have h1 := has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) hf1 hg1,
     have h2 := has_groupoid.compatible (times_cont_diff_groupoid ⊤ I') hf2 hg2,
     exact times_cont_diff_groupoid_prod h1 h2,