refactor(analysis/topology): move is_open_map to continuity

Author: johoelzl

analysis/topology/continuity.lean

@@ -365,23 +365,22 @@ by ext x; rw [set.mem_preimage_eq, ← closure_induced he.1, he.2]
 
 end embedding
 
-section quotient_map
-
 /-- A function between topological spaces is a quotient map if it is surjective,
   and for all `s : set β`, `s` is open iff its preimage is an open set. -/
 def quotient_map [tα : topological_space α] [tβ : topological_space β] (f : α → β) : Prop :=
 function.surjective f ∧ tβ = tα.coinduced f
 
+namespace quotient_map
 variables [topological_space α] [topological_space β] [topological_space γ] [topological_space δ]
 
-lemma quotient_map_id : quotient_map (@id α) :=
+protected lemma id : quotient_map (@id α) :=
 ⟨assume a, ⟨a, rfl⟩, coinduced_id.symm⟩
 
-lemma quotient_map_compose {f : α → β} {g : β → γ} (hf : quotient_map f) (hg : quotient_map g) :
+protected lemma comp {f : α → β} {g : β → γ} (hf : quotient_map f) (hg : quotient_map g) :
   quotient_map (g ∘ f) :=
 ⟨function.surjective_comp hg.left hf.left, by rw [hg.right, hf.right, coinduced_compose]⟩
 
-lemma quotient_map_of_quotient_map_compose {f : α → β} {g : β → γ}
+protected lemma of_quotient_map_compose {f : α → β} {g : β → γ}
   (hf : continuous f) (hg : continuous g)
   (hgf : quotient_map (g ∘ f)) : quotient_map g :=
 ⟨assume b, let ⟨a, h⟩ := hgf.left b in ⟨f a, h⟩,
@@ -390,15 +389,68 @@ lemma quotient_map_of_quotient_map_compose {f : α → β} {g : β → γ}
     (by rw [hgf.right, ← continuous_iff_le_coinduced];
         apply hf.comp continuous_coinduced_rng)⟩
 
-lemma quotient_map.continuous_iff {f : α → β} {g : β → γ} (hf : quotient_map f) :
+protected lemma continuous_iff {f : α → β} {g : β → γ} (hf : quotient_map f) :
   continuous g ↔ continuous (g ∘ f) :=
 by rw [continuous_iff_le_coinduced, continuous_iff_le_coinduced, hf.right, coinduced_compose]
 
-lemma quotient_map.continuous {f : α → β} (hf : quotient_map f) : continuous f :=
+protected lemma continuous {f : α → β} (hf : quotient_map f) : continuous f :=
 hf.continuous_iff.mp continuous_id
 
 end quotient_map
 
+section is_open_map
+variables [topological_space α] [topological_space β]
+
+def is_open_map (f : α → β) := ∀ U : set α, is_open U → is_open (f '' U)
+
+lemma is_open_map_iff_nhds_le (f : α → β) : is_open_map f ↔ ∀(a:α), nhds (f a) ≤ (nhds a).map f :=
+begin
+  split,
+  { assume h a s hs,
+    rcases mem_nhds_sets_iff.1 hs with ⟨t, hts, ht, hat⟩,
+    exact filter.mem_sets_of_superset
+      (mem_nhds_sets (h t ht) (mem_image_of_mem _ hat))
+      (image_subset_iff.2 hts) },
+  { refine assume h s hs, is_open_iff_mem_nhds.2 _,
+    rintros b ⟨a, ha, rfl⟩,
+    exact h _ (filter.image_mem_map $ mem_nhds_sets hs ha) }
+end
+
+end is_open_map
+
+namespace is_open_map
+variables [topological_space α] [topological_space β] [topological_space γ]
+open function
+
+protected lemma id : is_open_map (@id α) := assume s hs, by rwa [image_id]
+
+protected lemma comp
+  {f : α → β} {g : β → γ} (hf : is_open_map f) (hg : is_open_map g) : is_open_map (g ∘ f) :=
+by intros s hs; rw [image_comp]; exact hg _ (hf _ hs)
+
+lemma of_inverse {f : α → β} {f' : β → α}
+  (h : continuous f') (l_inv : left_inverse f f') (r_inv : right_inverse f f') :
+  is_open_map f :=
+assume s hs,
+have f' ⁻¹' s = f '' s, by ext x; simp [mem_image_iff_of_inverse r_inv l_inv],
+this ▸ h s hs
+
+lemma to_quotient_map {f : α → β}
+  (open_map : is_open_map f) (cont : continuous f) (surj : function.surjective f) :
+  quotient_map f :=
+⟨ surj,
+  begin
+    ext s,
+    show is_open s ↔ is_open (f ⁻¹' s),
+    split,
+    { exact cont s },
+    { assume h,
+      rw ← @image_preimage_eq _ _ _ s surj,
+      exact open_map _ h }
+  end⟩
+
+end is_open_map
+
 section sierpinski
 variables [topological_space α]
 
@@ -526,6 +578,17 @@ lemma is_closed_prod [topological_space α] [topological_space β] {s₁ : set 
   (h₁ : is_closed s₁) (h₂ : is_closed s₂) : is_closed (set.prod s₁ s₂) :=
 closure_eq_iff_is_closed.mp $ by simp [h₁, h₂, closure_prod_eq, closure_eq_of_is_closed]
 
+protected lemma is_open_map.prod
+  [topological_space α] [topological_space β] [topological_space γ] [topological_space δ]
+  {f : α → β} {g : γ → δ}
+  (hf : is_open_map f) (hg : is_open_map g) : is_open_map (λ p : α × γ, (f p.1, g p.2)) :=
+begin
+  rw [is_open_map_iff_nhds_le],
+  rintros ⟨a, b⟩,
+  rw [nhds_prod_eq, nhds_prod_eq, ← filter.prod_map_map_eq],
+  exact filter.prod_mono ((is_open_map_iff_nhds_le f).1 hf a) ((is_open_map_iff_nhds_le g).1 hg b)
+end
+
 section tube_lemma
 
 def nhds_contain_boxes (s : set α) (t : set β) : Prop :=

analysis/topology/quotient_topological_structures.lean

@@ -6,65 +6,6 @@ open function set
 variables {α : Type*} [topological_space α] {β : Type*} [topological_space β]
 variables {γ : Type*} [topological_space γ] {δ : Type*} [topological_space δ]
 
-def is_open_map (f : α → β) := ∀ U : set α, is_open U → is_open (f '' U)
-
-lemma is_open_map_iff_nhds_le (f : α → β) : is_open_map f ↔ ∀(a:α), nhds (f a) ≤ (nhds a).map f :=
-begin
-  split,
-  { assume h a s hs,
-    rcases mem_nhds_sets_iff.1 hs with ⟨t, hts, ht, hat⟩,
-    exact filter.mem_sets_of_superset
-      (mem_nhds_sets (h t ht) (mem_image_of_mem _ hat))
-      (image_subset_iff.2 hts) },
-  { refine assume h s hs, is_open_iff_mem_nhds.2 _,
-    rintros b ⟨a, ha, rfl⟩,
-    exact h _ (filter.image_mem_map $ mem_nhds_sets hs ha) }
-end
-
-namespace is_open_map
-
-protected lemma id : is_open_map (@id α) := assume s hs, by rwa [image_id]
-
-protected lemma comp
-  {f : α → β} {g : β → γ} (hf : is_open_map f) (hg : is_open_map g) : is_open_map (g ∘ f) :=
-by intros s hs; rw [image_comp]; exact hg _ (hf _ hs)
-
-protected lemma prod {f : α → β} {g : γ → δ}
-  (hf : is_open_map f) (hg : is_open_map g) : is_open_map (λ p : α × γ, (f p.1, g p.2)) :=
-begin
-  rw [is_open_map_iff_nhds_le],
-  rintros ⟨a, b⟩,
-  rw [nhds_prod_eq, nhds_prod_eq, ← filter.prod_map_map_eq],
-  exact filter.prod_mono ((is_open_map_iff_nhds_le f).1 hf a) ((is_open_map_iff_nhds_le g).1 hg b)
-end
-
-lemma of_inverse {f : α → β} {f' : β → α}
-  (h : continuous f') (l_inv : left_inverse f f') (r_inv : right_inverse f f') :
-  is_open_map f :=
-assume s hs,
-have f' ⁻¹' s = f '' s, by ext x; simp [mem_image_iff_of_inverse r_inv l_inv],
-this ▸ h s hs
-
-lemma to_quotient_map {f : α → β}
-  (open_map : is_open_map f) (cont : continuous f) (surj : surjective f) :
-  quotient_map f :=
-⟨ surj,
-  begin
-    ext s,
-    show is_open s ↔ is_open (f ⁻¹' s),
-    split,
-    { exact cont s },
-    { assume h,
-      rw ← @image_preimage_eq _ _ _ s surj,
-      exact open_map _ h }
-  end⟩
-
-end is_open_map
-
-lemma is_open_coinduced {β} {s : set β} {f : α → β} :
-  @is_open β (topological_space.coinduced f _inst_1) s ↔ is_open (f ⁻¹' s) :=
-iff.refl _
-
 section topological_group
 variables [group α] [topological_group α]
 

analysis/topology/topological_space.lean

@@ -868,6 +868,10 @@ def topological_space.induced {α : Type u} {β : Type v} (f : α → β) (t : t
       show is_open (⋃h, f i h), from @is_open_Union β _ t _ $ assume h, (hf i h).left)
   end }
 
+lemma is_open_induced_iff [t : topological_space β] {s : set α} {f : α → β} :
+  @is_open α (t.induced f) s ↔ (∃t, is_open t ∧ s = f ⁻¹' t) :=
+iff.refl _
+
 lemma is_closed_induced_iff [t : topological_space β] {s : set α} {f : α → β} :
   @is_closed α (t.induced f) s ↔ (∃t, is_closed t ∧ s = f ⁻¹' t) :=
 ⟨assume ⟨t, ht, heq⟩, ⟨-t, is_closed_compl_iff.2 ht, by simp only [preimage_compl, heq.symm, lattice.neg_neg]⟩,
@@ -885,6 +889,10 @@ def topological_space.coinduced {α : Type u} {β : Type v} (f : α → β) (t :
     show is_open (⋃ (H : i ∈ s), f ⁻¹' i), from
       @is_open_Union _ _ t _ $ assume hi, h i hi) }
 
+lemma is_open_coinduced {t : topological_space α} {s : set β} {f : α → β} :
+  @is_open β (topological_space.coinduced f t) s ↔ is_open (f ⁻¹' s) :=
+iff.refl _
+
 variables {t t₁ t₂ : topological_space α} {t' : topological_space β} {f : α → β} {g : β → α}
 
 lemma induced_le_iff_le_coinduced {f : α → β } {tα : topological_space α} {tβ : topological_space β} :