doc(topology/algebra/ring): add module docs + tidy (#7893)

Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>

Author: ericrbg

src/ring_theory/ideal/basic.lean

@@ -490,6 +490,18 @@ protected theorem nontrivial {I : ideal α} (hI : I ≠ ⊤) : nontrivial I.quot
 lemma mk_surjective : function.surjective (mk I) :=
 λ y, quotient.induction_on' y (λ x, exists.intro x rfl)
 
+/-- If `I` is an ideal of a commutative ring `R`, if `q : R → R/I` is the quotient map, and if
+`s ⊆ R` is a subset, then `q⁻¹(q(s)) = ⋃ᵢ(i + s)`, the union running over all `i ∈ I`. -/
+lemma quotient_ring_saturate (I : ideal α) (s : set α) :
+  mk I ⁻¹' (mk I '' s) = (⋃ x : I, (λ y, x.1 + y) '' s) :=
+begin
+  ext x,
+  simp only [mem_preimage, mem_image, mem_Union, ideal.quotient.eq],
+  exact ⟨λ ⟨a, a_in, h⟩, ⟨⟨_, I.neg_mem h⟩, a, a_in, by simp⟩,
+         λ ⟨⟨i, hi⟩, a, ha, eq⟩,
+           ⟨a, ha, by rw [← eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi⟩⟩
+end
+
 instance (I : ideal α) [hI : I.is_prime] : integral_domain I.quotient :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ a b,
     quotient.induction_on₂' a b $ λ a b hab,

src/topology/algebra/ring.lean

@@ -10,6 +10,25 @@ import ring_theory.ideal.basic
 import ring_theory.subring
 import algebra.ring.prod
 
+/-!
+
+# Topological (semi)rings
+
+A topological (semi)ring is a (semi)ring equipped with a topology such that all operations are
+continuous. Besides this definition, this file proves that the topological closure of a subring
+(resp. an ideal) is a subring (resp. an ideal) and defines products and quotients
+of topological (semi)rings.
+
+## Main Results
+
+- `subring.topological_closure`/`subsemiring.topological_closure`: the topological closure of a
+  `subring`/`subsemiring` is itself a `sub(semi)ring`.
+- `prod_ring`/`prod_semiring`: The product of two topological (semi)rings.
+- `ideal.closure`: The closure of an ideal is an ideal.
+- `topological_ring_quotient`: The quotient of a topological ring by an ideal is a topological ring.
+
+-/
+
 open classical set filter topological_space
 open_locale classical
 
@@ -52,14 +71,6 @@ lemma subsemiring.topological_closure_minimal
   s.topological_closure ≤ t :=
 closure_minimal h ht
 
-instance (S : submonoid α) : has_continuous_mul (S.topological_closure) :=
-{ continuous_mul :=
-  begin
-    apply continuous_induced_rng,
-    change continuous (λ p : S.topological_closure × S.topological_closure, (p.1 : α) * (p.2 : α)),
-    continuity,
-  end }
-
 /-- The product topology on the cartesian product of two topological semirings
   makes the product into a topological semiring. -/
 instance prod_semiring {β : Type*}
@@ -113,17 +124,14 @@ instance subring.topological_closure_topological_ring (s : subring α) :
   ..s.to_submonoid.topological_closure_has_continuous_mul }
 
 lemma subring.subring_topological_closure (s : subring α) :
-  s ≤ s.topological_closure :=
-subset_closure
+  s ≤ s.topological_closure := subset_closure
 
 lemma subring.is_closed_topological_closure (s : subring α) :
-  is_closed (s.topological_closure : set α) :=
-by convert is_closed_closure
+  is_closed (s.topological_closure : set α) := by convert is_closed_closure
 
 lemma subring.topological_closure_minimal
   (s : subring α) {t : subring α} (h : s ≤ t) (ht : is_closed (t : set α)) :
-  s.topological_closure ≤ t :=
-closure_minimal h ht
+  s.topological_closure ≤ t := closure_minimal h ht
 
 end topological_ring
 
@@ -132,14 +140,11 @@ variables {α : Type*} [topological_space α] [comm_ring α] [topological_ring 
 
 /-- The closure of an ideal in a topological ring as an ideal. -/
 def ideal.closure (S : ideal α) : ideal α :=
-{ carrier := closure S,
-  smul_mem' := assume c x hx,
-    have continuous (λx:α, c * x) := continuous_const.mul continuous_id,
-    map_mem_closure this hx $ assume a, S.mul_mem_left _,
+{ carrier   := closure S,
+  smul_mem' := λ c x hx, map_mem_closure (mul_left_continuous _) hx $ λ a, S.mul_mem_left c,
   ..(add_submonoid.topological_closure S.to_add_submonoid) }
 
-@[simp] lemma ideal.coe_closure (S : ideal α) :
-  (S.closure : set α) = closure S := rfl
+@[simp] lemma ideal.coe_closure (S : ideal α) : (S.closure : set α) = closure S := rfl
 
 end topological_comm_ring
 
@@ -150,51 +155,34 @@ open ideal.quotient
 instance topological_ring_quotient_topology : topological_space N.quotient :=
 by dunfold ideal.quotient submodule.quotient; apply_instance
 
-lemma quotient_ring_saturate {α : Type*} [comm_ring α] (N : ideal α) (s : set α) :
-  mk N ⁻¹' (mk N '' s) = (⋃ x : N, (λ y, x.1 + y) '' s) :=
-begin
-  ext x,
-  simp only [mem_preimage, mem_image, mem_Union, ideal.quotient.eq],
-  split,
-  { exact assume ⟨a, a_in, h⟩, ⟨⟨_, N.neg_mem h⟩, a, a_in, by simp⟩ },
-  { exact assume ⟨⟨i, hi⟩, a, ha, eq⟩, ⟨a, ha,
-      by rw [← eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub];
-      exact N.neg_mem hi⟩ }
-end
+-- note for the reader: in the following, `mk` is `ideal.quotient.mk`, the canonical map `R → R/I`.
 
 variable [topological_ring α]
 
 lemma quotient_ring.is_open_map_coe : is_open_map (mk N) :=
 begin
-  assume s s_op,
-  show is_open (mk N ⁻¹' (mk N '' s)),
-  rw quotient_ring_saturate N s,
-  exact is_open_Union (assume ⟨n, _⟩, is_open_map_add_left n s s_op)
+  intros s s_op,
+  change is_open (mk N ⁻¹' (mk N '' s)),
+  rw quotient_ring_saturate,
+  exact is_open_Union (λ ⟨n, _⟩, is_open_map_add_left n s s_op)
 end
 
 lemma quotient_ring.quotient_map_coe_coe : quotient_map (λ p : α × α, (mk N p.1, mk N p.2)) :=
-begin
-  apply is_open_map.to_quotient_map,
-  { exact (quotient_ring.is_open_map_coe N).prod (quotient_ring.is_open_map_coe N) },
-  { exact (continuous_quot_mk.comp continuous_fst).prod_mk
-          (continuous_quot_mk.comp continuous_snd) },
-  { rintro ⟨⟨x⟩, ⟨y⟩⟩,
-    exact ⟨(x, y), rfl⟩ }
-end
+is_open_map.to_quotient_map
+((quotient_ring.is_open_map_coe N).prod (quotient_ring.is_open_map_coe N))
+((continuous_quot_mk.comp continuous_fst).prod_mk (continuous_quot_mk.comp continuous_snd))
+(by rintro ⟨⟨x⟩, ⟨y⟩⟩; exact ⟨(x, y), rfl⟩)
 
 instance topological_ring_quotient : topological_ring N.quotient :=
 { continuous_add :=
     have cont : continuous (mk N ∘ (λ (p : α × α), p.fst + p.snd)) :=
       continuous_quot_mk.comp continuous_add,
-    (quotient_map.continuous_iff (quotient_ring.quotient_map_coe_coe N)).2 cont,
+    (quotient_map.continuous_iff (quotient_ring.quotient_map_coe_coe N)).mpr cont,
   continuous_neg :=
-  begin
-    convert continuous_quotient_lift _ (continuous_quot_mk.comp continuous_neg),
-    apply_instance,
-  end,
+    by convert continuous_quotient_lift _ (continuous_quot_mk.comp continuous_neg); apply_instance,
   continuous_mul :=
     have cont : continuous (mk N ∘ (λ (p : α × α), p.fst * p.snd)) :=
       continuous_quot_mk.comp continuous_mul,
-    (quotient_map.continuous_iff (quotient_ring.quotient_map_coe_coe N)).2 cont }
+    (quotient_map.continuous_iff (quotient_ring.quotient_map_coe_coe N)).mpr cont }
 
 end topological_ring