feat(analysis/topology/completion): comm_ring on separation quotient, completion (separation_quotient A) is equivalent to completion A

Author: PatrickMassot

analysis/topology/completion.lean

@@ -44,39 +44,18 @@ From a slightly different perspective in order to reuse material in analysis.top
 import data.set.basic data.set.function
 import algebra.pi_instances
 import analysis.topology.uniform_space analysis.topology.topological_structures
+import ring_theory.ideals
 
 noncomputable theory
 local attribute [instance] classical.prop_decidable
 open filter set
 universes u v w x
 
-namespace filter
-variables {α : Type u} {β : Type v} {γ : Type w}
-
-@[simp] lemma prod_pure_pure {a : α} {b : β} :
-  filter.prod (pure a) (pure b) = pure (a, b) :=
-by simp
-
-end filter
-
 /- separation space -/
 namespace uniform_space
 variables {α : Type u} {β : Type v} {γ : Type w}
 variables [uniform_space α] [uniform_space β] [uniform_space γ]
 
-lemma uniform_continuous_of_const {c : α → β} (h : ∀a b, c a = c b) : uniform_continuous c :=
-have (λ (x : α × α), (c (x.fst), c (x.snd))) ⁻¹' id_rel = univ, from
-  eq_univ_iff_forall.2 $ assume ⟨a, b⟩, h a b,
-le_trans (map_le_iff_le_comap.2 $ by simp [comap_principal, this, univ_mem_sets]) refl_le_uniformity
-
-lemma cauchy_prod {f : filter α} {g : filter β} : cauchy f → cauchy g → cauchy (filter.prod f g)
-| ⟨f_proper, hf⟩ ⟨g_proper, hg⟩ := ⟨filter.prod_neq_bot.2 ⟨f_proper, g_proper⟩,
-  let p_α := λp:(α×β)×(α×β), (p.1.1, p.2.1), p_β := λp:(α×β)×(α×β), (p.1.2, p.2.2) in
-  suffices (f.prod f).comap p_α ⊓ (g.prod g).comap p_β ≤ uniformity.comap p_α ⊓ uniformity.comap p_β,
-    by simpa [uniformity_prod, filter.prod, filter.comap_inf, filter.comap_comap_comp, (∘),
-        lattice.inf_assoc, lattice.inf_comm, lattice.inf_left_comm],
-  lattice.inf_le_inf (filter.comap_mono hf) (filter.comap_mono hg)⟩
-
 def separation_setoid (α : Type u) [uniform_space α] : setoid α :=
 ⟨λx y, (x, y) ∈ separation_rel α, separated_equiv⟩
 
@@ -170,7 +149,7 @@ lemma comap_quotient_eq_uniformity :
   uniformity.comap (λ (p : α × α), (⟦p.fst⟧, ⟦p.snd⟧)) = uniformity :=
 le_antisymm comap_quotient_le_uniformity le_comap_map
 
-lemma complete_space_separation [h : complete_space α] :
+instance complete_space_separation [h : complete_space α] :
   complete_space (quotient (separation_setoid α)) :=
 ⟨assume f, assume hf : cauchy f,
   have cauchy (f.comap (λx, ⟦x⟧)), from
@@ -181,7 +160,7 @@ lemma complete_space_separation [h : complete_space α] :
     ... ≤ map (λx, ⟦x⟧) (nhds x) : map_mono hx
     ... ≤ _ : continuous_iff_tendsto.mp uniform_continuous_quotient_mk.continuous _⟩⟩
 
-lemma separated_separation [h : complete_space α] : separated (quotient (separation_setoid α)) :=
+instance separated_separation : separated (quotient (separation_setoid α)) :=
 set.ext $ assume ⟨a, b⟩, quotient.induction_on₂ a b $ assume a b,
   ⟨assume h,
     have a ≈ b, from assume s hs,
@@ -202,6 +181,53 @@ lemma eq_of_separated_of_uniform_continuous [separated β] {f : α → β} {x y
   (H : uniform_continuous f) (h : x ≈ y) : f x = f y :=
 separated_def.1 (by apply_instance) _ _ $ separated_of_uniform_continuous H h
 
+def separation_quotient (α : Type*) [uniform_space α] := quotient (separation_setoid α)
+
+namespace separation_quotient
+instance : uniform_space (separation_quotient α) := by dunfold separation_quotient ; apply_instance
+instance : separated (separation_quotient α) := by dunfold separation_quotient ; apply_instance
+
+def lift [separated β] (f : α → β) : (separation_quotient α → β) :=
+if h : uniform_continuous f then
+  quotient.lift f (λ x y, eq_of_separated_of_uniform_continuous h)
+else
+  λ x, f (classical.inhabited_of_nonempty $ (nonempty_quotient_iff $ separation_setoid α).1 ⟨x⟩).default
+
+lemma lift_mk [separated β] {f : α → β} (h : uniform_continuous f) (a : α) : lift f ⟦a⟧ = f a :=
+by rw [lift, dif_pos h]; refl
+
+lemma uniform_continuous_lift [separated β] (f : α → β) : uniform_continuous (lift f) :=
+begin
+  by_cases hf : uniform_continuous f,
+  { rw [lift, dif_pos hf], exact uniform_continuous_quotient_lift hf },
+  { rw [lift, dif_neg hf], exact uniform_continuous_of_const (assume a b, rfl) }
+end
+
+def map (f : α → β) : separation_quotient α → separation_quotient β :=
+lift (quotient.mk ∘ f)
+
+lemma map_mk {f : α → β} (h : uniform_continuous f) (a : α) : map f ⟦a⟧ = ⟦f a⟧ :=
+by rw [map, lift_mk (h.comp uniform_continuous_quotient_mk)]
+
+lemma uniform_continuous_map (f : α → β): uniform_continuous (map f) :=
+uniform_continuous_lift (quotient.mk ∘ f)
+
+lemma map_unique {f : α → β} (hf : uniform_continuous f)
+  {g : separation_quotient α → separation_quotient β}
+  (comm : quotient.mk ∘ f = g ∘ quotient.mk) : map f = g :=
+by ext ⟨a⟩;
+calc map f ⟦a⟧ = ⟦f a⟧ : map_mk hf a
+  ... = g ⟦a⟧ : congr_fun comm a
+
+lemma map_id : map (@id α) = id :=
+map_unique uniform_continuous_id rfl
+
+lemma map_comp {f : α → β} {g : β → γ} (hf : uniform_continuous f) (hg : uniform_continuous g) :
+  map g ∘ map f = map (g ∘ f) :=
+(map_unique (hf.comp hg) $ by simp only [(∘), map_mk, hf, hg]).symm
+
+end separation_quotient
+
 lemma separation_prod {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) ≈ (a₂, b₂) ↔ a₁ ≈ a₂ ∧ b₁ ≈ b₂ :=
 begin
   split,
@@ -224,6 +250,15 @@ separated_def.2 $ assume x y H, prod.ext
   (eq_of_separated_of_uniform_continuous uniform_continuous_fst H)
   (eq_of_separated_of_uniform_continuous uniform_continuous_snd H)
 
+instance [comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :
+  comm_ring (quotient (separation_setoid α)) :=
+begin
+  dsimp [separation_setoid],
+  conv in (quotient _) {congr, congr, funext, rw group_separation_rel x y },
+  change comm_ring (quotient_ring.quotient $ closure (is_ideal.trivial α)),
+  apply_instance
+end
+
 end uniform_space
 
 /-- Space of Cauchy filters
@@ -423,7 +458,7 @@ begin
   { rw [extend, if_pos hf],
     exact uniform_continuous_uniformly_extend uniform_embedding_pure_cauchy pure_cauchy_dense hf },
   { rw [extend, if_neg hf],
-    exact uniform_space.uniform_continuous_of_const (assume a b, by congr) }
+    exact uniform_continuous_of_const (assume a b, by congr) }
 end
 
 end extend
@@ -514,9 +549,9 @@ namespace completion
 @[priority 50]
 instance : uniform_space (completion α) := by dunfold completion ; apply_instance
 
-instance : complete_space (completion α) := complete_space_separation
+instance : complete_space (completion α) := by dunfold completion ; apply_instance
 
-instance : separated (completion α) := separated_separation
+instance : separated (completion α) := by dunfold completion ; apply_instance
 
 instance : t2_space (completion α) := separated_t2
 
@@ -612,6 +647,10 @@ have ∀x:(completion α × completion β) × (completion γ × completion δ),
   is_closed_property dense₄ hp (assume p:(α×β)×(γ×δ), ih p.1.1 p.1.2 p.2.1 p.2.2),
 this ((a, b), (c, d))
 
+lemma ext [t2_space β] {f g : completion α → β} (hf : continuous f) (hg : continuous g)
+  (h : ∀a:α, f a = g a) : f = g :=
+funext $ assume a, completion.induction_on a (is_closed_eq hf hg) h
+
 section extension
 variables {f : α → β}
 variables [complete_space β] [separated β]
@@ -637,7 +676,7 @@ section map
 variables {f : α → β}
 
 /-- Completion functor acting on morphisms -/
-protected def map (f : α → γ) : completion α → completion γ :=
+protected def map (f : α → β) : completion α → completion β :=
 completion.extension (coe ∘ f)
 
 lemma uniform_continuous_map : uniform_continuous (completion.map f) :=
@@ -647,13 +686,66 @@ lemma continuous_map : continuous (completion.map f) :=
 uniform_continuous_extension.continuous
 
 @[simp] lemma map_coe (hf : uniform_continuous f) (a : α) : (completion.map f) a = f a :=
+by rw [completion.map, extension_coe]; from hf.comp (uniform_continuous_coe β)
+
+lemma map_unique {f : α → β} {g : completion α → completion β}
+  (hg : uniform_continuous g) (h : ∀a:α, ↑(f a) = g a) : completion.map f = g :=
+completion.ext continuous_map hg.continuous $
 begin
-  rw [completion.map, extension_coe],
-  exact hf.comp (uniform_continuous_coe β)
+  intro a,
+  simp only [completion.map, (∘), h],
+  rw [extension_coe ((uniform_continuous_coe α).comp hg)]
 end
 
+lemma map_id : completion.map (@id α) = id :=
+map_unique uniform_continuous_id (assume a, rfl)
+
+lemma extension_map [complete_space γ] [separated γ] {f : β → γ} {g : α → β}
+  (hf : uniform_continuous f) (hg : uniform_continuous g) :
+  completion.extension f ∘ completion.map g = completion.extension (f ∘ g) :=
+completion.ext (continuous_map.comp continuous_extension) continuous_extension $
+  by intro a; simp only [hg, hf, hg.comp hf, (∘), map_coe, extension_coe]
+
+lemma map_comp {f : α → β} {g : β → γ} (hf : uniform_continuous f) (hg : uniform_continuous g) :
+  completion.map g ∘ completion.map f = completion.map (g ∘ f) :=
+extension_map (hg.comp (uniform_continuous_coe _)) hf
+
 end map
 
+/- In this section we construct isomorphisms between the completion of a uniform space and the
+completion of its separation quotient -/
+section separation_quotient_completion
+
+def completion_separation_quotient_equiv (α : Type u) [uniform_space α] :
+  completion (separation_quotient α) ≃ completion α :=
+begin
+  refine ⟨completion.extension (separation_quotient.lift (coe : α → completion α)),
+    completion.map quotient.mk, _, _⟩,
+  { assume a,
+    refine completion.induction_on a (is_closed_eq (continuous_extension.comp continuous_map) continuous_id) _,
+    rintros ⟨a⟩,
+    show completion.map quotient.mk (completion.extension (separation_quotient.lift coe) ↑⟦a⟧) = ↑⟦a⟧,
+    rw [extension_coe (separation_quotient.uniform_continuous_lift _),
+      separation_quotient.lift_mk (uniform_continuous_coe α),
+      completion.map_coe uniform_continuous_quotient_mk] },
+  { assume a,
+    refine completion.induction_on a (is_closed_eq (continuous_map.comp continuous_extension) continuous_id) _,
+    assume a,
+    rw [map_coe uniform_continuous_quotient_mk,
+      extension_coe (separation_quotient.uniform_continuous_lift _),
+      separation_quotient.lift_mk (uniform_continuous_coe α) _] }
+end
+
+lemma uniform_continuous_completion_separation_quotient_equiv :
+  uniform_continuous ⇑(completion_separation_quotient_equiv α) :=
+uniform_continuous_extension
+
+lemma uniform_continuous_completion_separation_quotient_equiv_symm :
+  uniform_continuous ⇑(completion_separation_quotient_equiv α).symm :=
+uniform_continuous_map
+
+end separation_quotient_completion
+
 section prod
 variables [uniform_space β]
 protected def prod {α β} [uniform_space α] [uniform_space β] (p : completion α × completion β) : completion (α × β) :=

analysis/topology/continuity.lean

@@ -104,6 +104,12 @@ have ∀ (a : α), nhds a ⊓ principal s ≠ ⊥ → nhds (f a) ⊓ principal (
   neq_bot_of_le_neq_bot h₁ h₂,
 by simp [image_subset_iff, closure_eq_nhds]; assumption
 
+lemma mem_closure [topological_space α] [topological_space β]
+  {s : set α} {t : set β} {f : α → β} {a : α}
+  (hf : continuous f) (ha : a ∈ closure s) (ht : ∀a∈s, f a ∈ t) : f a ∈ closure t :=
+subset.trans (image_closure_subset_closure_image hf) (closure_mono $ image_subset_iff.2 ht) $
+  (mem_image_of_mem f ha)
+
 lemma compact_image {s : set α} {f : α → β} (hs : compact s) (hf : continuous f) : compact (f '' s) :=
 compact_of_finite_subcover $ assume c hco hcs,
   have hdo : ∀t∈c, is_open (f ⁻¹' t), from assume t' ht, hf _ $ hco _ ht,
@@ -507,6 +513,15 @@ have filter.prod (nhds a) (nhds b) ⊓ principal (set.prod s t) =
   by rw [←prod_inf_prod, prod_principal_principal],
 by simp [closure_eq_nhds, nhds_prod_eq, this]; exact prod_neq_bot
 
+lemma mem_closure2 [topological_space α] [topological_space β] [topological_space γ]
+  {s : set α} {t : set β} {u : set γ} {f : α → β → γ} {a : α} {b : β}
+  (hf : continuous (λp:α×β, f p.1 p.2)) (ha : a ∈ closure s) (hb : b ∈ closure t)
+  (hu : ∀a b, a ∈ s → b ∈ t → f a b ∈ u) :
+  f a b ∈ closure u :=
+have (a, b) ∈ closure (set.prod s t), by rw [closure_prod_eq]; from ⟨ha, hb⟩,
+show (λp:α×β, f p.1 p.2) (a, b) ∈ closure u, from
+  mem_closure hf this $ assume ⟨a, b⟩ ⟨ha, hb⟩, hu a b ha hb
+
 lemma is_closed_prod [topological_space α] [topological_space β] {s₁ : set α} {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]

analysis/topology/topological_structures.lean

@@ -385,45 +385,16 @@ end topological_ring
 
 section topological_comm_ring
 universe u'
-variables (α) [topological_space α] [comm_ring α] [t : topological_ring α]
+variables (α) [topological_space α] [comm_ring α] [topological_ring α]
 
+instance ideal_closure (S : set α) [is_ideal S] : is_ideal (closure S) :=
+{ zero_ := subset_closure (is_ideal.zero S),
+  add_  := assume x y hx hy,
+    mem_closure2 continuous_add' hx hy $ assume a b, is_ideal.add,
+  smul  := assume c x hx,
+    have continuous (λx:α, c * x) := continuous_mul continuous_const continuous_id,
+    mem_closure this hx $ assume a, is_ideal.mul_left }
 
-class is_ideal' {α : Type u} [comm_ring α] (s : set α) : Prop :=
-(zero : (0:α) ∈ s)
-(add  : (λ p : α × α, p.1 + p.2) ''  set.prod s s ⊆ s)
-(mul : ∀ b, (λ s, b*s) '' s ⊆ s)
-
-lemma is_ideal_iff {β : Type*} [comm_ring β] (S : set β) :
- is_ideal S ↔ is_ideal' S :=
-begin
-  split ; intro h ; haveI := h,
-  { split,
-    { exact is_ideal.zero S },
-    { rintros a ⟨⟨x, y⟩, ⟨x_in, y_in⟩, sum⟩,
-      rw ←sum,
-      exact is_ideal.add x_in y_in },
-    { rintros b s ⟨a, ⟨a_in, prod⟩⟩,
-      rw ←prod,
-      exact is_ideal.mul_left a_in } },
-  { exact { zero_ := h.zero,
-      add_ := λ x y x_in y_in, have xy : x + y ∈ (λ (p : β × β), p.fst + p.snd) '' set.prod S S :=
-          mem_image_of_mem (λ p : β × β, p.1 + p.2) (mk_mem_prod x_in y_in),
-        is_ideal'.add S xy,
-      smul := λ b, by rw ←image_subset_iff' ; exact is_ideal'.mul S b }}
-end
-
-instance ideal_closure [topological_ring α] (S : set α) [is_ideal S] : is_ideal (closure S) :=
-begin
-  rcases (is_ideal_iff S).1 (by apply_instance) with ⟨zero, add, mul⟩,
-  rw is_ideal_iff,
-  split,
-  { exact subset_closure zero },
-  { rw ←closure_prod_eq,
-    exact subset.trans (image_closure_subset_closure_image continuous_add') (closure_mono add) },
-  { intro b,
-    have : continuous (λ s, b*s) := continuous_mul continuous_const continuous_id,
-    exact subset.trans (image_closure_subset_closure_image this) (closure_mono (mul b)) },
-end
 end topological_comm_ring
 
 /-- (Partially) ordered topology

data/quot.lean

@@ -83,6 +83,9 @@ theorem quotient.choice_eq {ι : Type*} {α : ι → Type*} [∀ i, setoid (α i
   (f : ∀ i, α i) : quotient.choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
 quotient.sound $ λ i, quotient.mk_out _
 
+lemma nonempty_quotient_iff (s : setoid α): nonempty (quotient s) ↔ nonempty α :=
+⟨assume ⟨a⟩, quotient.induction_on a nonempty.intro, assume ⟨a⟩, ⟨⟦a⟧⟩⟩
+
 /-- `trunc α` is the quotient of `α` by the always-true relation. This
   is related to the propositional truncation in HoTT, and is similar
   in effect to `nonempty α`, but unlike `nonempty α`, `trunc α` is data,

data/set/basic.lean

@@ -882,9 +882,6 @@ theorem image_subset_iff {s : set α} {t : set β} {f : α → β} :
   f '' s ⊆ t ↔ s ⊆ f ⁻¹' t :=
 ball_image_iff
 
-lemma image_subset_iff' {α : Type*} {β : Type*} (f : α → β) (s : set α) (t : set β) :
-  f '' s ⊆ t ↔ ∀ a, a ∈ s → f a ∈ t := image_subset_iff
-
 theorem image_preimage_subset (f : α → β) (s : set β) :
   f '' (f ⁻¹' s) ⊆ s :=
 image_subset_iff.2 (subset.refl _)

order/filter.lean

@@ -1596,6 +1596,9 @@ by simp only [filter.prod, comap_inf, inf_comm, inf_assoc, lattice.inf_left_comm
   filter.prod (principal s) (principal t) = principal (set.prod s t) :=
 by simp only [filter.prod, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]; refl
 
+@[simp] lemma prod_pure_pure {a : α} {b : β} : filter.prod (pure a) (pure b) = pure (a, b) :=
+by simp
+
 lemma prod_def {f : filter α} {g : filter β} : f.prod g = (f.lift $ λs, g.lift' $ set.prod s) :=
 have ∀(s:set α) (t : set β),
     principal (set.prod s t) = (principal s).comap prod.fst ⊓ (principal t).comap prod.snd,