From c63dad10f242dc7bc6cae151f2e276bddc5d9aea Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 5 Aug 2020 11:37:40 +0000
Subject: [PATCH] chore(ring_theory/ideals): Move the definition of ideals out
 of algebra/module (#3692)

Neatness was the main motivation - it makes it easier to reason about what would need doing in #3635.
It also results in somewhere sensible for the docs about ideals. Also adds a very minimal docstring to `ring_theory/ideals.lean`.
---
 src/algebra/module/basic.lean | 27 ----------------------
 src/ring_theory/ideals.lean   | 43 ++++++++++++++++++++++++++++++++++-
 2 files changed, 42 insertions(+), 28 deletions(-)

diff --git a/src/algebra/module/basic.lean b/src/algebra/module/basic.lean
index 83d6d5c401019..1a269c6aace1f 100644
--- a/src/algebra/module/basic.lean
+++ b/src/algebra/module/basic.lean
@@ -571,33 +571,6 @@ end add_comm_group
 
 end submodule
 
--- TODO: Do we want one-sided ideals?
-
-/-- Ideal in a commutative ring is an additive subgroup `s` such that
-`a * b ∈ s` whenever `b ∈ s`. We define `ideal R` as `submodule R R`. -/
-@[reducible] def ideal (R : Type u) [comm_ring R] := submodule R R
-
-namespace ideal
-variables [comm_ring R] (I : ideal R) {a b : R}
-
-protected lemma zero_mem : (0 : R) ∈ I := I.zero_mem
-
-protected lemma add_mem : a ∈ I → b ∈ I → a + b ∈ I := I.add_mem
-
-lemma neg_mem_iff : -a ∈ I ↔ a ∈ I := I.neg_mem_iff
-
-lemma add_mem_iff_left : b ∈ I → (a + b ∈ I ↔ a ∈ I) := I.add_mem_iff_left
-
-lemma add_mem_iff_right : a ∈ I → (a + b ∈ I ↔ b ∈ I) := I.add_mem_iff_right
-
-protected lemma sub_mem : a ∈ I → b ∈ I → a - b ∈ I := I.sub_mem
-
-lemma mul_mem_left : b ∈ I → a * b ∈ I := I.smul_mem _
-
-lemma mul_mem_right (h : a ∈ I) : a * b ∈ I := mul_comm b a ▸ I.mul_mem_left h
-
-end ideal
-
 /--
 Vector spaces are defined as an `abbreviation` for semimodules,
 if the base ring is a field.
diff --git a/src/ring_theory/ideals.lean b/src/ring_theory/ideals.lean
index 062a835e0ec71..3bf4f403f6d53 100644
--- a/src/ring_theory/ideals.lean
+++ b/src/ring_theory/ideals.lean
@@ -6,13 +6,54 @@ Authors: Kenny Lau, Chris Hughes, Mario Carneiro
 import algebra.associated
 import linear_algebra.basic
 import order.zorn
+/-!
+
+# Ideals over a ring
+
+This file defines `ideal R`, the type of ideals over a commutative ring `R`.
+
+## Implementation notes
+
+`ideal R` is implemented using `submodule R R`, where `•` is interpreted as `*`.
+
+## TODO
+
+Support one-sided ideals, and ideals over non-commutative rings
+-/
 
 universes u v w
-variables {α : Type u} {β : Type v} {a b : α}
+variables {α : Type u} {β : Type v}
 open set function
 
 open_locale classical big_operators
 
+/-- Ideal in a commutative ring is an additive subgroup `s` such that
+`a * b ∈ s` whenever `b ∈ s`. -/
+@[reducible] def ideal (R : Type u) [comm_ring R] := submodule R R
+
+namespace ideal
+variables [comm_ring α] (I : ideal α) {a b : α}
+
+protected lemma zero_mem : (0 : α) ∈ I := I.zero_mem
+
+protected lemma add_mem : a ∈ I → b ∈ I → a + b ∈ I := I.add_mem
+
+lemma neg_mem_iff : -a ∈ I ↔ a ∈ I := I.neg_mem_iff
+
+lemma add_mem_iff_left : b ∈ I → (a + b ∈ I ↔ a ∈ I) := I.add_mem_iff_left
+
+lemma add_mem_iff_right : a ∈ I → (a + b ∈ I ↔ b ∈ I) := I.add_mem_iff_right
+
+protected lemma sub_mem : a ∈ I → b ∈ I → a - b ∈ I := I.sub_mem
+
+lemma mul_mem_left : b ∈ I → a * b ∈ I := I.smul_mem _
+
+lemma mul_mem_right (h : a ∈ I) : a * b ∈ I := mul_comm b a ▸ I.mul_mem_left h
+end ideal
+
+variables {a b : α}
+
+-- A separate namespace definition is needed because the variables were historically in a different order
 namespace ideal
 variables [comm_ring α] (I : ideal α)