feat(ring_theory): every division_ring is_noetherian (#7661)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

src/ring_theory/ideal/basic.lean

@@ -88,7 +88,7 @@ lemma span_mono {s t : set α} : s ⊆ t → span s ≤ span t := submodule.span
 
 @[simp] lemma span_eq : span (I : set α) = I := submodule.span_eq _
 
-@[simp] lemma span_singleton_one : span (1 : set α) = ⊤ :=
+@[simp] lemma span_singleton_one : span ({1} : set α) = ⊤ :=
 (eq_top_iff_one _).2 $ subset_span $ mem_singleton _
 
 lemma mem_span_insert {s : set α} {x y} :
@@ -104,6 +104,8 @@ submodule.span_singleton_eq_bot
 
 @[simp] lemma span_zero : span (0 : set α) = ⊥ := by rw [←set.singleton_zero, span_singleton_eq_bot]
 
+@[simp] lemma span_one : span (1 : set α) = ⊤ := by rw [←set.singleton_one, span_singleton_one]
+
 /--
 The ideal generated by an arbitrary binary relation.
 -/
@@ -313,7 +315,7 @@ lemma span_singleton_mul_left_unit {a : α} (h2 : is_unit a) (x : α) :
   span ({a * x} : set α) = span {x} := by rw [mul_comm, span_singleton_mul_right_unit h2]
 
 lemma span_singleton_eq_top {x} : span ({x} : set α) = ⊤ ↔ is_unit x :=
-by rw [is_unit_iff_dvd_one, ← span_singleton_le_span_singleton, singleton_one, span_singleton_one,
+by rw [is_unit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one,
   eq_top_iff]
 
 theorem span_singleton_prime {p : α} (hp : p ≠ 0) :
@@ -390,6 +392,35 @@ end ideal
 
 end ring
 
+section division_ring
+variables {K : Type u} [division_ring K] (I : ideal K)
+
+namespace ideal
+
+/-- All ideals in a division ring are trivial. -/
+lemma eq_bot_or_top : I = ⊥ ∨ I = ⊤ :=
+begin
+  rw or_iff_not_imp_right,
+  change _ ≠ _ → _,
+  rw ideal.ne_top_iff_one,
+  intro h1,
+  rw eq_bot_iff,
+  intros r hr,
+  by_cases H : r = 0, {simpa},
+  simpa [H, h1] using I.mul_mem_left r⁻¹ hr,
+end
+
+lemma eq_bot_of_prime [h : I.is_prime] : I = ⊥ :=
+or_iff_not_imp_right.mp I.eq_bot_or_top h.1
+
+lemma bot_is_maximal : is_maximal (⊥ : ideal K) :=
+⟨⟨λ h, absurd ((eq_top_iff_one (⊤ : ideal K)).mp rfl) (by rw ← h; simp),
+λ I hI, or_iff_not_imp_left.mp (eq_bot_or_top I) (ne_of_gt hI)⟩⟩
+
+end ideal
+
+end division_ring
+
 section comm_ring
 
 namespace ideal
@@ -534,28 +565,6 @@ def lift (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0
 
 end quotient
 
-/-- All ideals in a field are trivial. -/
-lemma eq_bot_or_top {K : Type u} [field K] (I : ideal K) :
-  I = ⊥ ∨ I = ⊤ :=
-begin
-  rw or_iff_not_imp_right,
-  change _ ≠ _ → _,
-  rw ideal.ne_top_iff_one,
-  intro h1,
-  rw eq_bot_iff,
-  intros r hr,
-  by_cases H : r = 0, {simpa},
-  simpa [H, h1] using I.mul_mem_left r⁻¹ hr,
-end
-
-lemma eq_bot_of_prime {K : Type u} [field K] (I : ideal K) [h : I.is_prime] :
-  I = ⊥ :=
-or_iff_not_imp_right.mp I.eq_bot_or_top h.1
-
-lemma bot_is_maximal {K : Type u} [field K] : is_maximal (⊥ : ideal K) :=
-⟨⟨λ h, absurd ((eq_top_iff_one (⊤ : ideal K)).mp rfl) (by rw ← h; simp),
-λ I hI, or_iff_not_imp_left.mp (eq_bot_or_top I) (ne_of_gt hI)⟩⟩
-
 section pi
 variables (ι : Type v)
 

src/ring_theory/ideal/operations.lean

@@ -317,7 +317,7 @@ by { unfold span, rw [submodule.span_mul_span, set.singleton_mul_singleton], }
 lemma span_singleton_pow (s : R) (n : ℕ):
   span {s} ^ n = (span {s ^ n} : ideal R) :=
 begin
-  induction n with n ih, { simp [set.singleton_one] },
+  induction n with n ih, { simp [set.singleton_one], },
   simp only [pow_succ, ih, span_singleton_mul_span_singleton],
 end
 
@@ -1267,7 +1267,7 @@ end
   (⊥ : ideal I.quotient).is_maximal ↔ I.is_maximal :=
 ⟨λ hI, (@mk_ker _ _ I) ▸
   @comap_is_maximal_of_surjective _ _ _ _ (quotient.mk I) ⊥ quotient.mk_surjective hI,
- λ hI, @bot_is_maximal _ (@quotient.field _ _ I hI) ⟩
+ λ hI, @bot_is_maximal _ (@field.to_division_ring _ (@quotient.field _ _ I hI)) ⟩
 
 section quotient_algebra
 

src/ring_theory/principal_ideal_domain.lean

@@ -8,7 +8,7 @@ import ring_theory.unique_factorization_domain
 /-!
 # Principal ideal rings and principal ideal domains
 
-A principal ideal ring (PIR) is a commutative ring in which all ideals are principal. A
+A principal ideal ring (PIR) is a ring in which all left ideals are principal. A
 principal ideal domain (PID) is an integral domain which is a principal ideal ring.
 
 # Main definitions
@@ -17,8 +17,7 @@ Note that for principal ideal domains, one should use
 `[integral_domain R] [is_principal_ideal_ring R]`. There is no explicit definition of a PID.
 Theorems about PID's are in the `principal_ideal_ring` namespace.
 
-- `is_principal_ideal_ring`: a predicate on commutative rings, saying that every
-  ideal is principal.
+- `is_principal_ideal_ring`: a predicate on rings, saying that every left ideal is principal.
 - `generator`: a generator of a principal ideal (or more generally submodule)
 - `to_unique_factorization_monoid`: a PID is a unique factorization domain
 
@@ -35,19 +34,39 @@ open set function
 open submodule
 open_locale classical
 
+section
+variables [ring R] [add_comm_group M] [module R M]
+
 /-- An `R`-submodule of `M` is principal if it is generated by one element. -/
-class submodule.is_principal [ring R] [add_comm_group M] [module R M] (S : submodule R M) : Prop :=
+class submodule.is_principal (S : submodule R M) : Prop :=
 (principal [] : ∃ a, S = span R {a})
 
-/-- A commutative ring is a principal ideal ring if all ideals are principal. -/
-class is_principal_ideal_ring (R : Type u) [comm_ring R] : Prop :=
+instance bot_is_principal : (⊥ : submodule R M).is_principal :=
+⟨⟨0, by simp⟩⟩
+
+instance top_is_principal : (⊤ : submodule R R).is_principal :=
+⟨⟨1, ideal.span_singleton_one.symm⟩⟩
+
+variables (R)
+
+/-- A ring is a principal ideal ring if all (left) ideals are principal. -/
+class is_principal_ideal_ring (R : Type u) [ring R] : Prop :=
 (principal : ∀ (S : ideal R), S.is_principal)
 
 attribute [instance] is_principal_ideal_ring.principal
 
+@[priority 100]
+instance division_ring.is_principal_idea_ring (K : Type u) [division_ring K] :
+  is_principal_ideal_ring K :=
+{ principal := λ S, by rcases ideal.eq_bot_or_top S with (rfl|rfl); apply_instance }
+
+end
+
 namespace submodule.is_principal
+variables [add_comm_group M]
 
-variables [comm_ring R] [add_comm_group M] [module R M]
+section ring
+variables [ring R] [module R M]
 
 /-- `generator I`, if `I` is a principal submodule, is an `x ∈ M` such that `span R {x} = I` -/
 noncomputable def generator (S : submodule R M) [S.is_principal] : M :=
@@ -63,20 +82,27 @@ lemma mem_iff_eq_smul_generator (S : submodule R M) [S.is_principal] {x : M} :
   x ∈ S ↔ ∃ s : R, x = s • generator S :=
 by simp_rw [@eq_comm _ x, ← mem_span_singleton, span_singleton_generator]
 
-lemma mem_iff_generator_dvd (S : ideal R) [S.is_principal] {x : R} : x ∈ S ↔ generator S ∣ x :=
-(mem_iff_eq_smul_generator S).trans (exists_congr (λ a, by simp only [mul_comm, smul_eq_mul]))
-
 lemma eq_bot_iff_generator_eq_zero (S : submodule R M) [S.is_principal] :
   S = ⊥ ↔ generator S = 0 :=
 by rw [← @span_singleton_eq_bot R M, span_singleton_generator]
 
+end ring
+
+section comm_ring
+variables [comm_ring R] [module R M]
+
+lemma mem_iff_generator_dvd (S : ideal R) [S.is_principal] {x : R} : x ∈ S ↔ generator S ∣ x :=
+(mem_iff_eq_smul_generator S).trans (exists_congr (λ a, by simp only [mul_comm, smul_eq_mul]))
+
 lemma prime_generator_of_is_prime (S : ideal R) [submodule.is_principal S] [is_prime : S.is_prime]
   (ne_bot : S ≠ ⊥) :
   prime (generator S) :=
 ⟨λ h, ne_bot ((eq_bot_iff_generator_eq_zero S).2 h),
  λ h, is_prime.ne_top (S.eq_top_of_is_unit_mem (generator_mem S) h),
  by simpa only [← mem_iff_generator_dvd S] using is_prime.2⟩
 
+end comm_ring
+
 end submodule.is_principal
 
 namespace is_prime
@@ -137,18 +163,18 @@ end
 namespace principal_ideal_ring
 open is_principal_ideal_ring
 
-variables [integral_domain R] [is_principal_ideal_ring R]
-
 @[priority 100] -- see Note [lower instance priority]
-instance is_noetherian_ring : is_noetherian_ring R :=
+instance is_noetherian_ring [ring R] [is_principal_ideal_ring R] :
+  is_noetherian_ring R :=
 is_noetherian_ring_iff.2 ⟨assume s : ideal R,
 begin
   rcases (is_principal_ideal_ring.principal s).principal with ⟨a, rfl⟩,
   rw [← finset.coe_singleton],
   exact ⟨{a}, set_like.coe_injective rfl⟩
 end⟩
 
-lemma is_maximal_of_irreducible {p : R} (hp : irreducible p) :
+lemma is_maximal_of_irreducible [comm_ring R] [is_principal_ideal_ring R]
+  {p : R} (hp : irreducible p) :
   ideal.is_maximal (span R ({p} : set R)) :=
 ⟨⟨mt ideal.span_singleton_eq_top.1 hp.1, λ I hI, begin
   rcases principal I with ⟨a, rfl⟩,
@@ -158,6 +184,8 @@ lemma is_maximal_of_irreducible {p : R} (hp : irreducible p) :
   erw [ideal.span_singleton_le_span_singleton, is_unit.mul_right_dvd hb]
 end⟩⟩
 
+variables [integral_domain R] [is_principal_ideal_ring R]
+
 lemma irreducible_iff_prime {p : R} : irreducible p ↔ prime p :=
 ⟨λ hp, (ideal.span_singleton_prime hp.ne_zero).1 $
     (is_maximal_of_irreducible hp).is_prime,