feat(analysis/topology): quotient spaces and quotient maps (#155)

* style(analysis/topology): simplify induced_mono and induced_sup

* style(analysis/topology/topological_space): reorganize section constructions

* feat(analysis/topology/topological_space): add more galois connection lemmas

* feat(analysis/topology): quotient spaces and quotient maps

analysis/topology/continuity.lean

@@ -226,16 +226,6 @@ end constructions
 
 section embedding
 
-lemma induced_mono {t₁ t₂ : topological_space α} {f : β → α} (h : t₁ ≤ t₂) :
-  t₁.induced f ≤ t₂.induced f :=
-continuous_iff_induced_le.mp $
-  show @continuous β α (@topological_space.induced β α f t₂) t₁ (id ∘ f),
-  begin
-    apply continuous.comp,
-    exact continuous_induced_dom,
-    exact assume s hs, h _ hs
-  end
-
 lemma induced_id [t : topological_space α] : t.induced id = t :=
 topological_space_eq $ funext $ assume s, propext $
   ⟨assume ⟨s', hs, h⟩, h.symm ▸ hs, assume hs, ⟨s, hs, rfl⟩⟩
@@ -246,14 +236,6 @@ topological_space_eq $ funext $ assume s, propext $
   ⟨assume ⟨s', ⟨s, hs, h₂⟩, h₁⟩, h₁.symm ▸ h₂.symm ▸ ⟨s, hs, rfl⟩,
     assume ⟨s, hs, h⟩, ⟨preimage g s, ⟨s, hs, rfl⟩, h ▸ rfl⟩⟩
 
-lemma induced_sup (t₁ : topological_space β) (t₂ : topological_space β) {f : α → β} :
-  (t₁ ⊔ t₂).induced f = t₁.induced f ⊔ t₂.induced f :=
-le_antisymm
-  (continuous_iff_induced_le.mp $ continuous_sup_rng
-    (continuous_sup_dom_left continuous_induced_dom)
-    (continuous_sup_dom_right continuous_induced_dom))
-  (sup_le (induced_mono le_sup_left) (induced_mono le_sup_right))
-
 /-- A function between topological spaces is an embedding if it is injective,
   and for all `s : set α`, `s` is open iff it is the preimage of an open set. -/
 def embedding [tα : topological_space α] [tβ : topological_space β] (f : α → β) : Prop :=
@@ -296,6 +278,40 @@ h_eq.symm ▸ by rwa [image_preimage_eq_inter_range]
 
 end embedding
 
+section quotient_map
+
+lemma coinduced_id [t : topological_space α] : t.coinduced id = t :=
+topological_space_eq rfl
+
+lemma coinduced_compose [tα : topological_space α]
+  {f : α → β} {g : β → γ} : (tα.coinduced f).coinduced g = tα.coinduced (g ∘ f) :=
+topological_space_eq rfl
+
+/-- 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
+
+variables [topological_space α] [topological_space β] [topological_space γ] [topological_space δ]
+
+lemma quotient_map_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) :
+  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 : β → γ}
+  (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⟩,
+  le_antisymm
+    (by rwa ← continuous_iff_le_coinduced)
+    (by rw [hgf.right, ← continuous_iff_le_coinduced];
+        apply hf.comp continuous_coinduced_rng)⟩
+
+end quotient_map
+
 section sierpinski
 variables [topological_space α]
 
@@ -580,6 +596,36 @@ closure_induced $ assume x y, subtype.eq
 
 end subtype
 
+section quotient
+variables [topological_space α] [topological_space β] [topological_space γ]
+variables {r : α → α → Prop} {s : setoid α}
+
+lemma quotient_map.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_quot_mk : quotient_map (@quot.mk α r) :=
+⟨quot.exists_rep, rfl⟩
+
+lemma continuous_quot_mk : continuous (@quot.mk α r) :=
+continuous_coinduced_rng
+
+lemma continuous_quot_lift {f : α → β} (hr : ∀ a b, r a b → f a = f b)
+  (h : continuous f) : continuous (quot.lift f hr : quot r → β) :=
+continuous_coinduced_dom h
+
+lemma quotient_map_quotient_mk : quotient_map (@quotient.mk α s) :=
+quotient_map_quot_mk
+
+lemma continuous_quotient_mk : continuous (@quotient.mk α s) :=
+continuous_coinduced_rng
+
+lemma continuous_quotient_lift {f : α → β} (hs : ∀ a b, a ≈ b → f a = f b)
+  (h : continuous f) : continuous (quotient.lift f hs : quotient s → β) :=
+continuous_coinduced_dom h
+
+end quotient
+
 section pi
 variables {ι : Type*} {π : ι → Type*}
 

analysis/topology/topological_space.lean

@@ -726,8 +726,7 @@ le_antisymm
 
 end topological_space
 
-/- constructions using the complete lattice structure -/
-section constructions
+section lattice
 
 variables {α : Type u} {β : Type v}
 
@@ -751,42 +750,6 @@ private lemma le_Inf {tt : set (topological_space α)} {t : topological_space α
   t ≤ Inf tt :=
 assume s hs t' ht', h t' ht' s hs
 
-/-- Given `f : α → β` and a topology on `β`, the induced topology on `α` is the collection of
-  sets that are preimages of some open set in `β`. This is the coarsest topology that
-  makes `f` continuous. -/
-def topological_space.induced {α : Type u} {β : Type v} (f : α → β) (t : topological_space β) :
-  topological_space α :=
-{ is_open        := λs, ∃s', t.is_open s' ∧ s = f ⁻¹' s',
-  is_open_univ   := ⟨univ, by simp; exact t.is_open_univ⟩,
-  is_open_inter  := assume s₁ s₂ ⟨s'₁, hs₁, eq₁⟩ ⟨s'₂, hs₂, eq₂⟩,
-    ⟨s'₁ ∩ s'₂, by simp [eq₁, eq₂]; exact t.is_open_inter _ _ hs₁ hs₂⟩,
-  is_open_sUnion := assume s h,
-  begin
-    simp [classical.skolem] at h,
-    cases h with f hf,
-    apply exists.intro (⋃(x : set α) (h : x ∈ s), f x h),
-    simp [sUnion_eq_Union, (λx h, (hf x h).right.symm)],
-    exact (@is_open_Union β _ t _ $ assume i,
-      show is_open (⋃h, f i h), from @is_open_Union β _ t _ $ assume h, (hf i h).left)
-  end }
-
-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, by simp; assumption, by simp [preimage_compl, heq.symm]⟩,
-  assume ⟨t, ht, heq⟩, ⟨-t, ht, by simp [preimage_compl, heq.symm]⟩⟩
-
-/-- Given `f : α → β` and a topology on `α`, the coinduced topology on `β` is defined
-  such that `s:set β` is open if the preimage of `s` is open. This is the finest topology that
-  makes `f` continuous. -/
-def topological_space.coinduced {α : Type u} {β : Type v} (f : α → β) (t : topological_space α) :
-  topological_space β :=
-{ is_open        := λs, t.is_open (f ⁻¹' s),
-  is_open_univ   := by simp; exact t.is_open_univ,
-  is_open_inter  := assume s₁ s₂ h₁ h₂, by simp; exact t.is_open_inter _ _ h₁ h₂,
-  is_open_sUnion := assume s h, by rw [preimage_sUnion]; exact (@is_open_Union _ _ t _ $ assume i,
-    show is_open (⋃ (H : i ∈ s), f ⁻¹' i), from
-      @is_open_Union _ _ t _ $ assume hi, h i hi) }
-
 instance : has_inf (topological_space α) := ⟨λ t₁ t₂,
 { is_open        := λs, t₁.is_open s ∧ t₂.is_open s,
   is_open_univ   := ⟨t₁.is_open_univ, t₂.is_open_univ⟩,
@@ -820,13 +783,6 @@ instance {α : Type u} : complete_lattice (topological_space α) :=
   Inf_le        := assume s a, Inf_le,
   ..topological_space.partial_order }
 
-instance inhabited_topological_space {α : Type u} : inhabited (topological_space α) :=
-⟨⊤⟩
-
-lemma t2_space_top : @t2_space α ⊤ :=
-{ t2 := assume x y hxy, ⟨{x}, {y}, trivial, trivial, mem_insert _ _, mem_insert _ _,
-  eq_empty_iff_forall_not_mem.2 $ by intros z hz; simp at hz; cc⟩ }
-
 lemma le_of_nhds_le_nhds {t₁ t₂ : topological_space α} (h : ∀x, @nhds α t₂ x ≤ @nhds α t₁ x) :
   t₁ ≤ t₂ :=
 assume s, show @is_open α t₁ s → @is_open α t₂ s,
@@ -838,38 +794,129 @@ le_antisymm
   (le_of_nhds_le_nhds $ assume x, le_of_eq $ h x)
   (le_of_nhds_le_nhds $ assume x, le_of_eq $ (h x).symm)
 
+end lattice
+
+section galois_connection
+variables {α : Type u} {β : Type v}
+
+/-- Given `f : α → β` and a topology on `β`, the induced topology on `α` is the collection of
+  sets that are preimages of some open set in `β`. This is the coarsest topology that
+  makes `f` continuous. -/
+def topological_space.induced {α : Type u} {β : Type v} (f : α → β) (t : topological_space β) :
+  topological_space α :=
+{ is_open        := λs, ∃s', t.is_open s' ∧ s = f ⁻¹' s',
+  is_open_univ   := ⟨univ, by simp; exact t.is_open_univ⟩,
+  is_open_inter  := assume s₁ s₂ ⟨s'₁, hs₁, eq₁⟩ ⟨s'₂, hs₂, eq₂⟩,
+    ⟨s'₁ ∩ s'₂, by simp [eq₁, eq₂]; exact t.is_open_inter _ _ hs₁ hs₂⟩,
+  is_open_sUnion := assume s h,
+  begin
+    simp [classical.skolem] at h,
+    cases h with f hf,
+    apply exists.intro (⋃(x : set α) (h : x ∈ s), f x h),
+    simp [sUnion_eq_Union, (λx h, (hf x h).right.symm)],
+    exact (@is_open_Union β _ t _ $ assume i,
+      show is_open (⋃h, f i h), from @is_open_Union β _ t _ $ assume h, (hf i h).left)
+  end }
+
+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, by simp; assumption, by simp [preimage_compl, heq.symm]⟩,
+  assume ⟨t, ht, heq⟩, ⟨-t, ht, by simp [preimage_compl, heq.symm]⟩⟩
+
+/-- Given `f : α → β` and a topology on `α`, the coinduced topology on `β` is defined
+  such that `s:set β` is open if the preimage of `s` is open. This is the finest topology that
+  makes `f` continuous. -/
+def topological_space.coinduced {α : Type u} {β : Type v} (f : α → β) (t : topological_space α) :
+  topological_space β :=
+{ is_open        := λs, t.is_open (f ⁻¹' s),
+  is_open_univ   := by simp; exact t.is_open_univ,
+  is_open_inter  := assume s₁ s₂ h₁ h₂, by simp; exact t.is_open_inter _ _ h₁ h₂,
+  is_open_sUnion := assume s h, by rw [preimage_sUnion]; exact (@is_open_Union _ _ t _ $ assume i,
+    show is_open (⋃ (H : i ∈ s), f ⁻¹' i), from
+      @is_open_Union _ _ t _ $ assume hi, h i hi) }
+
+variables {t t₁ t₂ : topological_space α} {t' : topological_space β} {f : α → β} {g : β → α}
+
 lemma induced_le_iff_le_coinduced {f : α → β } {tα : topological_space α} {tβ : topological_space β} :
   tβ.induced f ≤ tα ↔ tβ ≤ tα.coinduced f :=
 iff.intro
   (assume h s hs, show tα.is_open (f ⁻¹' s), from h _ ⟨s, hs, rfl⟩)
   (assume h s ⟨t, ht, hst⟩, hst.symm ▸ h _ ht)
 
+lemma gc_induced_coinduced (f : α → β) :
+  galois_connection (topological_space.induced f) (topological_space.coinduced f) :=
+assume f g, induced_le_iff_le_coinduced
+
+lemma induced_mono (h : t₁ ≤ t₂) : t₁.induced g ≤ t₂.induced g :=
+(gc_induced_coinduced g).monotone_l h
+
+lemma coinduced_mono (h : t₁ ≤ t₂) : t₁.coinduced f ≤ t₂.coinduced f :=
+(gc_induced_coinduced f).monotone_u h
+
+@[simp] lemma induced_bot : (⊥ : topological_space α).induced g = ⊥ :=
+(gc_induced_coinduced g).l_bot
+
+@[simp] lemma induced_sup : (t₁ ⊔ t₂).induced g = t₁.induced g ⊔ t₂.induced g :=
+(gc_induced_coinduced g).l_sup
+
+@[simp] lemma induced_supr {ι : Sort w} {t : ι → topological_space α} :
+  (⨆i, t i).induced g = (⨆i, (t i).induced g) :=
+(gc_induced_coinduced g).l_supr
+
+@[simp] lemma coinduced_top : (⊤ : topological_space α).coinduced f = ⊤ :=
+(gc_induced_coinduced f).u_top
+
+@[simp] lemma coinduced_inf : (t₁ ⊓ t₂).coinduced f = t₁.coinduced f ⊓ t₂.coinduced f :=
+(gc_induced_coinduced f).u_inf
+
+@[simp] lemma coinduced_infi {ι : Sort w} {t : ι → topological_space α} :
+  (⨅i, t i).coinduced f = (⨅i, (t i).coinduced f) :=
+(gc_induced_coinduced f).u_infi
+
+end galois_connection
+
+/- constructions using the complete lattice structure -/
+section constructions
+open topological_space
+
+variables {α : Type u} {β : Type v}
+
+instance inhabited_topological_space {α : Type u} : inhabited (topological_space α) :=
+⟨⊤⟩
+
+lemma t2_space_top : @t2_space α ⊤ :=
+{ t2 := assume x y hxy, ⟨{x}, {y}, trivial, trivial, mem_insert _ _, mem_insert _ _,
+  eq_empty_iff_forall_not_mem.2 $ by intros z hz; simp at hz; cc⟩ }
+
 instance : topological_space empty := ⊤
 instance : topological_space unit := ⊤
 instance : topological_space bool := ⊤
 instance : topological_space ℕ := ⊤
 instance : topological_space ℤ := ⊤
 
 instance sierpinski_space : topological_space Prop :=
-topological_space.generate_from {{true}}
+generate_from {{true}}
 
 instance {p : α → Prop} [t : topological_space α] : topological_space (subtype p) :=
-topological_space.induced subtype.val t
+induced subtype.val t
+
+instance {r : α → α → Prop} [t : topological_space α] : topological_space (quot r) :=
+coinduced (quot.mk r) t
+
+instance {s : setoid α} [t : topological_space α] : topological_space (quotient s) :=
+coinduced quotient.mk t
 
 instance [t₁ : topological_space α] [t₂ : topological_space β] : topological_space (α × β) :=
-topological_space.induced prod.fst t₁ ⊔ topological_space.induced prod.snd t₂
+induced prod.fst t₁ ⊔ induced prod.snd t₂
 
 instance [t₁ : topological_space α] [t₂ : topological_space β] : topological_space (α ⊕ β) :=
-topological_space.coinduced sum.inl t₁ ⊓ topological_space.coinduced sum.inr t₂
+coinduced sum.inl t₁ ⊓ coinduced sum.inr t₂
 
 instance {β : α → Type v} [t₂ : Πa, topological_space (β a)] : topological_space (sigma β) :=
-⨅a, topological_space.coinduced (sigma.mk a) (t₂ a)
+⨅a, coinduced (sigma.mk a) (t₂ a)
 
 instance Pi.topological_space {β : α → Type v} [t₂ : Πa, topological_space (β a)] : topological_space (Πa, β a) :=
-⨆a, topological_space.induced (λf, f a) (t₂ a)
-
-section
-open topological_space
+⨆a, induced (λf, f a) (t₂ a)
 
 lemma generate_from_le {t : topological_space α} { g : set (set α) } (h : ∀s∈g, is_open s) :
   generate_from g ≤ t :=
@@ -947,8 +994,6 @@ instance Pi.t2_space {β : α → Type v} [t₂ : Πa, topological_space (β a)]
   let ⟨i, hi⟩ := not_forall.mp (mt funext h) in
   separated_by_f (λz, z i) (le_supr _ i) hi⟩
 
-end
-
 end constructions
 
 namespace topological_space