feat(geometry/manifold/*): "composition" of charted_space and `has_…

…groupoid` instances (#17305)

src/geometry/manifold/charted_space.lean

@@ -571,6 +571,17 @@ begin
     exact hsconn.is_preconnected.image _ ((E x).continuous_on_symm.mono hssubset) },
 end
 
+/-- If `M` is modelled on `H'` and `H'` is itself modelled on `H`, then we can consider `M` as being
+modelled on `H`. -/
+def charted_space.comp (H : Type*) [topological_space H] (H' : Type*) [topological_space H']
+  (M : Type*) [topological_space M] [charted_space H H'] [charted_space H' M] :
+  charted_space H M :=
+{ atlas := image2 local_homeomorph.trans (atlas H' M) (atlas H H'),
+  chart_at := λ p : M, (chart_at H' p).trans (chart_at H (chart_at H' p p)),
+  mem_chart_source := λ p, by simp only with mfld_simps,
+  chart_mem_atlas :=
+    λ p, ⟨chart_at H' p, chart_at H _, chart_mem_atlas H' p, chart_mem_atlas H _, rfl⟩ }
+
 end
 
 /-- For technical reasons we introduce two type tags:
@@ -867,6 +878,14 @@ variable (G)
 lemma structure_groupoid.id_mem_maximal_atlas : local_homeomorph.refl H ∈ G.maximal_atlas H :=
 G.subset_maximal_atlas $ by simp
 
+/-- In the model space, any element of the groupoid is in the maximal atlas. -/
+lemma structure_groupoid.mem_maximal_atlas_of_mem_groupoid {f : local_homeomorph H H} (hf : f ∈ G) :
+  f ∈ G.maximal_atlas H :=
+begin
+  rintros e (rfl : e = local_homeomorph.refl H),
+  exact ⟨G.trans (G.symm hf) G.id_mem, G.trans (G.symm G.id_mem) hf⟩,
+end
+
 end maximal_atlas
 
 section singleton

src/geometry/manifold/local_invariant_properties.lean

@@ -605,6 +605,38 @@ lemma is_local_structomorph_within_at_local_invariant_prop [closed_under_restric
     { simpa only [hex, hef ⟨hx, hex⟩] with mfld_simps using hfx }
   end }
 
+variables {H₁ : Type*} [topological_space H₁] {H₂ : Type*} [topological_space H₂]
+   {H₃ : Type*} [topological_space H₃] [charted_space H₁ H₂] [charted_space H₂ H₃]
+   {G₁ : structure_groupoid H₁} [has_groupoid H₂ G₁] [closed_under_restriction G₁]
+   (G₂ : structure_groupoid H₂) [has_groupoid H₃ G₂]
+
+lemma has_groupoid.comp
+  (H : ∀ e ∈ G₂, lift_prop_on (is_local_structomorph_within_at G₁) (e : H₂ → H₂) e.source) :
+  @has_groupoid H₁ _ H₃ _ (charted_space.comp H₁ H₂ H₃) G₁ :=
+{ compatible := begin
+    rintros _ _ ⟨e, f, he, hf, rfl⟩ ⟨e', f', he', hf', rfl⟩,
+    apply G₁.locality,
+    intros x hx,
+    simp only with mfld_simps at hx,
+    have hxs : x ∈ f.symm ⁻¹' (e.symm ≫ₕ e').source,
+    { simp only [hx] with mfld_simps },
+    have hxs' : x ∈ f.target ∩ (f.symm) ⁻¹' ((e.symm ≫ₕ e').source ∩ (e.symm ≫ₕ e') ⁻¹' f'.source),
+    { simp only [hx] with mfld_simps },
+    obtain ⟨φ, hφG₁, hφ, hφ_dom⟩ := local_invariant_prop.lift_prop_on_indep_chart
+      (is_local_structomorph_within_at_local_invariant_prop G₁) (G₁.subset_maximal_atlas hf)
+      (G₁.subset_maximal_atlas hf') (H _ (G₂.compatible he he')) hxs' hxs,
+    simp_rw [← local_homeomorph.coe_trans, local_homeomorph.trans_assoc] at hφ,
+    simp_rw [local_homeomorph.trans_symm_eq_symm_trans_symm, local_homeomorph.trans_assoc],
+    have hs : is_open (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source :=
+      (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').open_source,
+    refine ⟨_, hs.inter φ.open_source, _, _⟩,
+    { simp only [hx, hφ_dom] with mfld_simps, },
+    { refine G₁.eq_on_source (closed_under_restriction' hφG₁ hs) _,
+      rw local_homeomorph.restr_source_inter,
+      refine (hφ.mono _).restr_eq_on_source,
+      mfld_set_tac },
+  end }
+
 end local_structomorph
 
 end structure_groupoid

src/topology/local_homeomorph.lean

@@ -783,6 +783,19 @@ lemma eq_on_source.restr {e e' : local_homeomorph α β} (he : e ≈ e') (s : se
   e.restr s ≈ e'.restr s :=
 local_equiv.eq_on_source.restr he _
 
+lemma set.eq_on.restr_eq_on_source {e e' : local_homeomorph α β}
+  (h : eq_on e e' (e.source ∩ e'.source)) :
+  e.restr e'.source ≈ e'.restr e.source :=
+begin
+  split,
+  { rw e'.restr_source' _ e.open_source,
+    rw e.restr_source' _ e'.open_source,
+    exact set.inter_comm _ _ },
+  { rw e.restr_source' _ e'.open_source,
+    refine (eq_on.trans _ h).trans _;
+    simp only with mfld_simps },
+end
+
 /-- Composition of a local homeomorphism and its inverse is equivalent to the restriction of the
 identity to the source -/
 lemma trans_self_symm :