feat(geometry/manifold/charted_space): typeclass `closed_under_restri…

…ction` for structure groupoids (#3347)

* Define a typeclass `closed_under_restriction` for structure groupoids.
* Prove that it is equivalent to requiring that the structure groupoid contain all local homeomorphisms equivalent to the restriction of the identity to an open subset.
* Verify that `continuous_groupoid` and `times_cont_diff_groupoid` satisfy `closed_under_restriction`.  
* Show that a charted space defined by a single chart is `has_groupoid` for any structure groupoid satisfying `closed_under_restriction`.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Restriction.20in.20structure.20groupoid)

src/geometry/manifold/charted_space.lean

@@ -134,13 +134,14 @@ open set local_homeomorph
 
 section groupoid
 
-/- One could add to the definition of a structure groupoid the fact that the restriction of an
+/-! One could add to the definition of a structure groupoid the fact that the restriction of an
 element of the groupoid to any open set still belongs to the groupoid.
 (This is in Kobayashi-Nomizu.)
 I am not sure I want this, for instance on `H × E` where `E` is a vector space, and the groupoid is
 made of functions respecting the fibers and linear in the fibers (so that a charted space over this
 groupoid is naturally a vector bundle) I prefer that the members of the groupoid are always
-defined on sets of the form `s × E`.
+defined on sets of the form `s × E`.  There is a typeclass `closed_under_restriction` for groupoids
+which have the restriction property.
 
 The only nontrivial requirement is locality: if a local homeomorphism belongs to the groupoid
 around each point in its domain of definition, then it belongs to the groupoid. Without this
@@ -365,6 +366,86 @@ instance : order_top (structure_groupoid H) :=
   le_top := λ u f hf, by { split; exact dec_trivial },
   ..structure_groupoid.partial_order }
 
+/-- A groupoid is closed under restriction if it contains all restrictions of its element local
+homeomorphisms to open subsets of the source. -/
+class closed_under_restriction (G : structure_groupoid H) : Prop :=
+(closed_under_restriction : ∀ {e : local_homeomorph H H}, e ∈ G → ∀ (s : set H), is_open s →
+  (e : local_homeomorph H H).restr s ∈ G)
+
+/-- The trivial restriction-closed groupoid, containing only local homeomorphisms equivalent to the
+restriction of the identity to the various open subsets. -/
+def id_restr_groupoid : structure_groupoid H :=
+{ members := {e | ∃ {s : set H} (h : is_open s), e ≈ local_homeomorph.of_set s h},
+  trans' := begin
+    rintros e e' ⟨s, hs, hse⟩ ⟨s', hs', hse'⟩,
+    refine ⟨s ∩ s', is_open_inter hs hs', _⟩,
+    have := local_homeomorph.eq_on_source.trans' hse hse',
+    rwa local_homeomorph.of_set_trans_of_set at this,
+  end,
+  symm' := begin
+    rintros e ⟨s, hs, hse⟩,
+    refine ⟨s, hs, _⟩,
+    rw [← of_set_symm],
+    exact local_homeomorph.eq_on_source.symm' hse,
+  end,
+  id_mem' := ⟨univ, is_open_univ, by simp only with mfld_simps⟩,
+  locality' := begin
+    intros e h,
+    refine ⟨e.source, e.open_source, by simp only with mfld_simps, _⟩,
+    intros x hx,
+    rcases h x hx with ⟨s, hs, hxs, s', hs', hes'⟩,
+    have hes : x ∈ (e.restr s).source,
+    { rw e.restr_source, refine ⟨hx, _⟩,
+      rw interior_eq_of_open hs, exact hxs },
+    simpa only with mfld_simps using local_homeomorph.eq_on_source.eq_on hes' hes,
+  end,
+  eq_on_source' := begin
+    rintros e e' ⟨s, hs, hse⟩ hee',
+    exact ⟨s, hs, setoid.trans hee' hse⟩,
+  end
+}
+
+lemma id_restr_groupoid_mem {s : set H} (hs : is_open s) :
+  of_set s hs ∈ (@id_restr_groupoid H _).members := ⟨s, hs, by refl⟩
+
+/-- The trivial restriction-closed groupoid is indeed `closed_under_restriction`. -/
+instance closed_under_restriction_id_restr_groupoid :
+  closed_under_restriction (@id_restr_groupoid H _) :=
+⟨ begin
+    rintros e ⟨s', hs', he⟩ s hs,
+    use [s' ∩ s, is_open_inter hs' hs],
+    refine setoid.trans (local_homeomorph.eq_on_source.restr he s) _,
+    exact ⟨by simp only [interior_eq_of_open hs] with mfld_simps, by simp only with mfld_simps⟩,
+  end ⟩
+
+/-- A groupoid is closed under restriction if and only if it contains the trivial restriction-closed
+groupoid. -/
+lemma closed_under_restriction_iff_id_le (G : structure_groupoid H) :
+  closed_under_restriction G ↔ id_restr_groupoid ≤ G :=
+begin
+  split,
+  { intros _i,
+    apply structure_groupoid.le_iff.mpr,
+    rintros e ⟨s, hs, hes⟩,
+    refine G.eq_on_source _ hes,
+    have h := _i.closed_under_restriction,
+    convert h G.id_mem s hs,
+    rw interior_eq_of_open hs,
+    simp only with mfld_simps },
+  { intros h,
+    split,
+    intros e he s hs,
+    rw ← of_set_trans (e : local_homeomorph H H) hs,
+    refine G.trans _ he,
+    apply structure_groupoid.le_iff.mp h,
+    exact id_restr_groupoid_mem hs },
+end
+
+/-- The groupoid of all local homeomorphisms on a topological space `H` is closed under restriction.
+-/
+instance : closed_under_restriction (continuous_groupoid H) :=
+(closed_under_restriction_iff_id_le _).mpr (by convert le_top)
+
 end groupoid
 
 
@@ -666,6 +747,38 @@ end
 
 end maximal_atlas
 
+section singleton
+variables {α : Type*} [topological_space α]
+variables (e : local_homeomorph α H)
+
+/-- If a single local homeomorphism `e` from a space `α` into `H` has source covering the whole
+space `α`, then that local homeomorphism induces an `H`-charted space structure on `α`.
+(This condition is equivalent to `e` being an open embedding of `α` into `H`.) -/
+def singleton_charted_space (h : e.source = set.univ) : charted_space H α :=
+{ atlas := {e},
+  chart_at := λ _, e,
+  mem_chart_source := λ _, by simp only [h] with mfld_simps,
+  chart_mem_atlas := λ _, by tauto }
+
+lemma singleton_charted_space_one_chart (h : e.source = set.univ) (e' : local_homeomorph α H)
+  (h' : e' ∈ (singleton_charted_space e h).atlas) : e' = e := h'
+
+/-- Given a local homeomorphism `e` from a space `α` into `H`, if its source covers the whole
+space `α`, then the induced charted space structure on `α` is `has_groupoid G` for any structure
+groupoid `G` which is closed under restrictions. -/
+lemma singleton_has_groupoid (h : e.source = set.univ) (G : structure_groupoid H)
+  [closed_under_restriction G] : @has_groupoid _ _ _ _ (singleton_charted_space e h) G :=
+{ compatible := begin
+    intros e' e'' he' he'',
+    rw singleton_charted_space_one_chart e h e' he',
+    rw singleton_charted_space_one_chart e h e'' he'',
+    refine G.eq_on_source _ e.trans_symm_self,
+    have hle : id_restr_groupoid ≤ G := (closed_under_restriction_iff_id_le G).mp (by assumption),
+    exact structure_groupoid.le_iff.mp hle _ (id_restr_groupoid_mem _),
+  end }
+
+end singleton
+
 /-! ### Structomorphisms -/
 
 /-- A `G`-diffeomorphism between two charted spaces is a homeomorphism which, when read in the

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -472,6 +472,16 @@ begin
     exact h3, }
 end
 
+/-- The `C^n` groupoid is closed under restriction. -/
+instance : closed_under_restriction (times_cont_diff_groupoid n I) :=
+(closed_under_restriction_iff_id_le _).mpr
+begin
+  apply structure_groupoid.le_iff.mpr,
+  rintros e ⟨s, hs, hes⟩,
+  apply (times_cont_diff_groupoid n I).eq_on_source' _ _ _ hes,
+  exact of_set_mem_times_cont_diff_groupoid n I hs,
+end
+
 end times_cont_diff_groupoid
 
 end model_with_corners

src/topology/local_homeomorph.lean

@@ -318,6 +318,9 @@ lemma of_set_target : (of_set s hs).target = s := rfl
 @[simp, mfld_simps] lemma of_set_coe : (of_set s hs : α → α) = id := rfl
 @[simp, mfld_simps] lemma of_set_symm : (of_set s hs).symm = of_set s hs := rfl
 
+@[simp, mfld_simps] lemma of_set_univ_eq_refl : of_set univ is_open_univ = local_homeomorph.refl α :=
+by ext; simp
+
 end
 
 /-- Composition of two local homeomorphisms when the target of the first and the source of
@@ -404,6 +407,13 @@ lemma of_set_trans' {s : set α} (hs : is_open s) :
   (of_set s hs).trans e = e.restr (e.source ∩ s) :=
 by rw [of_set_trans, restr_source_inter]
 
+@[simp, mfld_simps] lemma of_set_trans_of_set {s : set α} (hs : is_open s) {s' : set α} (hs' : is_open s') :
+  (of_set s hs).trans (of_set s' hs') = of_set (s ∩ s') (is_open_inter hs hs')  :=
+begin
+  rw (of_set s hs).trans_of_set hs',
+  ext; simp [interior_eq_of_open hs']
+end
+
 lemma restr_trans (s : set α) :
   (e.restr s).trans e' = (e.trans e').restr s :=
 eq_of_local_equiv_eq $ local_equiv.restr_trans e.to_local_equiv e'.to_local_equiv (interior s)