feat(analysis/topology/completion) comm_ring on separation quotient

analysis/topology/completion.lean

@@ -44,6 +44,7 @@ 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
@@ -224,6 +225,13 @@ 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

analysis/topology/topological_structures.lean

@@ -381,34 +381,9 @@ end topological_ring
 
 section topological_comm_ring
 universe u'
-variables (α) [topological_space α] [comm_ring α] [t : topological_ring α]
+variables (α) [topological_space α] [comm_ring α] [topological_ring α]
 
-
-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) :=
+instance ideal_closure (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,

ring_theory/ideals.lean

@@ -39,6 +39,30 @@ instance span (S : set α) : is_ideal (span S) := {}
 
 end is_ideal
 
+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
+
 class is_proper_ideal {α : Type u} [comm_ring α] (S : set α) extends is_ideal S : Prop :=
 (ne_univ : S ≠ set.univ)