feat(linear_algebra,ring_theory): refactoring modules (#456)

Co-authored with Kenny Lau. See also
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/module.20refactoring for discussion.

Major changes made:

- `semimodule α β` and `module α β` and `vector_space α β` now take one more argument, that `β` is an `add_comm_group`, i.e. before making an instance of a module, you need to prove that it's an abelian group first.
- vector space is no longer over a field, but a discrete field.
- The idiom for making an instance `module α β` (after proving that `β` is an abelian group) is `module.of_core { smul := sorry, smul_add  := sorry, add_smul := sorry, mul_smul := sorry, one_smul := sorry }`.
- `is_linear_map` and `linear_map` are now both structures, and they are independent, meaning that `linear_map` is no longer defined as `subtype is_linear_map`. The idiom for making `linear_map` from `is_linear_map` is `is_linear_map.mk' (f : M -> N) (sorry : is_linear_map f)`, and the idiom for making `is_linear_map` from `linear_map` is `f.is_linear` (i.e. `linear_map.is_linear f`).
- `is_linear_map.add` etc no longer exist. instead, you can now add two linear maps together, etc.
- the class`is_submodule` is gone, replaced by the structure `submodule` which contains a carrier, i.e. if `N : submodule R M` then `N.carrier` is a type. And there is an instance `module R N` in the same situation.
- similarly, the class `is_ideal` is gone, replaced by the structure `ideal`, which also contains a carrier.
- endomorphism ring and general linear group are defined.
- submodules form a complete lattice. the trivial ideal is now idiomatically the bottom element, and the universal ideal the top element.
- `linear_algebra/quotient_module.lean` is deleted, and it's now `submodule.quotient` (so if `N : submodule R M` then `submodule R N.quotient`) Similarly, `quotient_ring.quotient` is replaced by `ideal.quotient`. The canonical map from `N` to `N.quotient` is `submodule.quotient.mk`, and the canonical map from the ideal `I` to `I.quotient` is `ideal.quotient.mk I`.
- `linear_equiv` is now based on a linear map and an equiv, and the difference being that now you need to prove that the inverse is also linear, and there is currently no interface to get around that.
- Everything you want to know about linear independence and basis is now in the newly created file `linear_algebra/basis.lean`.
- Everything you want to know about linear combinations is now in the newly created file `linear_algebra/lc.lean`.
- `linear_algebra/linear_map_module.lean` and `linear_algebra/prod_module.lean` and `linear_algebra/quotient_module.lean` and `linear_algebra/submodule.lean` and `linear_algebra/subtype_module.lean` are deleted (with their contents placed elsewhere).

squashed commits:

* feat(linear_algebra/basic): product modules, cat/lat structure

* feat(linear_algebra/basic): refactoring quotient_module

* feat(linear_algebra/basic): merge in submodule.lean

* feat(linear_algebra/basic): merge in linear_map_module.lean

* refactor(linear_algebra/dimension): update for new modules

* feat(ring_theory/ideals): convert ideals

* refactor tensor product

* simplify local ring proof for Zp

* refactor(ring_theory/noetherian)

* refactor(ring_theory/localization)

* refactor(linear_algebra/tensor_product)

* feat(data/polynomial): lcoeff

algebra/order.lean

@@ -22,6 +22,10 @@ lt_of_le_not_le h₁ $ mt (le_antisymm h₁) h₂
 lemma lt_iff_le_and_ne [partial_order α] {a b : α} : a < b ↔ a ≤ b ∧ a ≠ b :=
 ⟨λ h, ⟨le_of_lt h, ne_of_lt h⟩, λ ⟨h1, h2⟩, lt_of_le_of_ne h1 h2⟩
 
+lemma eq_iff_le_not_lt [partial_order α] {a b : α} : a = b ↔ a ≤ b ∧ ¬ a < b :=
+⟨λ h, ⟨le_of_eq h, h ▸ lt_irrefl _⟩, λ ⟨h₁, h₂⟩, le_antisymm h₁ $
+  classical.by_contradiction $ λ h₃, h₂ (lt_of_le_not_le h₁ h₃)⟩
+
 lemma eq_or_lt_of_le [partial_order α] {a b : α} (h : a ≤ b) : a = b ∨ a < b :=
 (lt_or_eq_of_le h).symm
 

algebra/pi_instances.lean

@@ -61,9 +61,9 @@ instance add_comm_group     [∀ i, add_comm_group     $ f i] : add_comm_group
 instance ring               [∀ i, ring               $ f i] : ring               (Π i : I, f i) := by pi_instance
 instance comm_ring          [∀ i, comm_ring          $ f i] : comm_ring          (Π i : I, f i) := by pi_instance
 
-instance semimodule   (α) {r : semiring α} [∀ i, semimodule α $ f i]   : semimodule α (Π i : I, f i)   := by pi_instance
-instance module       (α) {r : ring α}     [∀ i, module α $ f i]       : module α (Π i : I, f i)       := {..pi.semimodule α}
-instance vector_space (α) {r : field α}    [∀ i, vector_space α $ f i] : vector_space α (Π i : I, f i) := {..pi.module α}
+instance semimodule   (α) {r : semiring α}       [∀ i, add_comm_monoid $ f i] [∀ i, semimodule α $ f i]   : semimodule α (Π i : I, f i)   := by pi_instance
+instance module       (α) {r : ring α}           [∀ i, add_comm_group $ f i]  [∀ i, module α $ f i]       : module α (Π i : I, f i)       := {..pi.semimodule α}
+instance vector_space (α) {r : discrete_field α} [∀ i, add_comm_group $ f i]  [∀ i, vector_space α $ f i] : vector_space α (Π i : I, f i) := {..pi.module α}
 
 instance left_cancel_semigroup [∀ i, left_cancel_semigroup $ f i] : left_cancel_semigroup (Π i : I, f i) :=
 by pi_instance
@@ -113,7 +113,6 @@ variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {p q : α × β}
 
 instance [has_add α] [has_add β] : has_add (α × β) :=
 ⟨λp q, (p.1 + q.1, p.2 + q.2)⟩
-
 @[to_additive prod.has_add]
 instance [has_mul α] [has_mul β] : has_mul (α × β) :=
 ⟨λp q, (p.1 * q.1, p.2 * q.2)⟩
@@ -122,26 +121,31 @@ instance [has_mul α] [has_mul β] : has_mul (α × β) :=
 lemma fst_mul [has_mul α] [has_mul β] : (p * q).1 = p.1 * q.1 := rfl
 @[simp, to_additive prod.snd_add]
 lemma snd_mul [has_mul α] [has_mul β] : (p * q).2 = p.2 * q.2 := rfl
+@[simp, to_additive prod.mk_add_mk]
+lemma mk_mul_mk [has_mul α] [has_mul β] (a₁ a₂ : α) (b₁ b₂ : β) :
+  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂) := rfl
 
 instance [has_zero α] [has_zero β] : has_zero (α × β) := ⟨(0, 0)⟩
-
 @[to_additive prod.has_zero]
 instance [has_one α] [has_one β] : has_one (α × β) := ⟨(1, 1)⟩
 
 @[simp, to_additive prod.fst_zero]
 lemma fst_one [has_one α] [has_one β] : (1 : α × β).1 = 1 := rfl
 @[simp, to_additive prod.snd_zero]
 lemma snd_one [has_one α] [has_one β] : (1 : α × β).2 = 1 := rfl
+@[to_additive prod.zero_eq_mk]
+lemma one_eq_mk [has_one α] [has_one β] : (1 : α × β) = (1, 1) := rfl
 
 instance [has_neg α] [has_neg β] : has_neg (α × β) := ⟨λp, (- p.1, - p.2)⟩
-
 @[to_additive prod.has_neg]
 instance [has_inv α] [has_inv β] : has_inv (α × β) := ⟨λp, (p.1⁻¹, p.2⁻¹)⟩
 
 @[simp, to_additive prod.fst_neg]
 lemma fst_inv [has_inv α] [has_inv β] : (p⁻¹).1 = (p.1)⁻¹ := rfl
 @[simp, to_additive prod.snd_neg]
 lemma snd_inv [has_inv α] [has_inv β] : (p⁻¹).2 = (p.2)⁻¹ := rfl
+@[to_additive prod.neg_mk]
+lemma inv_mk [has_inv α] [has_inv β] (a : α) (b : β) : (a, b)⁻¹ = (a⁻¹, b⁻¹) := rfl
 
 instance [add_semigroup α] [add_semigroup β] : add_semigroup (α × β) :=
 { add_assoc := assume a b c, mk.inj_iff.mpr ⟨add_assoc _ _ _, add_assoc _ _ _⟩,
@@ -252,14 +256,28 @@ by constructor; simp [inl, inr] {contextual := tt}
 
 instance [has_scalar α β] [has_scalar α γ] : has_scalar α (β × γ) := ⟨λa p, (a • p.1, a • p.2)⟩
 
-instance {r : ring α} [module α β] [module α γ] : module α (β × γ) :=
-{ smul_add  := assume a p₁ p₂, mk.inj_iff.mpr ⟨smul_add, smul_add⟩,
-  add_smul  := assume a p₁ p₂, mk.inj_iff.mpr ⟨add_smul, add_smul⟩,
-  mul_smul  := assume a₁ a₂ p, mk.inj_iff.mpr ⟨mul_smul, mul_smul⟩,
-  one_smul  := assume ⟨b, c⟩, mk.inj_iff.mpr ⟨one_smul, one_smul⟩,
+@[simp] theorem smul_fst [has_scalar α β] [has_scalar α γ]
+  (a : α) (x : β × γ) : (a • x).1 = a • x.1 := rfl
+@[simp] theorem smul_snd [has_scalar α β] [has_scalar α γ]
+  (a : α) (x : β × γ) : (a • x).2 = a • x.2 := rfl
+@[simp] theorem smul_mk [has_scalar α β] [has_scalar α γ]
+  (a : α) (b : β) (c : γ) : a • (b, c) = (a • b, a • c) := rfl
+
+instance {r : semiring α} [add_comm_monoid β] [add_comm_monoid γ]
+  [semimodule α β] [semimodule α γ] : semimodule α (β × γ) :=
+{ smul_add  := assume a p₁ p₂, mk.inj_iff.mpr ⟨smul_add _ _ _, smul_add _ _ _⟩,
+  add_smul  := assume a p₁ p₂, mk.inj_iff.mpr ⟨add_smul _ _ _, add_smul _ _ _⟩,
+  mul_smul  := assume a₁ a₂ p, mk.inj_iff.mpr ⟨mul_smul _ _ _, mul_smul _ _ _⟩,
+  one_smul  := assume ⟨b, c⟩, mk.inj_iff.mpr ⟨one_smul _, one_smul _⟩,
+  zero_smul := assume ⟨b, c⟩, mk.inj_iff.mpr ⟨zero_smul _, zero_smul _⟩,
+  smul_zero := assume a, mk.inj_iff.mpr ⟨smul_zero _, smul_zero _⟩,
   .. prod.has_scalar }
 
-instance {r : field α} [vector_space α β] [vector_space α γ] : vector_space α (β × γ) := {}
+instance {r : ring α} [add_comm_group β] [add_comm_group γ]
+  [module α β] [module α γ] : module α (β × γ) := {}
+
+instance {r : discrete_field α} [add_comm_group β] [add_comm_group γ]
+  [vector_space α β] [vector_space α γ] : vector_space α (β × γ) := {}
 
 end prod
 
@@ -271,4 +289,4 @@ lemma prod_mk_prod {α β γ : Type*} [comm_monoid α] [comm_monoid β] (s : fin
 by haveI := classical.dec_eq γ; exact
 finset.induction_on s rfl (by simp [prod.ext_iff] {contextual := tt})
 
-end finset
+end finset

analysis/bounded_linear_maps.lean

@@ -17,7 +17,7 @@ mul_inv_eq hb ha
 noncomputable theory
 local attribute [instance] classical.prop_decidable
 
-local notation f `→_{`:50 a `}`:0 b := filter.tendsto f (nhds a) (nhds b)
+local notation f ` →_{`:50 a `} `:0 b := filter.tendsto f (nhds a) (nhds b)
 
 open filter (tendsto)
 
@@ -44,13 +44,13 @@ lemma is_linear_map.with_bound
 namespace is_bounded_linear_map
 
 lemma zero : is_bounded_linear_map (λ (x:E), (0:F)) :=
-is_linear_map.map_zero.with_bound 0 $ by simp [le_refl]
+(0 : E →ₗ F).is_linear.with_bound 0 $ by simp [le_refl]
 
 lemma id : is_bounded_linear_map (λ (x:E), x) :=
-is_linear_map.id.with_bound 1 $ by simp [le_refl]
+linear_map.id.is_linear.with_bound 1 $ by simp [le_refl]
 
 lemma smul {f : E → F} (c : k) : is_bounded_linear_map f → is_bounded_linear_map (λ e, c • f e)
-| ⟨hf, ⟨M, hM, h⟩⟩ := hf.map_smul_right.with_bound (∥c∥ * M) $ assume x,
+| ⟨hf, ⟨M, hM, h⟩⟩ := (c • hf.mk' f).is_linear.with_bound (∥c∥ * M) $ assume x,
   calc ∥c • f x∥ = ∥c∥ * ∥f x∥ : norm_smul c (f x)
     ... ≤ ∥c∥ * (M * ∥x∥) : mul_le_mul_of_nonneg_left (h x) (norm_nonneg c)
     ... = (∥c∥ * M) * ∥x∥ : (mul_assoc _ _ _).symm
@@ -63,7 +63,7 @@ end
 
 lemma add {f : E → F} {g : E → F} :
   is_bounded_linear_map f → is_bounded_linear_map g → is_bounded_linear_map (λ e, f e + g e)
-| ⟨hlf, Mf, hMf, hf⟩  ⟨hlg, Mg, hMg, hg⟩ := (hlf.map_add hlg).with_bound (Mf + Mg) $ assume x,
+| ⟨hlf, Mf, hMf, hf⟩  ⟨hlg, Mg, hMg, hg⟩ := (hlf.mk' _ + hlg.mk' _).is_linear.with_bound (Mf + Mg) $ assume x,
   calc ∥f x + g x∥ ≤ ∥f x∥ + ∥g x∥ : norm_triangle _ _
     ... ≤ Mf * ∥x∥ + Mg * ∥x∥ : add_le_add (hf x) (hg x)
     ... ≤ (Mf + Mg) * ∥x∥ : by rw add_mul
@@ -73,15 +73,15 @@ lemma sub {f : E → F} {g : E → F} (hf : is_bounded_linear_map f) (hg : is_bo
 
 lemma comp {f : E → F} {g : F → G} :
   is_bounded_linear_map g → is_bounded_linear_map f → is_bounded_linear_map (g ∘ f)
-| ⟨hlg, Mg, hMg, hg⟩ ⟨hlf, Mf, hMf, hf⟩ := (hlg.comp hlf).with_bound (Mg * Mf) $ assume x,
+| ⟨hlg, Mg, hMg, hg⟩ ⟨hlf, Mf, hMf, hf⟩ := ((hlg.mk' _).comp (hlf.mk' _)).is_linear.with_bound (Mg * Mf) $ assume x,
   calc ∥g (f x)∥ ≤ Mg * ∥f x∥ : hg _
     ... ≤ Mg * (Mf * ∥x∥) : mul_le_mul_of_nonneg_left (hf _) (le_of_lt hMg)
     ... = Mg * Mf * ∥x∥ : (mul_assoc _ _ _).symm
 
-lemma tendsto {L : E → F} (x : E) : is_bounded_linear_map L → tendsto L (nhds x) (nhds (L x))
+lemma tendsto {L : E → F} (x : E) : is_bounded_linear_map L → L →_{x} (L x)
 | ⟨hL, M, hM, h_ineq⟩ := tendsto_iff_norm_tendsto_zero.2 $
   squeeze_zero (assume e, norm_nonneg _)
-    (assume e, calc ∥L e - L x∥ = ∥L (e - x)∥ : by rw ← hL.sub e x
+    (assume e, calc ∥L e - L x∥ = ∥hL.mk' L (e - x)∥ : by rw (hL.mk' _).map_sub e x; refl
       ... ≤ M*∥e-x∥ : h_ineq (e-x))
     (suffices (λ (e : E), M * ∥e - x∥) →_{x} (M * 0), by simpa,
       tendsto_mul tendsto_const_nhds (lim_norm _))
@@ -90,7 +90,7 @@ lemma continuous {L : E → F} (hL : is_bounded_linear_map L) : continuous L :=
 continuous_iff_tendsto.2 $ assume x, hL.tendsto x
 
 lemma lim_zero_bounded_linear_map {L : E → F} (H : is_bounded_linear_map L) : (L →_{0} 0) :=
-by simpa [H.to_is_linear_map.zero] using continuous_iff_tendsto.1 H.continuous 0
+(H.1.mk' _).map_zero ▸ continuous_iff_tendsto.1 H.continuous 0
 
 end is_bounded_linear_map
 
@@ -99,9 +99,10 @@ lemma bounded_continuous_linear_map
   {E : Type*} [normed_space ℝ E] {F : Type*} [normed_space ℝ F] {L : E → F}
   (lin : is_linear_map L) (cont : continuous L) : is_bounded_linear_map L :=
 let ⟨δ, δ_pos, hδ⟩ := exists_delta_of_continuous cont zero_lt_one 0 in
-have H : ∀{a}, ∥a∥ ≤ δ → ∥L a∥ < 1, by simpa [lin.zero, dist_zero_right] using hδ,
+have HL0 : L 0 = 0, from (lin.mk' _).map_zero,
+have H : ∀{a}, ∥a∥ ≤ δ → ∥L a∥ < 1, by simpa only [HL0, dist_zero_right] using hδ,
 lin.with_bound (δ⁻¹) $ assume x,
-classical.by_cases (assume : x = 0, by simp [this, lin.zero]) $
+classical.by_cases (assume : x = 0, by simp only [this, HL0, norm_zero, mul_zero]) $
 assume h : x ≠ 0,
 let p := ∥x∥ * δ⁻¹, q := p⁻¹ in
 have p_inv : p⁻¹ = δ*∥x∥⁻¹, by simp,

analysis/normed_space.lean

@@ -7,7 +7,7 @@ Authors: Patrick Massot, Johannes Hölzl
 -/
 
 import algebra.pi_instances
-import linear_algebra.prod_module
+import linear_algebra.basic
 import analysis.nnreal
 variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*}
 
@@ -285,25 +285,17 @@ end normed_field
 section normed_space
 
 class normed_space (α : out_param $ Type*) (β : Type*) [out_param $ normed_field α]
-  extends has_norm β , vector_space α β, metric_space β :=
-(dist_eq   : ∀ x y, dist x y = norm (x - y))
+  extends normed_group β, vector_space α β :=
 (norm_smul : ∀ a b, norm (a • b) = has_norm.norm a * norm b)
 
 variables [normed_field α]
 
-instance normed_space.to_normed_group [i : normed_space α β] : normed_group β :=
-by refine { add := (+),
-            dist_eq := normed_space.dist_eq,
-            zero := 0,
-            neg := λ x, -x,
-            ..i, .. }; simp
-
 instance normed_field.to_normed_space : normed_space α α :=
 { dist_eq := normed_field.dist_eq,
   norm_smul := normed_field.norm_mul }
 
 lemma norm_smul [normed_space α β] (s : α) (x : β) : ∥s • x∥ = ∥s∥ * ∥x∥ :=
-normed_space.norm_smul _ _
+normed_space.norm_smul s x
 
 lemma nnnorm_smul [normed_space α β] (s : α) (x : β) : nnnorm (s • x) = nnnorm s * nnnorm x :=
 nnreal.eq $ norm_smul s x

analysis/topology/quotient_topological_structures.lean

@@ -113,12 +113,12 @@ attribute [instance] topological_add_group_quotient
 end topological_group
 
 section ideal_is_add_subgroup
-variables [comm_ring α] {M : Type*} [module α M] (N : set α) [is_submodule N]
+variables [comm_ring α] {M : Type*} [add_comm_group M] [module α M] (N : submodule α M)
 
-instance submodule_is_add_subgroup : is_add_subgroup N :=
-{ zero_mem := is_submodule.zero,
-  add_mem  := λ a b, is_submodule.add,
-  neg_mem  := λ a, is_submodule.neg}
+instance submodule_is_add_subgroup : is_add_subgroup ↑N :=
+{ zero_mem := N.zero,
+  add_mem  := N.add,
+  neg_mem  := λ _, N.neg_mem }
 
 end ideal_is_add_subgroup
 
@@ -129,34 +129,34 @@ instance normal_subgroup_of_comm [comm_group α] (s : set α) [hs : is_subgroup
 attribute [instance] normal_add_subgroup_of_comm
 
 section topological_ring
-variables [topological_space α] [comm_ring α] [topological_ring α] (N : set α) [is_ideal N]
-open quotient_ring
+variables [topological_space α] [comm_ring α] [topological_ring α] (N : ideal α)
+open ideal.quotient
 
-instance topological_ring_quotient_topology : topological_space (quotient N) :=
-by dunfold quotient_ring.quotient ; apply_instance
+instance topological_ring_quotient_topology : topological_space N.quotient :=
+by dunfold ideal.quotient submodule.quotient; apply_instance
 
 -- this should be quotient_add_saturate ...
 lemma quotient_ring_saturate (s : set α) :
-  (coe : α → quotient N) ⁻¹' ((coe : α → quotient N) '' s) = (⋃ x : N, (λ y, x.1 + y) '' s) :=
+  mk N ⁻¹' (mk N '' s) = (⋃ x : N, (λ y, x.1 + y) '' s) :=
 begin
   ext x,
-  simp only [mem_preimage_eq, mem_image, mem_Union, quotient_ring.eq],
+  simp only [mem_preimage_eq, mem_image, mem_Union, ideal.quotient.eq],
   split,
-  { exact assume ⟨a, a_in, h⟩, ⟨⟨_, is_ideal.neg_iff.1 h⟩, a, a_in, by simp⟩ },
+  { 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 simp only [eq.symm, -sub_eq_add_neg, add_comm i a, sub_add_eq_sub_sub, sub_self, zero_sub,
-        is_ideal.neg_iff.symm, hi]⟩ }
+      by rw [← eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub];
+      exact N.neg_mem hi⟩ }
 end
 
-lemma quotient_ring.is_open_map_coe : is_open_map (coe : α →  quotient N) :=
+lemma quotient_ring.is_open_map_coe : is_open_map (mk N) :=
 begin
   assume s s_op,
-  show is_open ((coe : α →  quotient N) ⁻¹' (coe '' s)),
+  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)
 end
 
-lemma quotient_ring.quotient_map_coe_coe : quotient_map (λ p : α × α, ((p.1:quotient N), (p.2:quotient N))) :=
+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 is_open_map.prod (quotient_ring.is_open_map_coe N) (quotient_ring.is_open_map_coe N) },
@@ -167,14 +167,14 @@ begin
     exact ⟨(x, y), rfl⟩ }
 end
 
-instance topological_ring_quotient : topological_ring (quotient N) :=
+instance topological_ring_quotient : topological_ring N.quotient :=
 { continuous_add :=
-    have cont : continuous ((coe : α → quotient N) ∘ (λ (p : α × α), p.fst + p.snd)) :=
+    have cont : continuous (mk N ∘ (λ (p : α × α), p.fst + p.snd)) :=
       continuous.comp continuous_add' continuous_quot_mk,
     (quotient_map.continuous_iff (quotient_ring.quotient_map_coe_coe N)).2 cont,
   continuous_neg := continuous_quotient_lift _ (continuous.comp continuous_neg' continuous_quot_mk),
   continuous_mul :=
-    have cont : continuous ((coe : α → quotient N) ∘ (λ (p : α × α), p.fst * p.snd)) :=
+    have cont : continuous (mk N ∘ (λ (p : α × α), p.fst * p.snd)) :=
       continuous.comp continuous_mul' continuous_quot_mk,
     (quotient_map.continuous_iff (quotient_ring.quotient_map_coe_coe N)).2 cont }
 
@@ -183,16 +183,16 @@ end topological_ring
 namespace uniform_space
 
 lemma ring_sep_rel (α) [comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :
-  separation_setoid α = quotient_ring.quotient_rel (closure $ is_ideal.trivial α) :=
+  separation_setoid α = submodule.quotient_rel (ideal.closure ⊥) :=
 setoid.ext $ assume x y, group_separation_rel x y
 
 lemma ring_sep_quot (α) [r : comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :
-  quotient (separation_setoid α) = quotient_ring.quotient (closure $ is_ideal.trivial α) :=
+  quotient (separation_setoid α) = (⊥ : ideal α).closure.quotient :=
 by rw [@ring_sep_rel α r]; refl
 
 def sep_quot_equiv_ring_quot (α)
   [r : comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :
-  quotient (separation_setoid α) ≃ quotient_ring.quotient (closure $ is_ideal.trivial α) :=
+  quotient (separation_setoid α) ≃ (⊥ : ideal α).closure.quotient :=
 quotient.congr $ assume x y, group_separation_rel x y
 
 /- TODO: use a form of transport a.k.a. lift definition a.k.a. transfer -/
@@ -203,7 +203,7 @@ by rw ring_sep_quot α; apply_instance
 instance [comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :
   topological_ring (quotient (separation_setoid α)) :=
 begin
-  convert topological_ring_quotient (closure (is_ideal.trivial α)),
+  convert topological_ring_quotient (⊥ : ideal α).closure,
   { apply ring_sep_rel },
   { dsimp [topological_ring_quotient_topology, quotient.topological_space, to_topological_space],
     congr,

analysis/topology/topological_structures.lean

@@ -406,15 +406,19 @@ end topological_ring
 
 section topological_comm_ring
 universe u'
-variables (α) [topological_space α] [comm_ring α] [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,
+def ideal.closure (S : ideal α) : ideal α :=
+{ carrier := closure S,
+  zero := subset_closure S.zero_mem,
+  add  := assume x y hx hy,
+    mem_closure2 continuous_add' hx hy $ assume a b, S.add_mem,
   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 }
+    mem_closure this hx $ assume a, S.mul_mem_left }
+
+@[simp] lemma ideal.coe_closure (S : ideal α) :
+  (S.closure : set α) = closure S := rfl
 
 end topological_comm_ring