From af913073fc15f5622cbb6fa32940c6ee80116125 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 27 Jan 2021 14:27:48 +0100 Subject: [PATCH 01/14] start using `comm_semiring` in `ideal` --- src/ring_theory/ideal/basic.lean | 122 +++++++++++++++++-------------- 1 file changed, 67 insertions(+), 55 deletions(-) diff --git a/src/ring_theory/ideal/basic.lean b/src/ring_theory/ideal/basic.lean index a4aec2d7c8c5a..bdb9501669392 100644 --- a/src/ring_theory/ideal/basic.lean +++ b/src/ring_theory/ideal/basic.lean @@ -34,21 +34,15 @@ open_locale classical big_operators `a * b ∈ s` whenever `b ∈ s`. If `R` is a ring, then `s` is an additive subgroup. -/ @[reducible] def ideal (R : Type u) [comm_semiring R] := submodule R R +section comm_semiring + namespace ideal -variables [comm_ring α] (I : ideal α) {a b : α} +variables [comm_semiring α] (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 - variables (a) lemma mul_mem_left : b ∈ I → a * b ∈ I := I.smul_mem a variables {a} @@ -62,7 +56,7 @@ 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 α) +variables [comm_semiring α] (I : ideal α) @[ext] lemma ext {I J : ideal α} (h : ∀ x, x ∈ I ↔ x ∈ J) : I = J := submodule.ext h @@ -84,16 +78,6 @@ theorem eq_top_iff_one : I = ⊤ ↔ (1:α) ∈ I := theorem ne_top_iff_one : I ≠ ⊤ ↔ (1:α) ∉ I := not_congr I.eq_top_iff_one -lemma exists_mem_ne_zero_iff_ne_bot : (∃ p ∈ I, p ≠ (0 : α)) ↔ I ≠ ⊥ := -begin - refine ⟨λ h, let ⟨p, hp, hp0⟩ := h in λ h, absurd (h ▸ hp : p ∈ (⊥ : ideal α)) hp0, λ h, _⟩, - contrapose! h, - exact eq_bot_iff.2 (λ x hx, (h x hx).symm ▸ (ideal.zero_mem ⊥)), -end - -lemma exists_mem_ne_zero_of_ne_bot (hI : I ≠ ⊥) : ∃ p ∈ I, p ≠ (0 : α) := -(exists_mem_ne_zero_iff_ne_bot I).mpr hI - @[simp] theorem unit_mul_mem_iff_mem {x y : α} (hy : is_unit y) : y * x ∈ I ↔ x ∈ I := begin @@ -124,9 +108,6 @@ lemma span_mono {s t : set α} : s ⊆ t → span s ≤ span t := submodule.span lemma mem_span_insert {s : set α} {x y} : x ∈ span (insert y s) ↔ ∃ a (z ∈ span s), x = a * y + z := submodule.mem_span_insert -lemma mem_span_insert' {s : set α} {x y} : - x ∈ span (insert y s) ↔ ∃a, x + a * y ∈ span s := submodule.mem_span_insert' - lemma mem_span_singleton' {x y : α} : x ∈ span ({y} : set α) ↔ ∃ a, a * y = x := submodule.mem_span_singleton @@ -172,7 +153,7 @@ lemma span_singleton_mul_left_unit {a : α} (h2 : is_unit a) (x : α) : The ideal generated by an arbitrary binary relation. -/ def of_rel (r : α → α → Prop) : ideal α := -submodule.span α { x | ∃ (a b) (h : r a b), x = a - b } +submodule.span α { x | ∃ (a b) (h : r a b), x + b = a } /-- An ideal `P` of a ring `R` is prime if `P ≠ R` and `xy ∈ P → x ∈ P ∨ y ∈ P` -/ @[class] def is_prime (I : ideal α) : Prop := @@ -227,23 +208,24 @@ theorem is_maximal.eq_of_le {I J : ideal α} (hI : I.is_maximal) (hJ : J ≠ ⊤) (IJ : I ≤ J) : I = J := eq_iff_le_not_lt.2 ⟨IJ, λ h, hJ (hI.2 _ h)⟩ -theorem is_maximal.exists_inv {I : ideal α} - (hI : I.is_maximal) {x} (hx : x ∉ I) : ∃ y, y * x - 1 ∈ I := -begin - cases is_maximal_iff.1 hI with H₁ H₂, - rcases mem_span_insert'.1 (H₂ (span (insert x I)) x - (set.subset.trans (subset_insert _ _) subset_span) - hx (subset_span (mem_insert _ _))) with ⟨y, hy⟩, - rw [span_eq, ← neg_mem_iff, add_comm, neg_add', neg_mul_eq_neg_mul] at hy, - exact ⟨-y, hy⟩ -end - theorem is_maximal.is_prime {I : ideal α} (H : I.is_maximal) : I.is_prime := ⟨H.1, λ x y hxy, or_iff_not_imp_left.2 $ λ hx, begin - cases H.exists_inv hx with z hz, - have := I.mul_mem_left _ hz, - rw [mul_sub, mul_one, mul_comm, mul_assoc, sub_eq_add_neg] at this, - exact I.neg_mem_iff.1 ((I.add_mem_iff_right $ I.mul_mem_left _ hxy).1 this) + let J : ideal α := submodule.span α (insert x ↑I), + have IJ : I ≤ J, + { rw ← span_eq I, + exact (span_mono (subset_insert x ↑I)) }, + have oJ : (1 : α) ∈ J, + { have H1 := H, + cases H1 with Ht Hm, + obtain ⟨-, F⟩ := is_maximal_iff.mp H, + refine F _ x IJ hx _, + refine mem_span_insert.mpr ⟨(1 : α), 0, submodule.zero_mem (span I.carrier), _⟩, + rw [one_mul, add_zero] }, + rcases submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩, + obtain (F : y * 1 = y * (a • x + b)) := congr_arg (λ g : α, y * g) oe, + rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc], + refine submodule.add_mem I (I.mul_mem_left a hxy) (submodule.smul_mem I y _), + rwa submodule.span_eq at h, end⟩ @[priority 100] -- see Note [lower instance priority] @@ -271,7 +253,7 @@ let ⟨I, ⟨hI, _⟩⟩ := exists_le_maximal (⊥ : ideal α) submodule.bot_ne_ /-- If P is not properly contained in any maximal ideal then it is not properly contained in any proper ideal -/ -lemma maximal_of_no_maximal {R : Type u} [comm_ring R] {P : ideal R} +lemma maximal_of_no_maximal {R : Type u} [comm_semiring R] {P : ideal R} (hmax : ∀ m : ideal R, P < m → ¬is_maximal m) (J : ideal R) (hPJ : P < J) : J = ⊤ := begin by_contradiction hnonmax, @@ -295,6 +277,37 @@ lt_of_le_not_le (ideal.span_le.2 $ singleton_subset_iff.2 $ h₂ $ is_unit_of_dvd_one _ $ (mul_dvd_mul_iff_left h₁).1 $ by rwa [mul_one, ← ideal.span_singleton_le_span_singleton] +theorem is_maximal.exists_inv {I : ideal α} + (hI : I.is_maximal) {x} (hx : x ∉ I) : ∃ y, ∃ i ∈ I, y * x + i = 1 := +begin + cases is_maximal_iff.1 hI with H₁ H₂, + rcases mem_span_insert.1 (H₂ (span (insert x I)) x + (set.subset.trans (subset_insert _ _) subset_span) + hx (subset_span (mem_insert _ _))) with ⟨y, z, hz, hy⟩, + refine ⟨y, z, _, hy.symm⟩, + rwa ← span_eq I, +end + +end ideal + +end comm_semiring + +namespace ideal + +variables [comm_ring α] (I : ideal α) {a b : α} + +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 +--λ bi, ⟨λ h, sorry, λ h, ideal.add_mem I h bi⟩ + +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 mem_span_insert' {s : set α} {x y} : + x ∈ span (insert y s) ↔ ∃a, x + a * y ∈ span s := submodule.mem_span_insert' + /-- The quotient `R/I` of a ring `R` by an ideal `I`. -/ def quotient (I : ideal α) := I.quotient @@ -305,11 +318,12 @@ instance (I : ideal α) : has_one I.quotient := ⟨submodule.quotient.mk 1⟩ instance (I : ideal α) : has_mul I.quotient := ⟨λ a b, quotient.lift_on₂' a b (λ a b, submodule.quotient.mk (a * b)) $ -λ a₁ a₂ b₁ b₂ h₁ h₂, begin - apply @quot.sound _ I.quotient_rel.r, - calc a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁ : _ - ... ∈ I : I.add_mem (I.mul_mem_left _ h₁) (I.mul_mem_right _ h₂), - rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁] + λ a₁ a₂ b₁ b₂ h₁ h₂, quot.sound $ begin + obtain F := I.add_mem (I.mul_mem_left a₂ h₁) (I.mul_mem_right b₁ h₂), + have : a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁, + { rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁] }, + rw ← this at F, + convert F end⟩ instance (I : ideal α) : comm_ring I.quotient := @@ -372,9 +386,12 @@ lemma exists_inv {I : ideal α} [hI : I.is_maximal] : ∀ {a : I.quotient}, a ≠ 0 → ∃ b : I.quotient, a * b = 1 := begin rintro ⟨a⟩ h, - cases hI.exists_inv (mt eq_zero_iff_mem.2 h) with b hb, - rw [mul_comm] at hb, - exact ⟨mk _ b, quot.sound hb⟩ + rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩, + rw [mul_comm] at abc, + refine ⟨mk _ b, quot.sound _⟩, --quot.sound hb + rw ← eq_sub_iff_add_eq' at abc, + rw [abc, ← neg_mem_iff, neg_sub] at hc, + convert hc, end /-- quotient by maximal ideal is a field. def rather than instance, since users will have @@ -424,13 +441,6 @@ def lift (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0 @[simp] lemma lift_mk (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0) : lift S f H (mk S a) = f a := rfl -@[simp] lemma lift_comp_mk (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0) : - (lift S f H).comp (mk S) = f := ring_hom.ext (λ _, rfl) - -lemma lift_surjective (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0) - (hf : function.surjective f) : function.surjective (lift S f H) := -λ x, let ⟨y, hy⟩ := hf x in ⟨(quotient.mk S) y, by simpa⟩ - end quotient section lattice @@ -618,6 +628,8 @@ end end ideal +variables {a b : α} + /-- The set of non-invertible elements of a monoid. -/ def nonunits (α : Type u) [monoid α] : set α := { a | ¬is_unit a } From 5c994151e205bd11aca2dd4c4d4c0fcce17c4eae Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 27 Jan 2021 14:49:00 +0100 Subject: [PATCH 02/14] fix algebra/ring_quot --- src/algebra/ring_quot.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/algebra/ring_quot.lean b/src/algebra/ring_quot.lean index 657a587208d24..db1d93a0815b2 100644 --- a/src/algebra/ring_quot.lean +++ b/src/algebra/ring_quot.lean @@ -178,7 +178,7 @@ def ring_quot_to_ideal_quotient (r : B → B → Prop) : ring_quot r →+* (ideal.of_rel r).quotient := lift ⟨ideal.quotient.mk (ideal.of_rel r), - λ x y h, quot.sound (submodule.mem_Inf.mpr (λ p w, w ⟨x, y, h, rfl⟩))⟩ + λ x y h, quot.sound (submodule.mem_Inf.mpr (λ p w, w ⟨x, y, h, sub_add_cancel x y⟩))⟩ @[simp] lemma ring_quot_to_ideal_quotient_apply (r : B → B → Prop) (x : B) : ring_quot_to_ideal_quotient r (mk_ring_hom r x) = ideal.quotient.mk _ x := rfl @@ -188,10 +188,11 @@ def ideal_quotient_to_ring_quot (r : B → B → Prop) : (ideal.of_rel r).quotient →+* ring_quot r := ideal.quotient.lift (ideal.of_rel r) (mk_ring_hom r) begin - intros x h, - apply submodule.span_induction h, - { rintros - ⟨a,b,h,rfl⟩, - rw [ring_hom.map_sub, mk_ring_hom_rel h, sub_self], }, + refine λ x h, submodule.span_induction h _ _ _ _, + { rintro y ⟨a, b, h, su⟩, + symmetry' at su, + rw ← ((sub_eq_iff_eq_add)) at su, + rw [ ← su, ring_hom.map_sub, mk_ring_hom_rel h, sub_self], }, { simp, }, { intros a b ha hb, simp [ha, hb], }, { intros a x hx, simp [hx], }, From e1c73cdc0f70ba4de7707b5ae71ef06189ec063d Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 27 Jan 2021 16:07:36 +0100 Subject: [PATCH 03/14] fix ring_theory/jacobson_ideal --- src/ring_theory/ideal/basic.lean | 6 +- src/ring_theory/ideal/basic_n.lean | 873 ++++++++++++++++++++++++++++ src/ring_theory/jacobson_ideal.lean | 8 +- 3 files changed, 881 insertions(+), 6 deletions(-) create mode 100644 src/ring_theory/ideal/basic_n.lean diff --git a/src/ring_theory/ideal/basic.lean b/src/ring_theory/ideal/basic.lean index bdb9501669392..65334462fdf6d 100644 --- a/src/ring_theory/ideal/basic.lean +++ b/src/ring_theory/ideal/basic.lean @@ -444,7 +444,7 @@ def lift (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0 end quotient section lattice -variables {R : Type u} [comm_ring R] +variables {R : Type u} [comm_semiring R] lemma mem_sup_left {S T : ideal R} : ∀ {x : R}, x ∈ S → x ∈ S ⊔ T := show S ≤ S ⊔ T, from le_sup_left @@ -649,11 +649,11 @@ not_congr is_unit_zero_iff @[simp] theorem one_not_mem_nonunits [monoid α] : (1:α) ∉ nonunits α := not_not_intro is_unit_one -theorem coe_subset_nonunits [comm_ring α] {I : ideal α} (h : I ≠ ⊤) : +theorem coe_subset_nonunits [comm_semiring α] {I : ideal α} (h : I ≠ ⊤) : (I : set α) ⊆ nonunits α := λ x hx hu, h $ I.eq_top_of_is_unit_mem hx hu -lemma exists_max_ideal_of_mem_nonunits [comm_ring α] (h : a ∈ nonunits α) : +lemma exists_max_ideal_of_mem_nonunits [comm_semiring α] (h : a ∈ nonunits α) : ∃ I : ideal α, I.is_maximal ∧ a ∈ I := begin have : ideal.span ({a} : set α) ≠ ⊤, diff --git a/src/ring_theory/ideal/basic_n.lean b/src/ring_theory/ideal/basic_n.lean new file mode 100644 index 0000000000000..bdb9501669392 --- /dev/null +++ b/src/ring_theory/ideal/basic_n.lean @@ -0,0 +1,873 @@ +/- +Copyright (c) 2018 Kenny Lau. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kenny Lau, Chris Hughes, Mario Carneiro +-/ +import algebra.associated +import linear_algebra.basic +import order.zorn +import order.atoms +/-! + +# 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. + +See `algebra.ring_quot` for quotients of non-commutative rings. +-/ + +universes u v w +variables {α : Type u} {β : Type v} +open set function + +open_locale classical big_operators + +/-- An ideal in a commutative semiring `R` is an additive submonoid `s` such that +`a * b ∈ s` whenever `b ∈ s`. If `R` is a ring, then `s` is an additive subgroup. -/ +@[reducible] def ideal (R : Type u) [comm_semiring R] := submodule R R + +section comm_semiring + +namespace ideal +variables [comm_semiring α] (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 + +variables (a) +lemma mul_mem_left : b ∈ I → a * b ∈ I := I.smul_mem a +variables {a} + +variables (b) +lemma mul_mem_right (h : a ∈ I) : a * b ∈ I := mul_comm b a ▸ I.mul_mem_left b h +variables {b} +end ideal + +variables {a b : α} + +-- A separate namespace definition is needed because the variables were historically in a different order +namespace ideal +variables [comm_semiring α] (I : ideal α) + +@[ext] lemma ext {I J : ideal α} (h : ∀ x, x ∈ I ↔ x ∈ J) : I = J := +submodule.ext h + +theorem eq_top_of_unit_mem + (x y : α) (hx : x ∈ I) (h : y * x = 1) : I = ⊤ := +eq_top_iff.2 $ λ z _, calc + z = z * (y * x) : by simp [h] + ... = (z * y) * x : eq.symm $ mul_assoc z y x + ... ∈ I : I.mul_mem_left _ hx + +theorem eq_top_of_is_unit_mem {x} (hx : x ∈ I) (h : is_unit x) : I = ⊤ := +let ⟨y, hy⟩ := is_unit_iff_exists_inv'.1 h in eq_top_of_unit_mem I x y hx hy + +theorem eq_top_iff_one : I = ⊤ ↔ (1:α) ∈ I := +⟨by rintro rfl; trivial, + λ h, eq_top_of_unit_mem _ _ 1 h (by simp)⟩ + +theorem ne_top_iff_one : I ≠ ⊤ ↔ (1:α) ∉ I := +not_congr I.eq_top_iff_one + +@[simp] +theorem unit_mul_mem_iff_mem {x y : α} (hy : is_unit y) : y * x ∈ I ↔ x ∈ I := +begin + refine ⟨λ h, _, λ h, I.mul_mem_left y h⟩, + obtain ⟨y', hy'⟩ := is_unit_iff_exists_inv.1 hy, + have := I.mul_mem_left y' h, + rwa [← mul_assoc, mul_comm y' y, hy', one_mul] at this, +end + +@[simp] +theorem mul_unit_mem_iff_mem {x y : α} (hy : is_unit y) : x * y ∈ I ↔ x ∈ I := +mul_comm y x ▸ unit_mul_mem_iff_mem I hy + +/-- The ideal generated by a subset of a ring -/ +def span (s : set α) : ideal α := submodule.span α s + +lemma subset_span {s : set α} : s ⊆ span s := submodule.subset_span + +lemma span_le {s : set α} {I} : span s ≤ I ↔ s ⊆ I := submodule.span_le + +lemma span_mono {s t : set α} : s ⊆ t → span s ≤ span t := submodule.span_mono + +@[simp] lemma span_eq : span (I : set α) = I := submodule.span_eq _ + +@[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} : + x ∈ span (insert y s) ↔ ∃ a (z ∈ span s), x = a * y + z := submodule.mem_span_insert + +lemma mem_span_singleton' {x y : α} : + x ∈ span ({y} : set α) ↔ ∃ a, a * y = x := submodule.mem_span_singleton + +lemma mem_span_singleton {x y : α} : + x ∈ span ({y} : set α) ↔ y ∣ x := +mem_span_singleton'.trans $ exists_congr $ λ _, by rw [eq_comm, mul_comm] + +lemma span_singleton_le_span_singleton {x y : α} : + span ({x} : set α) ≤ span ({y} : set α) ↔ y ∣ x := +span_le.trans $ singleton_subset_iff.trans mem_span_singleton + +lemma span_singleton_eq_span_singleton {α : Type u} [integral_domain α] {x y : α} : + span ({x} : set α) = span ({y} : set α) ↔ associated x y := +begin + rw [←dvd_dvd_iff_associated, le_antisymm_iff, and_comm], + apply and_congr; + rw span_singleton_le_span_singleton, +end + +lemma span_eq_bot {s : set α} : span s = ⊥ ↔ ∀ x ∈ s, (x:α) = 0 := submodule.span_eq_bot + +@[simp] lemma span_singleton_eq_bot {x} : span ({x} : set α) = ⊥ ↔ x = 0 := +submodule.span_singleton_eq_bot + +@[simp] lemma span_zero : span (0 : set α) = ⊥ := by rw [←set.singleton_zero, span_singleton_eq_bot] + +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, + eq_top_iff] + +lemma span_singleton_mul_right_unit {a : α} (h2 : is_unit a) (x : α) : + span ({x * a} : set α) = span {x} := +begin + apply le_antisymm, + { rw span_singleton_le_span_singleton, use a}, + { rw span_singleton_le_span_singleton, rw is_unit.mul_right_dvd h2} +end + +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] + +/-- +The ideal generated by an arbitrary binary relation. +-/ +def of_rel (r : α → α → Prop) : ideal α := +submodule.span α { x | ∃ (a b) (h : r a b), x + b = a } + +/-- An ideal `P` of a ring `R` is prime if `P ≠ R` and `xy ∈ P → x ∈ P ∨ y ∈ P` -/ +@[class] def is_prime (I : ideal α) : Prop := +I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I + +theorem is_prime.mem_or_mem {I : ideal α} (hI : I.is_prime) : + ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I := hI.2 + +theorem is_prime.mem_or_mem_of_mul_eq_zero {I : ideal α} (hI : I.is_prime) + {x y : α} (h : x * y = 0) : x ∈ I ∨ y ∈ I := +hI.2 (h.symm ▸ I.zero_mem) + +theorem is_prime.mem_of_pow_mem {I : ideal α} (hI : I.is_prime) + {r : α} (n : ℕ) (H : r^n ∈ I) : r ∈ I := +begin + induction n with n ih, + { exact (mt (eq_top_iff_one _).2 hI.1).elim H }, + exact or.cases_on (hI.mem_or_mem H) id ih +end + +lemma not_is_prime_iff {I : ideal α} : ¬ I.is_prime ↔ I = ⊤ ∨ ∃ (x ∉ I) (y ∉ I), x * y ∈ I := +begin + simp_rw [ideal.is_prime, not_and_distrib, ne.def, not_not, not_forall, not_or_distrib], + exact or_congr iff.rfl + ⟨λ ⟨x, y, hxy, hx, hy⟩, ⟨x, hx, y, hy, hxy⟩, λ ⟨x, hx, y, hy, hxy⟩, ⟨x, y, hxy, hx, hy⟩⟩ +end + +theorem zero_ne_one_of_proper {I : ideal α} (h : I ≠ ⊤) : (0:α) ≠ 1 := +λ hz, I.ne_top_iff_one.1 h $ hz ▸ I.zero_mem + +theorem span_singleton_prime {p : α} (hp : p ≠ 0) : + is_prime (span ({p} : set α)) ↔ prime p := +by simp [is_prime, prime, span_singleton_eq_top, hp, mem_span_singleton] + +lemma bot_prime {R : Type*} [integral_domain R] : (⊥ : ideal R).is_prime := +⟨λ h, one_ne_zero (by rwa [ideal.eq_top_iff_one, submodule.mem_bot] at h), + λ x y h, mul_eq_zero.mp (by simpa only [submodule.mem_bot] using h)⟩ + +/-- An ideal is maximal if it is maximal in the collection of proper ideals. -/ +@[class] def is_maximal (I : ideal α) : Prop := is_coatom I + +theorem is_maximal_iff {I : ideal α} : I.is_maximal ↔ + (1:α) ∉ I ∧ ∀ (J : ideal α) x, I ≤ J → x ∉ I → x ∈ J → (1:α) ∈ J := +and_congr I.ne_top_iff_one $ forall_congr $ λ J, +by rw [lt_iff_le_not_le]; exact + ⟨λ H x h hx₁ hx₂, J.eq_top_iff_one.1 $ + H ⟨h, not_subset.2 ⟨_, hx₂, hx₁⟩⟩, + λ H ⟨h₁, h₂⟩, let ⟨x, xJ, xI⟩ := not_subset.1 h₂ in + J.eq_top_iff_one.2 $ H x h₁ xI xJ⟩ + +theorem is_maximal.eq_of_le {I J : ideal α} + (hI : I.is_maximal) (hJ : J ≠ ⊤) (IJ : I ≤ J) : I = J := +eq_iff_le_not_lt.2 ⟨IJ, λ h, hJ (hI.2 _ h)⟩ + +theorem is_maximal.is_prime {I : ideal α} (H : I.is_maximal) : I.is_prime := +⟨H.1, λ x y hxy, or_iff_not_imp_left.2 $ λ hx, begin + let J : ideal α := submodule.span α (insert x ↑I), + have IJ : I ≤ J, + { rw ← span_eq I, + exact (span_mono (subset_insert x ↑I)) }, + have oJ : (1 : α) ∈ J, + { have H1 := H, + cases H1 with Ht Hm, + obtain ⟨-, F⟩ := is_maximal_iff.mp H, + refine F _ x IJ hx _, + refine mem_span_insert.mpr ⟨(1 : α), 0, submodule.zero_mem (span I.carrier), _⟩, + rw [one_mul, add_zero] }, + rcases submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩, + obtain (F : y * 1 = y * (a • x + b)) := congr_arg (λ g : α, y * g) oe, + rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc], + refine submodule.add_mem I (I.mul_mem_left a hxy) (submodule.smul_mem I y _), + rwa submodule.span_eq at h, +end⟩ + +@[priority 100] -- see Note [lower instance priority] +instance is_maximal.is_prime' (I : ideal α) : ∀ [H : I.is_maximal], I.is_prime := +is_maximal.is_prime + +/-- Krull's theorem: if `I` is an ideal that is not the whole ring, then it is included in some + maximal ideal. -/ +theorem exists_le_maximal (I : ideal α) (hI : I ≠ ⊤) : + ∃ M : ideal α, M.is_maximal ∧ I ≤ M := +begin + rcases zorn.zorn_partial_order₀ { J : ideal α | J ≠ ⊤ } _ I hI with ⟨M, M0, IM, h⟩, + { refine ⟨M, ⟨M0, λ J hJ, by_contradiction $ λ J0, _⟩, IM⟩, + cases h J J0 (le_of_lt hJ), exact lt_irrefl _ hJ }, + { intros S SC cC I IS, + refine ⟨Sup S, λ H, _, λ _, le_Sup⟩, + obtain ⟨J, JS, J0⟩ : ∃ J ∈ S, (1 : α) ∈ J, + from (submodule.mem_Sup_of_directed ⟨I, IS⟩ cC.directed_on).1 ((eq_top_iff_one _).1 H), + exact SC JS ((eq_top_iff_one _).2 J0) } +end + +/-- Krull's theorem: a nontrivial ring has a maximal ideal. -/ +theorem exists_maximal [nontrivial α] : ∃ M : ideal α, M.is_maximal := +let ⟨I, ⟨hI, _⟩⟩ := exists_le_maximal (⊥ : ideal α) submodule.bot_ne_top in ⟨I, hI⟩ + +/-- If P is not properly contained in any maximal ideal then it is not properly contained + in any proper ideal -/ +lemma maximal_of_no_maximal {R : Type u} [comm_semiring R] {P : ideal R} +(hmax : ∀ m : ideal R, P < m → ¬is_maximal m) (J : ideal R) (hPJ : P < J) : J = ⊤ := +begin + by_contradiction hnonmax, + rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩, + exact hmax M (lt_of_lt_of_le hPJ hM2) hM1, +end + +theorem mem_span_pair {x y z : α} : + z ∈ span ({x, y} : set α) ↔ ∃ a b, a * x + b * y = z := +by simp [mem_span_insert, mem_span_singleton', @eq_comm _ _ z] + +lemma span_singleton_lt_span_singleton [integral_domain β] {x y : β} : + span ({x} : set β) < span ({y} : set β) ↔ dvd_not_unit y x := +by rw [lt_iff_le_not_le, span_singleton_le_span_singleton, span_singleton_le_span_singleton, + dvd_and_not_dvd_iff] + +lemma factors_decreasing [integral_domain β] (b₁ b₂ : β) (h₁ : b₁ ≠ 0) (h₂ : ¬ is_unit b₂) : + span ({b₁ * b₂} : set β) < span {b₁} := +lt_of_le_not_le (ideal.span_le.2 $ singleton_subset_iff.2 $ + ideal.mem_span_singleton.2 ⟨b₂, rfl⟩) $ λ h, +h₂ $ is_unit_of_dvd_one _ $ (mul_dvd_mul_iff_left h₁).1 $ +by rwa [mul_one, ← ideal.span_singleton_le_span_singleton] + +theorem is_maximal.exists_inv {I : ideal α} + (hI : I.is_maximal) {x} (hx : x ∉ I) : ∃ y, ∃ i ∈ I, y * x + i = 1 := +begin + cases is_maximal_iff.1 hI with H₁ H₂, + rcases mem_span_insert.1 (H₂ (span (insert x I)) x + (set.subset.trans (subset_insert _ _) subset_span) + hx (subset_span (mem_insert _ _))) with ⟨y, z, hz, hy⟩, + refine ⟨y, z, _, hy.symm⟩, + rwa ← span_eq I, +end + +end ideal + +end comm_semiring + +namespace ideal + +variables [comm_ring α] (I : ideal α) {a b : α} + +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 +--λ bi, ⟨λ h, sorry, λ h, ideal.add_mem I h bi⟩ + +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 mem_span_insert' {s : set α} {x y} : + x ∈ span (insert y s) ↔ ∃a, x + a * y ∈ span s := submodule.mem_span_insert' + +/-- The quotient `R/I` of a ring `R` by an ideal `I`. -/ +def quotient (I : ideal α) := I.quotient + +namespace quotient +variables {I} {x y : α} + +instance (I : ideal α) : has_one I.quotient := ⟨submodule.quotient.mk 1⟩ + +instance (I : ideal α) : has_mul I.quotient := +⟨λ a b, quotient.lift_on₂' a b (λ a b, submodule.quotient.mk (a * b)) $ + λ a₁ a₂ b₁ b₂ h₁ h₂, quot.sound $ begin + obtain F := I.add_mem (I.mul_mem_left a₂ h₁) (I.mul_mem_right b₁ h₂), + have : a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁, + { rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁] }, + rw ← this at F, + convert F +end⟩ + +instance (I : ideal α) : comm_ring I.quotient := +{ mul := (*), + one := 1, + mul_assoc := λ a b c, quotient.induction_on₃' a b c $ + λ a b c, congr_arg submodule.quotient.mk (mul_assoc a b c), + mul_comm := λ a b, quotient.induction_on₂' a b $ + λ a b, congr_arg submodule.quotient.mk (mul_comm a b), + one_mul := λ a, quotient.induction_on' a $ + λ a, congr_arg submodule.quotient.mk (one_mul a), + mul_one := λ a, quotient.induction_on' a $ + λ a, congr_arg submodule.quotient.mk (mul_one a), + left_distrib := λ a b c, quotient.induction_on₃' a b c $ + λ a b c, congr_arg submodule.quotient.mk (left_distrib a b c), + right_distrib := λ a b c, quotient.induction_on₃' a b c $ + λ a b c, congr_arg submodule.quotient.mk (right_distrib a b c), + ..submodule.quotient.add_comm_group I } + +/-- The ring homomorphism from a ring `R` to a quotient ring `R/I`. -/ +def mk (I : ideal α) : α →+* I.quotient := +⟨λ a, submodule.quotient.mk a, rfl, λ _ _, rfl, rfl, λ _ _, rfl⟩ + +instance : inhabited (quotient I) := ⟨mk I 37⟩ + +protected theorem eq : mk I x = mk I y ↔ x - y ∈ I := submodule.quotient.eq I + +@[simp] theorem mk_eq_mk (x : α) : (submodule.quotient.mk x : quotient I) = mk I x := rfl + +lemma eq_zero_iff_mem {I : ideal α} : mk I a = 0 ↔ a ∈ I := +by conv {to_rhs, rw ← sub_zero a }; exact quotient.eq' + +theorem zero_eq_one_iff {I : ideal α} : (0 : I.quotient) = 1 ↔ I = ⊤ := +eq_comm.trans $ eq_zero_iff_mem.trans (eq_top_iff_one _).symm + +theorem zero_ne_one_iff {I : ideal α} : (0 : I.quotient) ≠ 1 ↔ I ≠ ⊤ := +not_congr zero_eq_one_iff + +protected theorem nontrivial {I : ideal α} (hI : I ≠ ⊤) : nontrivial I.quotient := +⟨⟨0, 1, zero_ne_one_iff.2 hI⟩⟩ + +lemma mk_surjective : function.surjective (mk I) := +λ y, quotient.induction_on' y (λ x, exists.intro x rfl) + +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, + (hI.mem_or_mem (eq_zero_iff_mem.1 hab)).elim + (or.inl ∘ eq_zero_iff_mem.2) + (or.inr ∘ eq_zero_iff_mem.2), + .. quotient.comm_ring I, + .. quotient.nontrivial hI.1 } + +lemma is_integral_domain_iff_prime (I : ideal α) : is_integral_domain I.quotient ↔ I.is_prime := +⟨ λ ⟨h1, h2, h3⟩, ⟨zero_ne_one_iff.1 $ @zero_ne_one _ _ ⟨h1⟩, λ x y h, + by { simp only [←eq_zero_iff_mem, (mk I).map_mul] at ⊢ h, exact h3 _ _ h}⟩, + λ h, by exactI integral_domain.to_is_integral_domain I.quotient⟩ + +lemma exists_inv {I : ideal α} [hI : I.is_maximal] : + ∀ {a : I.quotient}, a ≠ 0 → ∃ b : I.quotient, a * b = 1 := +begin + rintro ⟨a⟩ h, + rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩, + rw [mul_comm] at abc, + refine ⟨mk _ b, quot.sound _⟩, --quot.sound hb + rw ← eq_sub_iff_add_eq' at abc, + rw [abc, ← neg_mem_iff, neg_sub] at hc, + convert hc, +end + +/-- quotient by maximal ideal is a field. def rather than instance, since users will have +computable inverses in some applications -/ +protected noncomputable def field (I : ideal α) [hI : I.is_maximal] : field I.quotient := +{ inv := λ a, if ha : a = 0 then 0 else classical.some (exists_inv ha), + mul_inv_cancel := λ a (ha : a ≠ 0), show a * dite _ _ _ = _, + by rw dif_neg ha; + exact classical.some_spec (exists_inv ha), + inv_zero := dif_pos rfl, + ..quotient.integral_domain I } + +/-- If the quotient by an ideal is a field, then the ideal is maximal. -/ +theorem maximal_of_is_field (I : ideal α) + (hqf : is_field I.quotient) : I.is_maximal := +begin + apply ideal.is_maximal_iff.2, + split, + { intro h, + rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩, + exact hxy (ideal.quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left _ h)) }, + { intros J x hIJ hxnI hxJ, + rcases hqf.mul_inv_cancel (mt ideal.quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩, + rw [← zero_add (1 : α), ← sub_self (x * y), sub_add], + refine J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (ideal.quotient.eq.1 hy)) } +end + +/-- The quotient of a ring by an ideal is a field iff the ideal is maximal. -/ +theorem maximal_ideal_iff_is_field_quotient (I : ideal α) : + I.is_maximal ↔ is_field I.quotient := +⟨λ h, @field.to_is_field I.quotient (@ideal.quotient.field _ _ I h), + λ h, maximal_of_is_field I h⟩ + +variable [comm_ring β] + +/-- Given a ring homomorphism `f : α →+* β` sending all elements of an ideal to zero, +lift it to the quotient by this ideal. -/ +def lift (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0) : + quotient S →+* β := +{ to_fun := λ x, quotient.lift_on' x f $ λ (a b) (h : _ ∈ _), + eq_of_sub_eq_zero $ by rw [← f.map_sub, H _ h], + map_one' := f.map_one, + map_zero' := f.map_zero, + map_add' := λ a₁ a₂, quotient.induction_on₂' a₁ a₂ f.map_add, + map_mul' := λ a₁ a₂, quotient.induction_on₂' a₁ a₂ f.map_mul } + +@[simp] lemma lift_mk (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0) : + lift S f H (mk S a) = f a := rfl + +end quotient + +section lattice +variables {R : Type u} [comm_ring R] + +lemma mem_sup_left {S T : ideal R} : ∀ {x : R}, x ∈ S → x ∈ S ⊔ T := +show S ≤ S ⊔ T, from le_sup_left + +lemma mem_sup_right {S T : ideal R} : ∀ {x : R}, x ∈ T → x ∈ S ⊔ T := +show T ≤ S ⊔ T, from le_sup_right + +lemma mem_supr_of_mem {ι : Type*} {S : ι → ideal R} (i : ι) : + ∀ {x : R}, x ∈ S i → x ∈ supr S := +show S i ≤ supr S, from le_supr _ _ + +lemma mem_Sup_of_mem {S : set (ideal R)} {s : ideal R} + (hs : s ∈ S) : ∀ {x : R}, x ∈ s → x ∈ Sup S := +show s ≤ Sup S, from le_Sup hs + +theorem mem_Inf {s : set (ideal R)} {x : R} : + x ∈ Inf s ↔ ∀ ⦃I⦄, I ∈ s → x ∈ I := +⟨λ hx I his, hx I ⟨I, infi_pos his⟩, λ H I ⟨J, hij⟩, hij ▸ λ S ⟨hj, hS⟩, hS ▸ H hj⟩ + +@[simp] lemma mem_inf {I J : ideal R} {x : R} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J := iff.rfl + +@[simp] lemma mem_infi {ι : Type*} {I : ι → ideal R} {x : R} : x ∈ infi I ↔ ∀ i, x ∈ I i := +submodule.mem_infi _ + +@[simp] lemma mem_bot {x : R} : x ∈ (⊥ : ideal R) ↔ x = 0 := +submodule.mem_bot _ + +end lattice + +/-- 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) + +/-- `I^n` as an ideal of `R^n`. -/ +def pi : ideal (ι → α) := +{ carrier := { x | ∀ i, x i ∈ I }, + zero_mem' := λ i, I.zero_mem, + add_mem' := λ a b ha hb i, I.add_mem (ha i) (hb i), + smul_mem' := λ a b hb i, I.mul_mem_left (a i) (hb i) } + +lemma mem_pi (x : ι → α) : x ∈ I.pi ι ↔ ∀ i, x i ∈ I := iff.rfl + +/-- `R^n/I^n` is a `R/I`-module. -/ +instance module_pi : module (I.quotient) (I.pi ι).quotient := +begin + refine { smul := λ c m, quotient.lift_on₂' c m (λ r m, submodule.quotient.mk $ r • m) _, .. }, + { intros c₁ m₁ c₂ m₂ hc hm, + change c₁ - c₂ ∈ I at hc, + change m₁ - m₂ ∈ (I.pi ι) at hm, + apply ideal.quotient.eq.2, + have : c₁ • (m₂ - m₁) ∈ I.pi ι, + { rw ideal.mem_pi, + intro i, + simp only [smul_eq_mul, pi.smul_apply, pi.sub_apply], + apply ideal.mul_mem_left, + rw ←ideal.neg_mem_iff, + simpa only [neg_sub] using hm i }, + rw [←ideal.add_mem_iff_left (I.pi ι) this, sub_eq_add_neg, add_comm, ←add_assoc, ←smul_add, + sub_add_cancel, ←sub_eq_add_neg, ←sub_smul, ideal.mem_pi], + exact λ i, I.mul_mem_right _ hc }, + all_goals { rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ <|> rintro ⟨a⟩, + simp only [(•), submodule.quotient.quot_mk_eq_mk, ideal.quotient.mk_eq_mk], + change ideal.quotient.mk _ _ = ideal.quotient.mk _ _, + congr' with i, simp [mul_assoc, mul_add, add_mul] } +end + +/-- `R^n/I^n` is isomorphic to `(R/I)^n` as an `R/I`-module. -/ +noncomputable def pi_quot_equiv : (I.pi ι).quotient ≃ₗ[I.quotient] (ι → I.quotient) := +{ to_fun := λ x, quotient.lift_on' x (λ f i, ideal.quotient.mk I (f i)) $ + λ a b hab, funext (λ i, ideal.quotient.eq.2 (hab i)), + map_add' := by { rintros ⟨_⟩ ⟨_⟩, refl }, + map_smul' := by { rintros ⟨_⟩ ⟨_⟩, refl }, + inv_fun := λ x, ideal.quotient.mk (I.pi ι) $ λ i, quotient.out' (x i), + left_inv := + begin + rintro ⟨x⟩, + exact ideal.quotient.eq.2 (λ i, ideal.quotient.eq.1 (quotient.out_eq' _)) + end, + right_inv := + begin + intro x, + ext i, + obtain ⟨r, hr⟩ := @quot.exists_rep _ _ (x i), + simp_rw ←hr, + convert quotient.out_eq' _ + end } + +/-- If `f : R^n → R^m` is an `R`-linear map and `I ⊆ R` is an ideal, then the image of `I^n` is + contained in `I^m`. -/ +lemma map_pi {ι} [fintype ι] {ι' : Type w} (x : ι → α) (hi : ∀ i, x i ∈ I) + (f : (ι → α) →ₗ[α] (ι' → α)) (i : ι') : f x i ∈ I := +begin + rw pi_eq_sum_univ x, + simp only [finset.sum_apply, smul_eq_mul, linear_map.map_sum, pi.smul_apply, linear_map.map_smul], + exact I.sum_mem (λ j hj, I.mul_mem_right _ (hi j)) +end + +end pi + +end ideal + +namespace ring + +variables {R : Type*} [comm_ring R] + +lemma not_is_field_of_subsingleton {R : Type*} [ring R] [subsingleton R] : ¬ is_field R := +λ ⟨⟨x, y, hxy⟩, _, _⟩, hxy (subsingleton.elim x y) + +lemma exists_not_is_unit_of_not_is_field [nontrivial R] (hf : ¬ is_field R) : + ∃ x ≠ (0 : R), ¬ is_unit x := +begin + have : ¬ _ := λ h, hf ⟨exists_pair_ne R, mul_comm, h⟩, + simp_rw is_unit_iff_exists_inv, + push_neg at ⊢ this, + obtain ⟨x, hx, not_unit⟩ := this, + exact ⟨x, hx, not_unit⟩ +end + +lemma not_is_field_iff_exists_ideal_bot_lt_and_lt_top [nontrivial R] : + ¬ is_field R ↔ ∃ I : ideal R, ⊥ < I ∧ I < ⊤ := +begin + split, + { intro h, + obtain ⟨x, nz, nu⟩ := exists_not_is_unit_of_not_is_field h, + use ideal.span {x}, + rw [bot_lt_iff_ne_bot, lt_top_iff_ne_top], + exact ⟨mt ideal.span_singleton_eq_bot.mp nz, mt ideal.span_singleton_eq_top.mp nu⟩ }, + { rintros ⟨I, bot_lt, lt_top⟩ hf, + obtain ⟨x, mem, ne_zero⟩ := submodule.exists_of_lt bot_lt, + rw submodule.mem_bot at ne_zero, + obtain ⟨y, hy⟩ := hf.mul_inv_cancel ne_zero, + rw [lt_top_iff_ne_top, ne.def, ideal.eq_top_iff_one, ← hy] at lt_top, + exact lt_top (I.mul_mem_right _ mem), } +end + +lemma not_is_field_iff_exists_prime [nontrivial R] : + ¬ is_field R ↔ ∃ p : ideal R, p ≠ ⊥ ∧ p.is_prime := +not_is_field_iff_exists_ideal_bot_lt_and_lt_top.trans + ⟨λ ⟨I, bot_lt, lt_top⟩, let ⟨p, hp, le_p⟩ := I.exists_le_maximal (lt_top_iff_ne_top.mp lt_top) in + ⟨p, bot_lt_iff_ne_bot.mp (lt_of_lt_of_le bot_lt le_p), hp.is_prime⟩, + λ ⟨p, ne_bot, prime⟩, ⟨p, bot_lt_iff_ne_bot.mpr ne_bot, lt_top_iff_ne_top.mpr prime.1⟩⟩ + +end ring + +namespace ideal + +/-- Maximal ideals in a non-field are nontrivial. -/ +variables {R : Type u} [comm_ring R] [nontrivial R] +lemma bot_lt_of_maximal (M : ideal R) [hm : M.is_maximal] (non_field : ¬ is_field R) : ⊥ < M := +begin + rcases (ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top.1 non_field) + with ⟨I, Ibot, Itop⟩, + split, finish, + intro mle, + apply @irrefl _ (<) _ (⊤ : ideal R), + have : M = ⊥ := eq_bot_iff.mpr mle, + rw this at *, + rwa hm.2 I Ibot at Itop, +end + +end ideal + +variables {a b : α} + +/-- The set of non-invertible elements of a monoid. -/ +def nonunits (α : Type u) [monoid α] : set α := { a | ¬is_unit a } + +@[simp] theorem mem_nonunits_iff [comm_monoid α] : a ∈ nonunits α ↔ ¬ is_unit a := iff.rfl + +theorem mul_mem_nonunits_right [comm_monoid α] : + b ∈ nonunits α → a * b ∈ nonunits α := +mt is_unit_of_mul_is_unit_right + +theorem mul_mem_nonunits_left [comm_monoid α] : + a ∈ nonunits α → a * b ∈ nonunits α := +mt is_unit_of_mul_is_unit_left + +theorem zero_mem_nonunits [semiring α] : 0 ∈ nonunits α ↔ (0:α) ≠ 1 := +not_congr is_unit_zero_iff + +@[simp] theorem one_not_mem_nonunits [monoid α] : (1:α) ∉ nonunits α := +not_not_intro is_unit_one + +theorem coe_subset_nonunits [comm_ring α] {I : ideal α} (h : I ≠ ⊤) : + (I : set α) ⊆ nonunits α := +λ x hx hu, h $ I.eq_top_of_is_unit_mem hx hu + +lemma exists_max_ideal_of_mem_nonunits [comm_ring α] (h : a ∈ nonunits α) : + ∃ I : ideal α, I.is_maximal ∧ a ∈ I := +begin + have : ideal.span ({a} : set α) ≠ ⊤, + { intro H, rw ideal.span_singleton_eq_top at H, contradiction }, + rcases ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩, + use [I, Imax], apply H, apply ideal.subset_span, exact set.mem_singleton a +end + +/-- A commutative ring is local if it has a unique maximal ideal. Note that + `local_ring` is a predicate. -/ +class local_ring (α : Type u) [comm_ring α] extends nontrivial α : Prop := +(is_local : ∀ (a : α), (is_unit a) ∨ (is_unit (1 - a))) + +namespace local_ring + +variables [comm_ring α] [local_ring α] + +lemma is_unit_or_is_unit_one_sub_self (a : α) : + (is_unit a) ∨ (is_unit (1 - a)) := +is_local a + +lemma is_unit_of_mem_nonunits_one_sub_self (a : α) (h : (1 - a) ∈ nonunits α) : + is_unit a := +or_iff_not_imp_right.1 (is_local a) h + +lemma is_unit_one_sub_self_of_mem_nonunits (a : α) (h : a ∈ nonunits α) : + is_unit (1 - a) := +or_iff_not_imp_left.1 (is_local a) h + +lemma nonunits_add {x y} (hx : x ∈ nonunits α) (hy : y ∈ nonunits α) : + x + y ∈ nonunits α := +begin + rintros ⟨u, hu⟩, + apply hy, + suffices : is_unit ((↑u⁻¹ : α) * y), + { rcases this with ⟨s, hs⟩, + use u * s, + convert congr_arg (λ z, (u : α) * z) hs, + rw ← mul_assoc, simp }, + rw show (↑u⁻¹ * y) = (1 - ↑u⁻¹ * x), + { rw eq_sub_iff_add_eq, + replace hu := congr_arg (λ z, (↑u⁻¹ : α) * z) hu.symm, + simpa [mul_add, add_comm] using hu }, + apply is_unit_one_sub_self_of_mem_nonunits, + exact mul_mem_nonunits_right hx +end + +variable (α) + +/-- The ideal of elements that are not units. -/ +def maximal_ideal : ideal α := +{ carrier := nonunits α, + zero_mem' := zero_mem_nonunits.2 $ zero_ne_one, + add_mem' := λ x y hx hy, nonunits_add hx hy, + smul_mem' := λ a x, mul_mem_nonunits_right } + +instance maximal_ideal.is_maximal : (maximal_ideal α).is_maximal := +begin + rw ideal.is_maximal_iff, + split, + { intro h, apply h, exact is_unit_one }, + { intros I x hI hx H, + erw not_not at hx, + rcases hx with ⟨u,rfl⟩, + simpa using I.mul_mem_left ↑u⁻¹ H } +end + +lemma maximal_ideal_unique : + ∃! I : ideal α, I.is_maximal := +⟨maximal_ideal α, maximal_ideal.is_maximal α, + λ I hI, hI.eq_of_le (maximal_ideal.is_maximal α).1 $ + λ x hx, hI.1 ∘ I.eq_top_of_is_unit_mem hx⟩ + +variable {α} + +lemma eq_maximal_ideal {I : ideal α} (hI : I.is_maximal) : I = maximal_ideal α := +unique_of_exists_unique (maximal_ideal_unique α) hI $ maximal_ideal.is_maximal α + +lemma le_maximal_ideal {J : ideal α} (hJ : J ≠ ⊤) : J ≤ maximal_ideal α := +begin + rcases ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩, + rwa ←eq_maximal_ideal hM1 +end + +@[simp] lemma mem_maximal_ideal (x) : + x ∈ maximal_ideal α ↔ x ∈ nonunits α := iff.rfl + +end local_ring + +lemma local_of_nonunits_ideal [comm_ring α] (hnze : (0:α) ≠ 1) + (h : ∀ x y ∈ nonunits α, x + y ∈ nonunits α) : local_ring α := +{ exists_pair_ne := ⟨0, 1, hnze⟩, + is_local := λ x, or_iff_not_imp_left.mpr $ λ hx, + begin + by_contra H, + apply h _ _ hx H, + simp [-sub_eq_add_neg, add_sub_cancel'_right] + end } + +lemma local_of_unique_max_ideal [comm_ring α] (h : ∃! I : ideal α, I.is_maximal) : + local_ring α := +local_of_nonunits_ideal +(let ⟨I, Imax, _⟩ := h in (λ (H : 0 = 1), Imax.1 $ I.eq_top_iff_one.2 $ H ▸ I.zero_mem)) +$ λ x y hx hy H, +let ⟨I, Imax, Iuniq⟩ := h in +let ⟨Ix, Ixmax, Hx⟩ := exists_max_ideal_of_mem_nonunits hx in +let ⟨Iy, Iymax, Hy⟩ := exists_max_ideal_of_mem_nonunits hy in +have xmemI : x ∈ I, from ((Iuniq Ix Ixmax) ▸ Hx), +have ymemI : y ∈ I, from ((Iuniq Iy Iymax) ▸ Hy), +Imax.1 $ I.eq_top_of_is_unit_mem (I.add_mem xmemI ymemI) H + +lemma local_of_unique_nonzero_prime (R : Type u) [comm_ring R] + (h : ∃! P : ideal R, P ≠ ⊥ ∧ ideal.is_prime P) : local_ring R := +local_of_unique_max_ideal begin + rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩, + refine ⟨P, ⟨hPnot_top, _⟩, λ M hM, hPunique _ ⟨_, ideal.is_maximal.is_prime hM⟩⟩, + { refine ideal.maximal_of_no_maximal (λ M hPM hM, ne_of_lt hPM _), + exact (hPunique _ ⟨ne_bot_of_gt hPM, ideal.is_maximal.is_prime hM⟩).symm }, + { rintro rfl, + exact hPnot_top (hM.2 P (bot_lt_iff_ne_bot.2 hPnonzero)) }, +end + +lemma local_of_surjective {A B : Type*} [comm_ring A] [local_ring A] [comm_ring B] [nontrivial B] + (f : A →+* B) (hf : function.surjective f) : + local_ring B := +{ is_local := + begin + intros b, + obtain ⟨a, rfl⟩ := hf b, + apply (local_ring.is_unit_or_is_unit_one_sub_self a).imp f.is_unit_map _, + rw [← f.map_one, ← f.map_sub], + apply f.is_unit_map, + end, + .. ‹nontrivial B› } + +/-- A local ring homomorphism is a homomorphism between local rings + such that the image of the maximal ideal of the source is contained within + the maximal ideal of the target. -/ +class is_local_ring_hom [semiring α] [semiring β] (f : α →+* β) : Prop := +(map_nonunit : ∀ a, is_unit (f a) → is_unit a) + +instance is_local_ring_hom_id (A : Type*) [semiring A] : is_local_ring_hom (ring_hom.id A) := +{ map_nonunit := λ a, id } + +@[simp] lemma is_unit_map_iff {A B : Type*} [semiring A] [semiring B] (f : A →+* B) + [is_local_ring_hom f] (a) : + is_unit (f a) ↔ is_unit a := +⟨is_local_ring_hom.map_nonunit a, f.is_unit_map⟩ + +instance is_local_ring_hom_comp {A B C : Type*} [semiring A] [semiring B] [semiring C] + (g : B →+* C) (f : A →+* B) [is_local_ring_hom g] [is_local_ring_hom f] : + is_local_ring_hom (g.comp f) := +{ map_nonunit := λ a, is_local_ring_hom.map_nonunit a ∘ is_local_ring_hom.map_nonunit (f a) } + +@[simp] lemma is_unit_of_map_unit [semiring α] [semiring β] (f : α →+* β) [is_local_ring_hom f] + (a) (h : is_unit (f a)) : is_unit a := +is_local_ring_hom.map_nonunit a h + +theorem of_irreducible_map [semiring α] [semiring β] (f : α →+* β) [h : is_local_ring_hom f] {x : α} + (hfx : irreducible (f x)) : irreducible x := +⟨λ h, hfx.1 $ is_unit.map f.to_monoid_hom h, λ p q hx, let ⟨H⟩ := h in +or.imp (H p) (H q) $ hfx.2 _ _ $ f.map_mul p q ▸ congr_arg f hx⟩ + +section +open local_ring +variables [comm_ring α] [local_ring α] [comm_ring β] [local_ring β] +variables (f : α →+* β) [is_local_ring_hom f] + +lemma map_nonunit (a) (h : a ∈ maximal_ideal α) : f a ∈ maximal_ideal β := +λ H, h $ is_unit_of_map_unit f a H + +end + +namespace local_ring +variables [comm_ring α] [local_ring α] [comm_ring β] [local_ring β] + +variable (α) +/-- The residue field of a local ring is the quotient of the ring by its maximal ideal. -/ +def residue_field := (maximal_ideal α).quotient + +noncomputable instance residue_field.field : field (residue_field α) := +ideal.quotient.field (maximal_ideal α) + +noncomputable instance : inhabited (residue_field α) := ⟨37⟩ + +/-- The quotient map from a local ring to its residue field. -/ +def residue : α →+* (residue_field α) := +ideal.quotient.mk _ + +namespace residue_field + +variables {α β} +/-- The map on residue fields induced by a local homomorphism between local rings -/ +noncomputable def map (f : α →+* β) [is_local_ring_hom f] : + residue_field α →+* residue_field β := +ideal.quotient.lift (maximal_ideal α) ((ideal.quotient.mk _).comp f) $ +λ a ha, +begin + erw ideal.quotient.eq_zero_iff_mem, + exact map_nonunit f a ha +end + +end residue_field + +end local_ring + +namespace field +variables [field α] + +@[priority 100] -- see Note [lower instance priority] +instance : local_ring α := +{ is_local := λ a, + if h : a = 0 + then or.inr (by rw [h, sub_zero]; exact is_unit_one) + else or.inl $ is_unit_of_mul_eq_one a a⁻¹ $ div_self h } + +end field diff --git a/src/ring_theory/jacobson_ideal.lean b/src/ring_theory/jacobson_ideal.lean index 8d42670b91e97..c9890fc62a14e 100644 --- a/src/ring_theory/jacobson_ideal.lean +++ b/src/ring_theory/jacobson_ideal.lean @@ -96,9 +96,11 @@ theorem mem_jacobson_iff {x : R} : x ∈ jacobson I ↔ ∀ y, ∃ z, x * y * z λ hx, mem_Inf.2 $ λ M ⟨him, hm⟩, classical.by_contradiction $ λ hxm, let ⟨y, hy⟩ := hm.exists_inv hxm, ⟨z, hz⟩ := hx (-y) in hm.1 $ (eq_top_iff_one _).2 $ sub_sub_cancel (x * -y * z + z) 1 ▸ M.sub_mem - (by rw [← one_mul z, ← mul_assoc, ← add_mul, mul_one, mul_neg_eq_neg_mul_symm, neg_add_eq_sub, ← neg_sub, - neg_mul_eq_neg_mul_symm, neg_mul_eq_mul_neg, mul_comm x y]; exact M.mul_mem_right _ hy) - (him hz)⟩ + (by {rw [← one_mul z, ← mul_assoc, ← add_mul, mul_one, mul_neg_eq_neg_mul_symm, neg_add_eq_sub, + ← neg_sub, neg_mul_eq_neg_mul_symm, neg_mul_eq_mul_neg, mul_comm x y, mul_comm _ (- z)], + rcases hy with ⟨i, hi, df⟩, + rw [← (sub_eq_iff_eq_add.mpr df.symm), sub_sub, add_comm, ← sub_sub, sub_self, zero_sub], + refine M.mul_mem_left (-z) ((neg_mem_iff _).mpr hi) }) (him hz)⟩ /-- An ideal equals its Jacobson radical iff it is the intersection of a set of maximal ideals. Allowing the set to include ⊤ is equivalent, and is included only to simplify some proofs. -/ From b79647510c73596dc6fdb780c35f75d1455fbcb9 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 27 Jan 2021 16:13:19 +0100 Subject: [PATCH 04/14] remove temporary file --- src/ring_theory/ideal/basic_n.lean | 873 ----------------------------- 1 file changed, 873 deletions(-) delete mode 100644 src/ring_theory/ideal/basic_n.lean diff --git a/src/ring_theory/ideal/basic_n.lean b/src/ring_theory/ideal/basic_n.lean deleted file mode 100644 index bdb9501669392..0000000000000 --- a/src/ring_theory/ideal/basic_n.lean +++ /dev/null @@ -1,873 +0,0 @@ -/- -Copyright (c) 2018 Kenny Lau. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kenny Lau, Chris Hughes, Mario Carneiro --/ -import algebra.associated -import linear_algebra.basic -import order.zorn -import order.atoms -/-! - -# 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. - -See `algebra.ring_quot` for quotients of non-commutative rings. --/ - -universes u v w -variables {α : Type u} {β : Type v} -open set function - -open_locale classical big_operators - -/-- An ideal in a commutative semiring `R` is an additive submonoid `s` such that -`a * b ∈ s` whenever `b ∈ s`. If `R` is a ring, then `s` is an additive subgroup. -/ -@[reducible] def ideal (R : Type u) [comm_semiring R] := submodule R R - -section comm_semiring - -namespace ideal -variables [comm_semiring α] (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 - -variables (a) -lemma mul_mem_left : b ∈ I → a * b ∈ I := I.smul_mem a -variables {a} - -variables (b) -lemma mul_mem_right (h : a ∈ I) : a * b ∈ I := mul_comm b a ▸ I.mul_mem_left b h -variables {b} -end ideal - -variables {a b : α} - --- A separate namespace definition is needed because the variables were historically in a different order -namespace ideal -variables [comm_semiring α] (I : ideal α) - -@[ext] lemma ext {I J : ideal α} (h : ∀ x, x ∈ I ↔ x ∈ J) : I = J := -submodule.ext h - -theorem eq_top_of_unit_mem - (x y : α) (hx : x ∈ I) (h : y * x = 1) : I = ⊤ := -eq_top_iff.2 $ λ z _, calc - z = z * (y * x) : by simp [h] - ... = (z * y) * x : eq.symm $ mul_assoc z y x - ... ∈ I : I.mul_mem_left _ hx - -theorem eq_top_of_is_unit_mem {x} (hx : x ∈ I) (h : is_unit x) : I = ⊤ := -let ⟨y, hy⟩ := is_unit_iff_exists_inv'.1 h in eq_top_of_unit_mem I x y hx hy - -theorem eq_top_iff_one : I = ⊤ ↔ (1:α) ∈ I := -⟨by rintro rfl; trivial, - λ h, eq_top_of_unit_mem _ _ 1 h (by simp)⟩ - -theorem ne_top_iff_one : I ≠ ⊤ ↔ (1:α) ∉ I := -not_congr I.eq_top_iff_one - -@[simp] -theorem unit_mul_mem_iff_mem {x y : α} (hy : is_unit y) : y * x ∈ I ↔ x ∈ I := -begin - refine ⟨λ h, _, λ h, I.mul_mem_left y h⟩, - obtain ⟨y', hy'⟩ := is_unit_iff_exists_inv.1 hy, - have := I.mul_mem_left y' h, - rwa [← mul_assoc, mul_comm y' y, hy', one_mul] at this, -end - -@[simp] -theorem mul_unit_mem_iff_mem {x y : α} (hy : is_unit y) : x * y ∈ I ↔ x ∈ I := -mul_comm y x ▸ unit_mul_mem_iff_mem I hy - -/-- The ideal generated by a subset of a ring -/ -def span (s : set α) : ideal α := submodule.span α s - -lemma subset_span {s : set α} : s ⊆ span s := submodule.subset_span - -lemma span_le {s : set α} {I} : span s ≤ I ↔ s ⊆ I := submodule.span_le - -lemma span_mono {s t : set α} : s ⊆ t → span s ≤ span t := submodule.span_mono - -@[simp] lemma span_eq : span (I : set α) = I := submodule.span_eq _ - -@[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} : - x ∈ span (insert y s) ↔ ∃ a (z ∈ span s), x = a * y + z := submodule.mem_span_insert - -lemma mem_span_singleton' {x y : α} : - x ∈ span ({y} : set α) ↔ ∃ a, a * y = x := submodule.mem_span_singleton - -lemma mem_span_singleton {x y : α} : - x ∈ span ({y} : set α) ↔ y ∣ x := -mem_span_singleton'.trans $ exists_congr $ λ _, by rw [eq_comm, mul_comm] - -lemma span_singleton_le_span_singleton {x y : α} : - span ({x} : set α) ≤ span ({y} : set α) ↔ y ∣ x := -span_le.trans $ singleton_subset_iff.trans mem_span_singleton - -lemma span_singleton_eq_span_singleton {α : Type u} [integral_domain α] {x y : α} : - span ({x} : set α) = span ({y} : set α) ↔ associated x y := -begin - rw [←dvd_dvd_iff_associated, le_antisymm_iff, and_comm], - apply and_congr; - rw span_singleton_le_span_singleton, -end - -lemma span_eq_bot {s : set α} : span s = ⊥ ↔ ∀ x ∈ s, (x:α) = 0 := submodule.span_eq_bot - -@[simp] lemma span_singleton_eq_bot {x} : span ({x} : set α) = ⊥ ↔ x = 0 := -submodule.span_singleton_eq_bot - -@[simp] lemma span_zero : span (0 : set α) = ⊥ := by rw [←set.singleton_zero, span_singleton_eq_bot] - -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, - eq_top_iff] - -lemma span_singleton_mul_right_unit {a : α} (h2 : is_unit a) (x : α) : - span ({x * a} : set α) = span {x} := -begin - apply le_antisymm, - { rw span_singleton_le_span_singleton, use a}, - { rw span_singleton_le_span_singleton, rw is_unit.mul_right_dvd h2} -end - -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] - -/-- -The ideal generated by an arbitrary binary relation. --/ -def of_rel (r : α → α → Prop) : ideal α := -submodule.span α { x | ∃ (a b) (h : r a b), x + b = a } - -/-- An ideal `P` of a ring `R` is prime if `P ≠ R` and `xy ∈ P → x ∈ P ∨ y ∈ P` -/ -@[class] def is_prime (I : ideal α) : Prop := -I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I - -theorem is_prime.mem_or_mem {I : ideal α} (hI : I.is_prime) : - ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I := hI.2 - -theorem is_prime.mem_or_mem_of_mul_eq_zero {I : ideal α} (hI : I.is_prime) - {x y : α} (h : x * y = 0) : x ∈ I ∨ y ∈ I := -hI.2 (h.symm ▸ I.zero_mem) - -theorem is_prime.mem_of_pow_mem {I : ideal α} (hI : I.is_prime) - {r : α} (n : ℕ) (H : r^n ∈ I) : r ∈ I := -begin - induction n with n ih, - { exact (mt (eq_top_iff_one _).2 hI.1).elim H }, - exact or.cases_on (hI.mem_or_mem H) id ih -end - -lemma not_is_prime_iff {I : ideal α} : ¬ I.is_prime ↔ I = ⊤ ∨ ∃ (x ∉ I) (y ∉ I), x * y ∈ I := -begin - simp_rw [ideal.is_prime, not_and_distrib, ne.def, not_not, not_forall, not_or_distrib], - exact or_congr iff.rfl - ⟨λ ⟨x, y, hxy, hx, hy⟩, ⟨x, hx, y, hy, hxy⟩, λ ⟨x, hx, y, hy, hxy⟩, ⟨x, y, hxy, hx, hy⟩⟩ -end - -theorem zero_ne_one_of_proper {I : ideal α} (h : I ≠ ⊤) : (0:α) ≠ 1 := -λ hz, I.ne_top_iff_one.1 h $ hz ▸ I.zero_mem - -theorem span_singleton_prime {p : α} (hp : p ≠ 0) : - is_prime (span ({p} : set α)) ↔ prime p := -by simp [is_prime, prime, span_singleton_eq_top, hp, mem_span_singleton] - -lemma bot_prime {R : Type*} [integral_domain R] : (⊥ : ideal R).is_prime := -⟨λ h, one_ne_zero (by rwa [ideal.eq_top_iff_one, submodule.mem_bot] at h), - λ x y h, mul_eq_zero.mp (by simpa only [submodule.mem_bot] using h)⟩ - -/-- An ideal is maximal if it is maximal in the collection of proper ideals. -/ -@[class] def is_maximal (I : ideal α) : Prop := is_coatom I - -theorem is_maximal_iff {I : ideal α} : I.is_maximal ↔ - (1:α) ∉ I ∧ ∀ (J : ideal α) x, I ≤ J → x ∉ I → x ∈ J → (1:α) ∈ J := -and_congr I.ne_top_iff_one $ forall_congr $ λ J, -by rw [lt_iff_le_not_le]; exact - ⟨λ H x h hx₁ hx₂, J.eq_top_iff_one.1 $ - H ⟨h, not_subset.2 ⟨_, hx₂, hx₁⟩⟩, - λ H ⟨h₁, h₂⟩, let ⟨x, xJ, xI⟩ := not_subset.1 h₂ in - J.eq_top_iff_one.2 $ H x h₁ xI xJ⟩ - -theorem is_maximal.eq_of_le {I J : ideal α} - (hI : I.is_maximal) (hJ : J ≠ ⊤) (IJ : I ≤ J) : I = J := -eq_iff_le_not_lt.2 ⟨IJ, λ h, hJ (hI.2 _ h)⟩ - -theorem is_maximal.is_prime {I : ideal α} (H : I.is_maximal) : I.is_prime := -⟨H.1, λ x y hxy, or_iff_not_imp_left.2 $ λ hx, begin - let J : ideal α := submodule.span α (insert x ↑I), - have IJ : I ≤ J, - { rw ← span_eq I, - exact (span_mono (subset_insert x ↑I)) }, - have oJ : (1 : α) ∈ J, - { have H1 := H, - cases H1 with Ht Hm, - obtain ⟨-, F⟩ := is_maximal_iff.mp H, - refine F _ x IJ hx _, - refine mem_span_insert.mpr ⟨(1 : α), 0, submodule.zero_mem (span I.carrier), _⟩, - rw [one_mul, add_zero] }, - rcases submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩, - obtain (F : y * 1 = y * (a • x + b)) := congr_arg (λ g : α, y * g) oe, - rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc], - refine submodule.add_mem I (I.mul_mem_left a hxy) (submodule.smul_mem I y _), - rwa submodule.span_eq at h, -end⟩ - -@[priority 100] -- see Note [lower instance priority] -instance is_maximal.is_prime' (I : ideal α) : ∀ [H : I.is_maximal], I.is_prime := -is_maximal.is_prime - -/-- Krull's theorem: if `I` is an ideal that is not the whole ring, then it is included in some - maximal ideal. -/ -theorem exists_le_maximal (I : ideal α) (hI : I ≠ ⊤) : - ∃ M : ideal α, M.is_maximal ∧ I ≤ M := -begin - rcases zorn.zorn_partial_order₀ { J : ideal α | J ≠ ⊤ } _ I hI with ⟨M, M0, IM, h⟩, - { refine ⟨M, ⟨M0, λ J hJ, by_contradiction $ λ J0, _⟩, IM⟩, - cases h J J0 (le_of_lt hJ), exact lt_irrefl _ hJ }, - { intros S SC cC I IS, - refine ⟨Sup S, λ H, _, λ _, le_Sup⟩, - obtain ⟨J, JS, J0⟩ : ∃ J ∈ S, (1 : α) ∈ J, - from (submodule.mem_Sup_of_directed ⟨I, IS⟩ cC.directed_on).1 ((eq_top_iff_one _).1 H), - exact SC JS ((eq_top_iff_one _).2 J0) } -end - -/-- Krull's theorem: a nontrivial ring has a maximal ideal. -/ -theorem exists_maximal [nontrivial α] : ∃ M : ideal α, M.is_maximal := -let ⟨I, ⟨hI, _⟩⟩ := exists_le_maximal (⊥ : ideal α) submodule.bot_ne_top in ⟨I, hI⟩ - -/-- If P is not properly contained in any maximal ideal then it is not properly contained - in any proper ideal -/ -lemma maximal_of_no_maximal {R : Type u} [comm_semiring R] {P : ideal R} -(hmax : ∀ m : ideal R, P < m → ¬is_maximal m) (J : ideal R) (hPJ : P < J) : J = ⊤ := -begin - by_contradiction hnonmax, - rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩, - exact hmax M (lt_of_lt_of_le hPJ hM2) hM1, -end - -theorem mem_span_pair {x y z : α} : - z ∈ span ({x, y} : set α) ↔ ∃ a b, a * x + b * y = z := -by simp [mem_span_insert, mem_span_singleton', @eq_comm _ _ z] - -lemma span_singleton_lt_span_singleton [integral_domain β] {x y : β} : - span ({x} : set β) < span ({y} : set β) ↔ dvd_not_unit y x := -by rw [lt_iff_le_not_le, span_singleton_le_span_singleton, span_singleton_le_span_singleton, - dvd_and_not_dvd_iff] - -lemma factors_decreasing [integral_domain β] (b₁ b₂ : β) (h₁ : b₁ ≠ 0) (h₂ : ¬ is_unit b₂) : - span ({b₁ * b₂} : set β) < span {b₁} := -lt_of_le_not_le (ideal.span_le.2 $ singleton_subset_iff.2 $ - ideal.mem_span_singleton.2 ⟨b₂, rfl⟩) $ λ h, -h₂ $ is_unit_of_dvd_one _ $ (mul_dvd_mul_iff_left h₁).1 $ -by rwa [mul_one, ← ideal.span_singleton_le_span_singleton] - -theorem is_maximal.exists_inv {I : ideal α} - (hI : I.is_maximal) {x} (hx : x ∉ I) : ∃ y, ∃ i ∈ I, y * x + i = 1 := -begin - cases is_maximal_iff.1 hI with H₁ H₂, - rcases mem_span_insert.1 (H₂ (span (insert x I)) x - (set.subset.trans (subset_insert _ _) subset_span) - hx (subset_span (mem_insert _ _))) with ⟨y, z, hz, hy⟩, - refine ⟨y, z, _, hy.symm⟩, - rwa ← span_eq I, -end - -end ideal - -end comm_semiring - -namespace ideal - -variables [comm_ring α] (I : ideal α) {a b : α} - -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 ---λ bi, ⟨λ h, sorry, λ h, ideal.add_mem I h bi⟩ - -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 mem_span_insert' {s : set α} {x y} : - x ∈ span (insert y s) ↔ ∃a, x + a * y ∈ span s := submodule.mem_span_insert' - -/-- The quotient `R/I` of a ring `R` by an ideal `I`. -/ -def quotient (I : ideal α) := I.quotient - -namespace quotient -variables {I} {x y : α} - -instance (I : ideal α) : has_one I.quotient := ⟨submodule.quotient.mk 1⟩ - -instance (I : ideal α) : has_mul I.quotient := -⟨λ a b, quotient.lift_on₂' a b (λ a b, submodule.quotient.mk (a * b)) $ - λ a₁ a₂ b₁ b₂ h₁ h₂, quot.sound $ begin - obtain F := I.add_mem (I.mul_mem_left a₂ h₁) (I.mul_mem_right b₁ h₂), - have : a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁, - { rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁] }, - rw ← this at F, - convert F -end⟩ - -instance (I : ideal α) : comm_ring I.quotient := -{ mul := (*), - one := 1, - mul_assoc := λ a b c, quotient.induction_on₃' a b c $ - λ a b c, congr_arg submodule.quotient.mk (mul_assoc a b c), - mul_comm := λ a b, quotient.induction_on₂' a b $ - λ a b, congr_arg submodule.quotient.mk (mul_comm a b), - one_mul := λ a, quotient.induction_on' a $ - λ a, congr_arg submodule.quotient.mk (one_mul a), - mul_one := λ a, quotient.induction_on' a $ - λ a, congr_arg submodule.quotient.mk (mul_one a), - left_distrib := λ a b c, quotient.induction_on₃' a b c $ - λ a b c, congr_arg submodule.quotient.mk (left_distrib a b c), - right_distrib := λ a b c, quotient.induction_on₃' a b c $ - λ a b c, congr_arg submodule.quotient.mk (right_distrib a b c), - ..submodule.quotient.add_comm_group I } - -/-- The ring homomorphism from a ring `R` to a quotient ring `R/I`. -/ -def mk (I : ideal α) : α →+* I.quotient := -⟨λ a, submodule.quotient.mk a, rfl, λ _ _, rfl, rfl, λ _ _, rfl⟩ - -instance : inhabited (quotient I) := ⟨mk I 37⟩ - -protected theorem eq : mk I x = mk I y ↔ x - y ∈ I := submodule.quotient.eq I - -@[simp] theorem mk_eq_mk (x : α) : (submodule.quotient.mk x : quotient I) = mk I x := rfl - -lemma eq_zero_iff_mem {I : ideal α} : mk I a = 0 ↔ a ∈ I := -by conv {to_rhs, rw ← sub_zero a }; exact quotient.eq' - -theorem zero_eq_one_iff {I : ideal α} : (0 : I.quotient) = 1 ↔ I = ⊤ := -eq_comm.trans $ eq_zero_iff_mem.trans (eq_top_iff_one _).symm - -theorem zero_ne_one_iff {I : ideal α} : (0 : I.quotient) ≠ 1 ↔ I ≠ ⊤ := -not_congr zero_eq_one_iff - -protected theorem nontrivial {I : ideal α} (hI : I ≠ ⊤) : nontrivial I.quotient := -⟨⟨0, 1, zero_ne_one_iff.2 hI⟩⟩ - -lemma mk_surjective : function.surjective (mk I) := -λ y, quotient.induction_on' y (λ x, exists.intro x rfl) - -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, - (hI.mem_or_mem (eq_zero_iff_mem.1 hab)).elim - (or.inl ∘ eq_zero_iff_mem.2) - (or.inr ∘ eq_zero_iff_mem.2), - .. quotient.comm_ring I, - .. quotient.nontrivial hI.1 } - -lemma is_integral_domain_iff_prime (I : ideal α) : is_integral_domain I.quotient ↔ I.is_prime := -⟨ λ ⟨h1, h2, h3⟩, ⟨zero_ne_one_iff.1 $ @zero_ne_one _ _ ⟨h1⟩, λ x y h, - by { simp only [←eq_zero_iff_mem, (mk I).map_mul] at ⊢ h, exact h3 _ _ h}⟩, - λ h, by exactI integral_domain.to_is_integral_domain I.quotient⟩ - -lemma exists_inv {I : ideal α} [hI : I.is_maximal] : - ∀ {a : I.quotient}, a ≠ 0 → ∃ b : I.quotient, a * b = 1 := -begin - rintro ⟨a⟩ h, - rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩, - rw [mul_comm] at abc, - refine ⟨mk _ b, quot.sound _⟩, --quot.sound hb - rw ← eq_sub_iff_add_eq' at abc, - rw [abc, ← neg_mem_iff, neg_sub] at hc, - convert hc, -end - -/-- quotient by maximal ideal is a field. def rather than instance, since users will have -computable inverses in some applications -/ -protected noncomputable def field (I : ideal α) [hI : I.is_maximal] : field I.quotient := -{ inv := λ a, if ha : a = 0 then 0 else classical.some (exists_inv ha), - mul_inv_cancel := λ a (ha : a ≠ 0), show a * dite _ _ _ = _, - by rw dif_neg ha; - exact classical.some_spec (exists_inv ha), - inv_zero := dif_pos rfl, - ..quotient.integral_domain I } - -/-- If the quotient by an ideal is a field, then the ideal is maximal. -/ -theorem maximal_of_is_field (I : ideal α) - (hqf : is_field I.quotient) : I.is_maximal := -begin - apply ideal.is_maximal_iff.2, - split, - { intro h, - rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩, - exact hxy (ideal.quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left _ h)) }, - { intros J x hIJ hxnI hxJ, - rcases hqf.mul_inv_cancel (mt ideal.quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩, - rw [← zero_add (1 : α), ← sub_self (x * y), sub_add], - refine J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (ideal.quotient.eq.1 hy)) } -end - -/-- The quotient of a ring by an ideal is a field iff the ideal is maximal. -/ -theorem maximal_ideal_iff_is_field_quotient (I : ideal α) : - I.is_maximal ↔ is_field I.quotient := -⟨λ h, @field.to_is_field I.quotient (@ideal.quotient.field _ _ I h), - λ h, maximal_of_is_field I h⟩ - -variable [comm_ring β] - -/-- Given a ring homomorphism `f : α →+* β` sending all elements of an ideal to zero, -lift it to the quotient by this ideal. -/ -def lift (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0) : - quotient S →+* β := -{ to_fun := λ x, quotient.lift_on' x f $ λ (a b) (h : _ ∈ _), - eq_of_sub_eq_zero $ by rw [← f.map_sub, H _ h], - map_one' := f.map_one, - map_zero' := f.map_zero, - map_add' := λ a₁ a₂, quotient.induction_on₂' a₁ a₂ f.map_add, - map_mul' := λ a₁ a₂, quotient.induction_on₂' a₁ a₂ f.map_mul } - -@[simp] lemma lift_mk (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0) : - lift S f H (mk S a) = f a := rfl - -end quotient - -section lattice -variables {R : Type u} [comm_ring R] - -lemma mem_sup_left {S T : ideal R} : ∀ {x : R}, x ∈ S → x ∈ S ⊔ T := -show S ≤ S ⊔ T, from le_sup_left - -lemma mem_sup_right {S T : ideal R} : ∀ {x : R}, x ∈ T → x ∈ S ⊔ T := -show T ≤ S ⊔ T, from le_sup_right - -lemma mem_supr_of_mem {ι : Type*} {S : ι → ideal R} (i : ι) : - ∀ {x : R}, x ∈ S i → x ∈ supr S := -show S i ≤ supr S, from le_supr _ _ - -lemma mem_Sup_of_mem {S : set (ideal R)} {s : ideal R} - (hs : s ∈ S) : ∀ {x : R}, x ∈ s → x ∈ Sup S := -show s ≤ Sup S, from le_Sup hs - -theorem mem_Inf {s : set (ideal R)} {x : R} : - x ∈ Inf s ↔ ∀ ⦃I⦄, I ∈ s → x ∈ I := -⟨λ hx I his, hx I ⟨I, infi_pos his⟩, λ H I ⟨J, hij⟩, hij ▸ λ S ⟨hj, hS⟩, hS ▸ H hj⟩ - -@[simp] lemma mem_inf {I J : ideal R} {x : R} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J := iff.rfl - -@[simp] lemma mem_infi {ι : Type*} {I : ι → ideal R} {x : R} : x ∈ infi I ↔ ∀ i, x ∈ I i := -submodule.mem_infi _ - -@[simp] lemma mem_bot {x : R} : x ∈ (⊥ : ideal R) ↔ x = 0 := -submodule.mem_bot _ - -end lattice - -/-- 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) - -/-- `I^n` as an ideal of `R^n`. -/ -def pi : ideal (ι → α) := -{ carrier := { x | ∀ i, x i ∈ I }, - zero_mem' := λ i, I.zero_mem, - add_mem' := λ a b ha hb i, I.add_mem (ha i) (hb i), - smul_mem' := λ a b hb i, I.mul_mem_left (a i) (hb i) } - -lemma mem_pi (x : ι → α) : x ∈ I.pi ι ↔ ∀ i, x i ∈ I := iff.rfl - -/-- `R^n/I^n` is a `R/I`-module. -/ -instance module_pi : module (I.quotient) (I.pi ι).quotient := -begin - refine { smul := λ c m, quotient.lift_on₂' c m (λ r m, submodule.quotient.mk $ r • m) _, .. }, - { intros c₁ m₁ c₂ m₂ hc hm, - change c₁ - c₂ ∈ I at hc, - change m₁ - m₂ ∈ (I.pi ι) at hm, - apply ideal.quotient.eq.2, - have : c₁ • (m₂ - m₁) ∈ I.pi ι, - { rw ideal.mem_pi, - intro i, - simp only [smul_eq_mul, pi.smul_apply, pi.sub_apply], - apply ideal.mul_mem_left, - rw ←ideal.neg_mem_iff, - simpa only [neg_sub] using hm i }, - rw [←ideal.add_mem_iff_left (I.pi ι) this, sub_eq_add_neg, add_comm, ←add_assoc, ←smul_add, - sub_add_cancel, ←sub_eq_add_neg, ←sub_smul, ideal.mem_pi], - exact λ i, I.mul_mem_right _ hc }, - all_goals { rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ <|> rintro ⟨a⟩, - simp only [(•), submodule.quotient.quot_mk_eq_mk, ideal.quotient.mk_eq_mk], - change ideal.quotient.mk _ _ = ideal.quotient.mk _ _, - congr' with i, simp [mul_assoc, mul_add, add_mul] } -end - -/-- `R^n/I^n` is isomorphic to `(R/I)^n` as an `R/I`-module. -/ -noncomputable def pi_quot_equiv : (I.pi ι).quotient ≃ₗ[I.quotient] (ι → I.quotient) := -{ to_fun := λ x, quotient.lift_on' x (λ f i, ideal.quotient.mk I (f i)) $ - λ a b hab, funext (λ i, ideal.quotient.eq.2 (hab i)), - map_add' := by { rintros ⟨_⟩ ⟨_⟩, refl }, - map_smul' := by { rintros ⟨_⟩ ⟨_⟩, refl }, - inv_fun := λ x, ideal.quotient.mk (I.pi ι) $ λ i, quotient.out' (x i), - left_inv := - begin - rintro ⟨x⟩, - exact ideal.quotient.eq.2 (λ i, ideal.quotient.eq.1 (quotient.out_eq' _)) - end, - right_inv := - begin - intro x, - ext i, - obtain ⟨r, hr⟩ := @quot.exists_rep _ _ (x i), - simp_rw ←hr, - convert quotient.out_eq' _ - end } - -/-- If `f : R^n → R^m` is an `R`-linear map and `I ⊆ R` is an ideal, then the image of `I^n` is - contained in `I^m`. -/ -lemma map_pi {ι} [fintype ι] {ι' : Type w} (x : ι → α) (hi : ∀ i, x i ∈ I) - (f : (ι → α) →ₗ[α] (ι' → α)) (i : ι') : f x i ∈ I := -begin - rw pi_eq_sum_univ x, - simp only [finset.sum_apply, smul_eq_mul, linear_map.map_sum, pi.smul_apply, linear_map.map_smul], - exact I.sum_mem (λ j hj, I.mul_mem_right _ (hi j)) -end - -end pi - -end ideal - -namespace ring - -variables {R : Type*} [comm_ring R] - -lemma not_is_field_of_subsingleton {R : Type*} [ring R] [subsingleton R] : ¬ is_field R := -λ ⟨⟨x, y, hxy⟩, _, _⟩, hxy (subsingleton.elim x y) - -lemma exists_not_is_unit_of_not_is_field [nontrivial R] (hf : ¬ is_field R) : - ∃ x ≠ (0 : R), ¬ is_unit x := -begin - have : ¬ _ := λ h, hf ⟨exists_pair_ne R, mul_comm, h⟩, - simp_rw is_unit_iff_exists_inv, - push_neg at ⊢ this, - obtain ⟨x, hx, not_unit⟩ := this, - exact ⟨x, hx, not_unit⟩ -end - -lemma not_is_field_iff_exists_ideal_bot_lt_and_lt_top [nontrivial R] : - ¬ is_field R ↔ ∃ I : ideal R, ⊥ < I ∧ I < ⊤ := -begin - split, - { intro h, - obtain ⟨x, nz, nu⟩ := exists_not_is_unit_of_not_is_field h, - use ideal.span {x}, - rw [bot_lt_iff_ne_bot, lt_top_iff_ne_top], - exact ⟨mt ideal.span_singleton_eq_bot.mp nz, mt ideal.span_singleton_eq_top.mp nu⟩ }, - { rintros ⟨I, bot_lt, lt_top⟩ hf, - obtain ⟨x, mem, ne_zero⟩ := submodule.exists_of_lt bot_lt, - rw submodule.mem_bot at ne_zero, - obtain ⟨y, hy⟩ := hf.mul_inv_cancel ne_zero, - rw [lt_top_iff_ne_top, ne.def, ideal.eq_top_iff_one, ← hy] at lt_top, - exact lt_top (I.mul_mem_right _ mem), } -end - -lemma not_is_field_iff_exists_prime [nontrivial R] : - ¬ is_field R ↔ ∃ p : ideal R, p ≠ ⊥ ∧ p.is_prime := -not_is_field_iff_exists_ideal_bot_lt_and_lt_top.trans - ⟨λ ⟨I, bot_lt, lt_top⟩, let ⟨p, hp, le_p⟩ := I.exists_le_maximal (lt_top_iff_ne_top.mp lt_top) in - ⟨p, bot_lt_iff_ne_bot.mp (lt_of_lt_of_le bot_lt le_p), hp.is_prime⟩, - λ ⟨p, ne_bot, prime⟩, ⟨p, bot_lt_iff_ne_bot.mpr ne_bot, lt_top_iff_ne_top.mpr prime.1⟩⟩ - -end ring - -namespace ideal - -/-- Maximal ideals in a non-field are nontrivial. -/ -variables {R : Type u} [comm_ring R] [nontrivial R] -lemma bot_lt_of_maximal (M : ideal R) [hm : M.is_maximal] (non_field : ¬ is_field R) : ⊥ < M := -begin - rcases (ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top.1 non_field) - with ⟨I, Ibot, Itop⟩, - split, finish, - intro mle, - apply @irrefl _ (<) _ (⊤ : ideal R), - have : M = ⊥ := eq_bot_iff.mpr mle, - rw this at *, - rwa hm.2 I Ibot at Itop, -end - -end ideal - -variables {a b : α} - -/-- The set of non-invertible elements of a monoid. -/ -def nonunits (α : Type u) [monoid α] : set α := { a | ¬is_unit a } - -@[simp] theorem mem_nonunits_iff [comm_monoid α] : a ∈ nonunits α ↔ ¬ is_unit a := iff.rfl - -theorem mul_mem_nonunits_right [comm_monoid α] : - b ∈ nonunits α → a * b ∈ nonunits α := -mt is_unit_of_mul_is_unit_right - -theorem mul_mem_nonunits_left [comm_monoid α] : - a ∈ nonunits α → a * b ∈ nonunits α := -mt is_unit_of_mul_is_unit_left - -theorem zero_mem_nonunits [semiring α] : 0 ∈ nonunits α ↔ (0:α) ≠ 1 := -not_congr is_unit_zero_iff - -@[simp] theorem one_not_mem_nonunits [monoid α] : (1:α) ∉ nonunits α := -not_not_intro is_unit_one - -theorem coe_subset_nonunits [comm_ring α] {I : ideal α} (h : I ≠ ⊤) : - (I : set α) ⊆ nonunits α := -λ x hx hu, h $ I.eq_top_of_is_unit_mem hx hu - -lemma exists_max_ideal_of_mem_nonunits [comm_ring α] (h : a ∈ nonunits α) : - ∃ I : ideal α, I.is_maximal ∧ a ∈ I := -begin - have : ideal.span ({a} : set α) ≠ ⊤, - { intro H, rw ideal.span_singleton_eq_top at H, contradiction }, - rcases ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩, - use [I, Imax], apply H, apply ideal.subset_span, exact set.mem_singleton a -end - -/-- A commutative ring is local if it has a unique maximal ideal. Note that - `local_ring` is a predicate. -/ -class local_ring (α : Type u) [comm_ring α] extends nontrivial α : Prop := -(is_local : ∀ (a : α), (is_unit a) ∨ (is_unit (1 - a))) - -namespace local_ring - -variables [comm_ring α] [local_ring α] - -lemma is_unit_or_is_unit_one_sub_self (a : α) : - (is_unit a) ∨ (is_unit (1 - a)) := -is_local a - -lemma is_unit_of_mem_nonunits_one_sub_self (a : α) (h : (1 - a) ∈ nonunits α) : - is_unit a := -or_iff_not_imp_right.1 (is_local a) h - -lemma is_unit_one_sub_self_of_mem_nonunits (a : α) (h : a ∈ nonunits α) : - is_unit (1 - a) := -or_iff_not_imp_left.1 (is_local a) h - -lemma nonunits_add {x y} (hx : x ∈ nonunits α) (hy : y ∈ nonunits α) : - x + y ∈ nonunits α := -begin - rintros ⟨u, hu⟩, - apply hy, - suffices : is_unit ((↑u⁻¹ : α) * y), - { rcases this with ⟨s, hs⟩, - use u * s, - convert congr_arg (λ z, (u : α) * z) hs, - rw ← mul_assoc, simp }, - rw show (↑u⁻¹ * y) = (1 - ↑u⁻¹ * x), - { rw eq_sub_iff_add_eq, - replace hu := congr_arg (λ z, (↑u⁻¹ : α) * z) hu.symm, - simpa [mul_add, add_comm] using hu }, - apply is_unit_one_sub_self_of_mem_nonunits, - exact mul_mem_nonunits_right hx -end - -variable (α) - -/-- The ideal of elements that are not units. -/ -def maximal_ideal : ideal α := -{ carrier := nonunits α, - zero_mem' := zero_mem_nonunits.2 $ zero_ne_one, - add_mem' := λ x y hx hy, nonunits_add hx hy, - smul_mem' := λ a x, mul_mem_nonunits_right } - -instance maximal_ideal.is_maximal : (maximal_ideal α).is_maximal := -begin - rw ideal.is_maximal_iff, - split, - { intro h, apply h, exact is_unit_one }, - { intros I x hI hx H, - erw not_not at hx, - rcases hx with ⟨u,rfl⟩, - simpa using I.mul_mem_left ↑u⁻¹ H } -end - -lemma maximal_ideal_unique : - ∃! I : ideal α, I.is_maximal := -⟨maximal_ideal α, maximal_ideal.is_maximal α, - λ I hI, hI.eq_of_le (maximal_ideal.is_maximal α).1 $ - λ x hx, hI.1 ∘ I.eq_top_of_is_unit_mem hx⟩ - -variable {α} - -lemma eq_maximal_ideal {I : ideal α} (hI : I.is_maximal) : I = maximal_ideal α := -unique_of_exists_unique (maximal_ideal_unique α) hI $ maximal_ideal.is_maximal α - -lemma le_maximal_ideal {J : ideal α} (hJ : J ≠ ⊤) : J ≤ maximal_ideal α := -begin - rcases ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩, - rwa ←eq_maximal_ideal hM1 -end - -@[simp] lemma mem_maximal_ideal (x) : - x ∈ maximal_ideal α ↔ x ∈ nonunits α := iff.rfl - -end local_ring - -lemma local_of_nonunits_ideal [comm_ring α] (hnze : (0:α) ≠ 1) - (h : ∀ x y ∈ nonunits α, x + y ∈ nonunits α) : local_ring α := -{ exists_pair_ne := ⟨0, 1, hnze⟩, - is_local := λ x, or_iff_not_imp_left.mpr $ λ hx, - begin - by_contra H, - apply h _ _ hx H, - simp [-sub_eq_add_neg, add_sub_cancel'_right] - end } - -lemma local_of_unique_max_ideal [comm_ring α] (h : ∃! I : ideal α, I.is_maximal) : - local_ring α := -local_of_nonunits_ideal -(let ⟨I, Imax, _⟩ := h in (λ (H : 0 = 1), Imax.1 $ I.eq_top_iff_one.2 $ H ▸ I.zero_mem)) -$ λ x y hx hy H, -let ⟨I, Imax, Iuniq⟩ := h in -let ⟨Ix, Ixmax, Hx⟩ := exists_max_ideal_of_mem_nonunits hx in -let ⟨Iy, Iymax, Hy⟩ := exists_max_ideal_of_mem_nonunits hy in -have xmemI : x ∈ I, from ((Iuniq Ix Ixmax) ▸ Hx), -have ymemI : y ∈ I, from ((Iuniq Iy Iymax) ▸ Hy), -Imax.1 $ I.eq_top_of_is_unit_mem (I.add_mem xmemI ymemI) H - -lemma local_of_unique_nonzero_prime (R : Type u) [comm_ring R] - (h : ∃! P : ideal R, P ≠ ⊥ ∧ ideal.is_prime P) : local_ring R := -local_of_unique_max_ideal begin - rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩, - refine ⟨P, ⟨hPnot_top, _⟩, λ M hM, hPunique _ ⟨_, ideal.is_maximal.is_prime hM⟩⟩, - { refine ideal.maximal_of_no_maximal (λ M hPM hM, ne_of_lt hPM _), - exact (hPunique _ ⟨ne_bot_of_gt hPM, ideal.is_maximal.is_prime hM⟩).symm }, - { rintro rfl, - exact hPnot_top (hM.2 P (bot_lt_iff_ne_bot.2 hPnonzero)) }, -end - -lemma local_of_surjective {A B : Type*} [comm_ring A] [local_ring A] [comm_ring B] [nontrivial B] - (f : A →+* B) (hf : function.surjective f) : - local_ring B := -{ is_local := - begin - intros b, - obtain ⟨a, rfl⟩ := hf b, - apply (local_ring.is_unit_or_is_unit_one_sub_self a).imp f.is_unit_map _, - rw [← f.map_one, ← f.map_sub], - apply f.is_unit_map, - end, - .. ‹nontrivial B› } - -/-- A local ring homomorphism is a homomorphism between local rings - such that the image of the maximal ideal of the source is contained within - the maximal ideal of the target. -/ -class is_local_ring_hom [semiring α] [semiring β] (f : α →+* β) : Prop := -(map_nonunit : ∀ a, is_unit (f a) → is_unit a) - -instance is_local_ring_hom_id (A : Type*) [semiring A] : is_local_ring_hom (ring_hom.id A) := -{ map_nonunit := λ a, id } - -@[simp] lemma is_unit_map_iff {A B : Type*} [semiring A] [semiring B] (f : A →+* B) - [is_local_ring_hom f] (a) : - is_unit (f a) ↔ is_unit a := -⟨is_local_ring_hom.map_nonunit a, f.is_unit_map⟩ - -instance is_local_ring_hom_comp {A B C : Type*} [semiring A] [semiring B] [semiring C] - (g : B →+* C) (f : A →+* B) [is_local_ring_hom g] [is_local_ring_hom f] : - is_local_ring_hom (g.comp f) := -{ map_nonunit := λ a, is_local_ring_hom.map_nonunit a ∘ is_local_ring_hom.map_nonunit (f a) } - -@[simp] lemma is_unit_of_map_unit [semiring α] [semiring β] (f : α →+* β) [is_local_ring_hom f] - (a) (h : is_unit (f a)) : is_unit a := -is_local_ring_hom.map_nonunit a h - -theorem of_irreducible_map [semiring α] [semiring β] (f : α →+* β) [h : is_local_ring_hom f] {x : α} - (hfx : irreducible (f x)) : irreducible x := -⟨λ h, hfx.1 $ is_unit.map f.to_monoid_hom h, λ p q hx, let ⟨H⟩ := h in -or.imp (H p) (H q) $ hfx.2 _ _ $ f.map_mul p q ▸ congr_arg f hx⟩ - -section -open local_ring -variables [comm_ring α] [local_ring α] [comm_ring β] [local_ring β] -variables (f : α →+* β) [is_local_ring_hom f] - -lemma map_nonunit (a) (h : a ∈ maximal_ideal α) : f a ∈ maximal_ideal β := -λ H, h $ is_unit_of_map_unit f a H - -end - -namespace local_ring -variables [comm_ring α] [local_ring α] [comm_ring β] [local_ring β] - -variable (α) -/-- The residue field of a local ring is the quotient of the ring by its maximal ideal. -/ -def residue_field := (maximal_ideal α).quotient - -noncomputable instance residue_field.field : field (residue_field α) := -ideal.quotient.field (maximal_ideal α) - -noncomputable instance : inhabited (residue_field α) := ⟨37⟩ - -/-- The quotient map from a local ring to its residue field. -/ -def residue : α →+* (residue_field α) := -ideal.quotient.mk _ - -namespace residue_field - -variables {α β} -/-- The map on residue fields induced by a local homomorphism between local rings -/ -noncomputable def map (f : α →+* β) [is_local_ring_hom f] : - residue_field α →+* residue_field β := -ideal.quotient.lift (maximal_ideal α) ((ideal.quotient.mk _).comp f) $ -λ a ha, -begin - erw ideal.quotient.eq_zero_iff_mem, - exact map_nonunit f a ha -end - -end residue_field - -end local_ring - -namespace field -variables [field α] - -@[priority 100] -- see Note [lower instance priority] -instance : local_ring α := -{ is_local := λ a, - if h : a = 0 - then or.inr (by rw [h, sub_zero]; exact is_unit_one) - else or.inl $ is_unit_of_mul_eq_one a a⁻¹ $ div_self h } - -end field From a43235620f9aee497ad12f5ef57261bfe9317d80 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 29 Jan 2021 06:32:09 +0100 Subject: [PATCH 05/14] fix ring_theory/jacobson --- src/ring_theory/jacobson.lean | 191 ++++++++++++++++++++++++---------- 1 file changed, 134 insertions(+), 57 deletions(-) diff --git a/src/ring_theory/jacobson.lean b/src/ring_theory/jacobson.lean index 4f66c6bce9716..29d0adc54b8af 100644 --- a/src/ring_theory/jacobson.lean +++ b/src/ring_theory/jacobson.lean @@ -71,6 +71,95 @@ begin rw [quotient_map_mk, coe_map_ring_hom, map_C], end +/- +lemma quotient.mk_bot_injective_of {R : Type*} [comm_ring R] : + function.injective (quotient.mk (⊥ : ideal R)) := +begin + rw is_add_group_hom.injective_iff, + intros r hr, + admit, +end +-/ + + +lemma semimodule.carrier_bot {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] : + (⊥ : submodule R M).carrier = {0} := rfl + +lemma semimodule.eq_bot_iff {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] + (P : submodule R M) : + P = ⊥ ↔ P.carrier = {0} := +begin + rw ← @semimodule.carrier_bot R, + refine ⟨λ h, congr_arg submodule.carrier h, λ h, submodule.ext (λ x, ⟨λ xP, _, λ xb, _⟩)⟩, + { rcases P with ⟨P.carrier, P0, P_add, P_smul⟩, + dsimp at h, + simp_rw [h] at xP, + exact xP }, + { rw [(submodule.mem_bot R).mp xb], + exact submodule.zero_mem _ } +end + +lemma submodule.eq_bot_iff {R : Type*} [semiring R] (P : submodule R R) : + P = ⊥ ↔ P.carrier = {0} := +semimodule.eq_bot_iff P + +--lemma ideal.carrier_bot {R : Type*} [comm_semiring R] : (⊥ : ideal R).carrier = {0} := rfl + +--lemma ideal.eq_bot_iff {R : Type*} [comm_semiring R] (P : ideal R) : +-- P = ⊥ ↔ P.carrier = {0} := +--semimodule.eq_bot_iff P + +lemma semimodule.ne_bot_iff {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] + (P : submodule R M) : + P ≠ ⊥ ↔ P.carrier ≠ {0} := +not_congr (semimodule.eq_bot_iff P) + +lemma exists_mem_of_not_subset {R : Type*} {s t : set R} (st : ¬ s ⊆ t) : + ∃ a ∈ s, a ∉ t := +set.not_subset.mp st + +lemma exists_mem_of_ne_bot {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] + {P : submodule R M} (Pb : P ≠ ⊥) : + ∃ (m : M), m ∈ P ∧ m ≠ 0 := +begin + have : ¬ P.carrier ⊆ {0}, + { rw semimodule.ne_bot_iff at Pb, + refine λ h, Pb (set.ext (λ x, ⟨λ xP, h xP, _⟩)), + rw set.mem_singleton_iff, + rintros rfl, + exact submodule.zero_mem P }, + obtain ⟨r, rP, r0⟩ := set.not_subset.mp this, + refine ⟨r, rP, _⟩, + rintro rfl, + exact r0 (set.mem_singleton 0), +end + +lemma ideal.exists_mem_of_ne_bot {R : Type*} [comm_semiring R] {P : ideal R} (Pb : P ≠ ⊥) : + ∃ (r : R), r ∈ P ∧ r ≠ 0 := +exists_mem_of_ne_bot Pb + +lemma ideal_v.exists_mem_of_ne_bot {R : Type*} [comm_ring R] {P : ideal R} (Pb : P ≠ ⊥) : + ∃ (r : R), r ∈ P ∧ r ≠ 0 := +exists_mem_of_ne_bot Pb + +lemma submodule.exists_mem_of_ne_bot {R : Type*} [semiring R] {P : submodule R R} (Pb : P ≠ ⊥) : + ∃ (r : R), r ∈ P ∧ r ≠ 0 := +exists_mem_of_ne_bot Pb + +lemma exists_nonzero {R : Type*} [comm_ring R] {P : ideal (polynomial R)} + (Pb : P ≠ ⊥) (hP : ∀ (x : R), C x ∈ P → x = 0) : + ∃ p : polynomial R, p ∈ P ∧ (polynomial.map (quotient.mk (P.comap C)) p) ≠ 0 := +begin + obtain ⟨p, hp, p0⟩ := exists_mem_of_ne_bot Pb, + refine ⟨p, hp, λ pp0, p0 _⟩, + refine (is_add_group_hom.injective_iff (polynomial.map (quotient.mk (P.comap C)))).mp _ p pp0, + refine map_injective _ ((quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr _), + rw [mk_ker, semimodule.eq_bot_iff], + refine set.ext (λ (r : R), ⟨λ h, hP _ h, λ h, _⟩), + rw [set.mem_singleton_iff.mp h], + exact (P.comap (C : R →+* polynomial R)).zero_mem', +end + end technical_lemmas section is_jacobson @@ -380,23 +469,17 @@ private lemma is_jacobson_polynomial_of_domain (R : Type*) [integral_domain R] [ (P : ideal (polynomial R)) [is_prime P] (hP : ∀ (x : R), C x ∈ P → x = 0) : P.jacobson = P := begin - by_cases hP : (P = ⊥), - { exact hP.symm ▸ jacobson_bot_polynomial_of_jacobson_bot (hR ⊥ radical_bot_of_integral_domain) }, - { refine jacobson_eq_iff_jacobson_quotient_eq_bot.mpr _, - let P' : ideal R := P.comap C, - have hP'_inj : function.injective (quotient.mk P') := (quotient.mk P').injective_iff.2 - (λ x hx, by rwa [quotient.eq_zero_iff_mem, (by rwa eq_bot_iff : P' = ⊥)] at hx), - haveI : P'.is_prime := comap_is_prime C P, - obtain ⟨pX, hpX, hp0⟩ := P.exists_mem_ne_zero_of_ne_bot hP, - have hp0 : (pX.map (quotient.mk P')).leading_coeff ≠ 0 := - λ hp0', hp0 $ map_injective (quotient.mk P') ((quotient.mk P').injective_iff.2 - (λ x hx, by rwa [quotient.eq_zero_iff_mem, (by rwa eq_bot_iff : P' = ⊥)] at hx)) - (by simpa using hp0'), - let φ : P'.quotient →+* P.quotient := quotient_map P C le_rfl, - let M : submonoid P'.quotient := submonoid.powers (pX.map (quotient.mk P')).leading_coeff, - refine jacobson_bot_of_integral_localization φ quotient_map_injective - (pX.map (quotient.mk P')).leading_coeff hp0 (localization.of M) (localization.of (M.map ↑φ)) - (is_integral_localization_map_polynomial_quotient P pX hpX _ _) }, + by_cases Pb : (P = ⊥), + { exact Pb.symm ▸ jacobson_bot_polynomial_of_jacobson_bot (hR ⊥ radical_bot_of_integral_domain) }, + { obtain ⟨p, pP, p0⟩ : ∃ p, p ∈ P ∧ polynomial.map (quotient.mk (P.comap C)) p ≠ 0 := + exists_nonzero Pb hP, + refine jacobson_eq_iff_jacobson_quotient_eq_bot.mpr _, + haveI : (P.comap (C : R →+* polynomial R)).is_prime := comap_is_prime C P, + refine jacobson_bot_of_integral_localization (quotient_map P C le_rfl) quotient_map_injective + _ _ (localization.of (submonoid.powers (p.map (quotient.mk (P.comap C))).leading_coeff)) + (localization.of _) (is_integral_localization_map_polynomial_quotient P _ _ _ _), + rwa [ne.def, leading_coeff_eq_zero], + exact pP, }, end lemma is_jacobson_polynomial_of_is_jacobson (hR : is_jacobson R) : @@ -450,40 +533,34 @@ lemma is_maximal_comap_C_of_is_maximal (hP' : ∀ (x : R), C x ∈ P → x = 0) is_maximal (comap C P : ideal R) := begin haveI hp'_prime : (P.comap C : ideal R).is_prime := comap_is_prime C P, - obtain ⟨pX, hpX, hp0⟩ := P.exists_mem_ne_zero_of_ne_bot - (ne_of_lt (bot_lt_of_maximal P polynomial_not_is_field)).symm, + obtain ⟨pX, hpX, hp0⟩ := + exists_mem_of_ne_bot (ne_of_lt (bot_lt_of_maximal P polynomial_not_is_field)).symm, + let φ : (P.comap C : ideal R).quotient →+* P.quotient := quotient_map P C le_rfl, + let M : submonoid (P.comap C : ideal R).quotient := + submonoid.powers (pX.map (quotient.mk (P.comap C : ideal R))).leading_coeff, + rw ← bot_quotient_is_maximal_iff at hP ⊢, have hp0 : (pX.map (quotient.mk (P.comap C : ideal R))).leading_coeff ≠ 0 := λ hp0', hp0 $ map_injective (quotient.mk (P.comap C : ideal R)) ((quotient.mk (P.comap C : ideal R)).injective_iff.2 (λ x hx, by rwa [quotient.eq_zero_iff_mem, (by rwa eq_bot_iff : (P.comap C : ideal R) = ⊥)] at hx)) (by simpa only [leading_coeff_eq_zero, map_zero] using hp0'), - let φ : (P.comap C : ideal R).quotient →+* P.quotient := quotient_map P C le_rfl, - let M : submonoid (P.comap C : ideal R).quotient := - submonoid.powers (pX.map (quotient.mk (P.comap C : ideal R))).leading_coeff, - let M' : submonoid P.quotient := M.map φ, let ϕ : localization_map M (localization M) := localization.of M, - let ϕ' : localization_map (M.map ↑φ) (localization (M.map ↑φ)) := localization.of (M.map ↑φ), - let φ' : (localization M) →+* (localization (M.map ↑φ)) := - (ϕ.map (M.mem_map_of_mem (φ : (P.comap C : ideal R).quotient →* P.quotient)) ϕ'), - have hcomm: φ'.comp ϕ.to_map = ϕ'.to_map.comp φ := ϕ.map_comp _, - have hφ : function.injective φ := quotient_map_injective, - have hM : (0 : ((P.comap C : ideal R)).quotient) ∉ M := - λ hM, hp0 (let ⟨n, hn⟩ := hM in pow_eq_zero hn), - have hM' : (0 : P.quotient) ∉ M' := - λ hM', hM (let ⟨z, hz⟩ := hM' in (hφ (trans hz.2 φ.map_zero.symm)) ▸ hz.1), - letI : integral_domain (localization M') := - localization_map.integral_domain_localization (le_non_zero_divisors_of_domain hM'), - rw ← bot_quotient_is_maximal_iff at hP ⊢, + have hM : (0 : ((P.comap C : ideal R)).quotient) ∉ M := λ ⟨n, hn⟩, hp0 (pow_eq_zero hn), suffices : (⊥ : ideal (localization M)).is_maximal, { rw ← ϕ.comap_map_of_is_prime_disjoint ⊥ bot_prime (λ x hx, hM (hx.2 ▸ hx.1)), refine ((is_maximal_iff_is_maximal_disjoint ϕ _).mp _).1, rwa map_bot }, + let M' : submonoid P.quotient := M.map φ, + have hM' : (0 : P.quotient) ∉ M' := + λ ⟨z, hz⟩, hM (quotient_map_injective (trans hz.2 φ.map_zero.symm) ▸ hz.1), + letI : integral_domain (localization M') := + localization_map.integral_domain_localization (le_non_zero_divisors_of_domain hM'), + let ϕ' : localization_map (M.map ↑φ) (localization (M.map ↑φ)) := localization.of (M.map ↑φ), suffices : (⊥ : ideal (localization M')).is_maximal, - { rw le_antisymm bot_le (comap_bot_le_of_injective φ' (map_injective_of_injective φ hφ M ϕ ϕ' - (le_non_zero_divisors_of_domain hM'))), - refine is_maximal_comap_of_is_integral_of_is_maximal' φ' _ ⊥ this, - exact @is_integral_localization_map_polynomial_quotient - R _ (localization M) _ _ _ P _ pX hpX ϕ ϕ' }, + { rw le_antisymm bot_le (comap_bot_le_of_injective _ (map_injective_of_injective _ + quotient_map_injective M ϕ ϕ' (le_non_zero_divisors_of_domain hM'))), + refine is_maximal_comap_of_is_integral_of_is_maximal' _ _ ⊥ this, + exact is_integral_localization_map_polynomial_quotient P pX hpX ϕ ϕ' }, rw (map_bot.symm : (⊥ : ideal (localization M')) = map ϕ'.to_map ⊥), refine map.is_maximal ϕ'.to_map (localization_map_bijective_of_field hM' _ ϕ') hP, rwa [← quotient.maximal_ideal_iff_is_field_quotient, ← bot_quotient_is_maximal_iff], @@ -494,27 +571,23 @@ private lemma quotient_mk_comp_C_is_integral_of_jacobson' (hR : is_jacobson R) (hP' : ∀ (x : R), C x ∈ P → x = 0) : ((quotient.mk P).comp C : R →+* P.quotient).is_integral := begin + refine (is_integral_quotient_map_iff _).mp _, let P' : ideal R := P.comap C, - obtain ⟨pX, hpX, hp0⟩ := P.exists_mem_ne_zero_of_ne_bot - (ne_of_lt (bot_lt_of_maximal P polynomial_not_is_field)).symm, + obtain ⟨pX, hpX, hp0⟩ := + exists_nonzero (ne_of_lt (bot_lt_of_maximal P polynomial_not_is_field)).symm hP', let M : submonoid P'.quotient := submonoid.powers (pX.map (quotient.mk P')).leading_coeff, let φ : P'.quotient →+* P.quotient := quotient_map P C le_rfl, let ϕ' : localization_map (M.map ↑φ) (localization (M.map ↑φ)) := localization.of (M.map ↑φ), - let ϕ : localization_map M (localization M) := localization.of M, haveI hp'_prime : P'.is_prime := comap_is_prime C P, - have hp0 : (pX.map (quotient.mk P')).leading_coeff ≠ 0 := - λ hp0', hp0 $ map_injective (quotient.mk P') ((quotient.mk P').injective_iff.2 - (λ x hx, by rwa [quotient.eq_zero_iff_mem, (by rwa eq_bot_iff : P' = ⊥)] at hx)) - (by simpa only [leading_coeff_eq_zero, map_zero] using hp0'), - refine (is_integral_quotient_map_iff _).mp _, - have hM : (0 : P'.quotient) ∉ M := λ hM, hp0 (let ⟨n, hn⟩ := hM in (pow_eq_zero hn)), + have hM : (0 : P'.quotient) ∉ M := λ ⟨n, hn⟩, hp0 $ leading_coeff_eq_zero.mp (pow_eq_zero hn), refine ((quotient_map P C le_rfl).is_integral_tower_bot_of_is_integral (localization.of (M.map ↑(quotient_map P C le_rfl))).to_map _ _), - { refine ϕ'.injective (le_non_zero_divisors_of_domain (λ hM', _)), - exact hM (let ⟨z, hz⟩ := hM' in (quotient_map_injective (trans hz.2 φ.map_zero.symm)) ▸ hz.1) }, - { rw ← (ϕ.map_comp _), + { refine ϕ'.injective (le_non_zero_divisors_of_domain (λ hM', hM _)), + exact (let ⟨z, hz⟩ := hM' in (quotient_map_injective (trans hz.2 φ.map_zero.symm)) ▸ hz.1) }, + { let ϕ : localization_map M (localization M) := localization.of M, + rw ← (ϕ.map_comp _), refine ring_hom.is_integral_trans ϕ.to_map - ((ϕ.map (M.mem_map_of_mem (φ : P'.quotient →* P.quotient)) ϕ')) _ _, + (ϕ.map (M.mem_map_of_mem (φ : P'.quotient →* P.quotient)) ϕ') _ _, { exact ϕ.to_map.is_integral_of_surjective (localization_map_bijective_of_field hM ((quotient.maximal_ideal_iff_is_field_quotient _).mp (is_maximal_comap_C_of_is_maximal P hP')) _).2 }, @@ -562,10 +635,12 @@ lemma comp_C_integral_of_surjective_of_jacobson begin haveI : (f.ker).is_maximal := @comap_is_maximal_of_surjective _ _ _ _ f ⊥ hf bot_is_maximal, let g : f.ker.quotient →+* S := ideal.quotient.lift f.ker f (λ _ h, h), - have hfg : (g.comp (quotient.mk f.ker)) = f := quotient.lift_comp_mk f.ker f _, + have hfg : (g.comp (quotient.mk f.ker)) = f := ring_hom_ext' rfl rfl, rw [← hfg, ring_hom.comp_assoc], refine ring_hom.is_integral_trans _ g (quotient_mk_comp_C_is_integral_of_jacobson f.ker) - (g.is_integral_of_surjective (quotient.lift_surjective f.ker f _ hf)), + (g.is_integral_of_surjective _), --(quotient.lift_surjective f.ker f _ hf)), + rw [← hfg] at hf, + exact function.surjective.of_comp hf, end end integral_domain @@ -634,10 +709,12 @@ lemma comp_C_integral_of_surjective_of_jacobson {R : Type*} [integral_domain R] begin haveI : (f.ker).is_maximal := @comap_is_maximal_of_surjective _ _ _ _ f ⊥ hf bot_is_maximal, let g : f.ker.quotient →+* S := ideal.quotient.lift f.ker f (λ _ h, h), - have hfg : (g.comp (quotient.mk f.ker)) = f := quotient.lift_comp_mk f.ker f _, + have hfg : (g.comp (quotient.mk f.ker)) = f := ring_hom_ext (λ (r : R), rfl) (λ i, rfl), rw [← hfg, ring_hom.comp_assoc], refine ring_hom.is_integral_trans _ g (quotient_mk_comp_C_is_integral_of_jacobson f.ker) - (g.is_integral_of_surjective (quotient.lift_surjective f.ker f _ hf)), + (g.is_integral_of_surjective _),--(quotient.lift_surjective f.ker f _ hf)), + rw [← hfg] at hf, + exact function.surjective.of_comp hf, end end mv_polynomial From da02236e1ad3ebfec0f0cadcc7e9484cd3c80b68 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 29 Jan 2021 08:32:23 +0100 Subject: [PATCH 06/14] cleaning up --- src/ring_theory/jacobson.lean | 63 +++++++++++++++++------------------ 1 file changed, 30 insertions(+), 33 deletions(-) diff --git a/src/ring_theory/jacobson.lean b/src/ring_theory/jacobson.lean index ab00e0252f301..8ffebd9c40023 100644 --- a/src/ring_theory/jacobson.lean +++ b/src/ring_theory/jacobson.lean @@ -91,48 +91,27 @@ lemma semimodule.eq_bot_iff {R M : Type*} [semiring R] [add_comm_monoid M] [semi begin rw ← @semimodule.carrier_bot R, refine ⟨λ h, congr_arg submodule.carrier h, λ h, submodule.ext (λ x, ⟨λ xP, _, λ xb, _⟩)⟩, - { rcases P with ⟨P.carrier, P0, P_add, P_smul⟩, - dsimp at h, + { rcases P with ⟨P_carrier, P0, P_add, P_smul⟩, + refine (λ (h : P_carrier = (⊥ : submodule R M).carrier), _) h, simp_rw [h] at xP, exact xP }, { rw [(submodule.mem_bot R).mp xb], exact submodule.zero_mem _ } end - +/- lemma submodule.eq_bot_iff {R : Type*} [semiring R] (P : submodule R R) : P = ⊥ ↔ P.carrier = {0} := semimodule.eq_bot_iff P ---lemma ideal.carrier_bot {R : Type*} [comm_semiring R] : (⊥ : ideal R).carrier = {0} := rfl - ---lemma ideal.eq_bot_iff {R : Type*} [comm_semiring R] (P : ideal R) : --- P = ⊥ ↔ P.carrier = {0} := ---semimodule.eq_bot_iff P - -lemma semimodule.ne_bot_iff {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] - (P : submodule R M) : - P ≠ ⊥ ↔ P.carrier ≠ {0} := -not_congr (semimodule.eq_bot_iff P) - lemma exists_mem_of_not_subset {R : Type*} {s t : set R} (st : ¬ s ⊆ t) : ∃ a ∈ s, a ∉ t := set.not_subset.mp st -lemma exists_mem_of_ne_bot {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] - {P : submodule R M} (Pb : P ≠ ⊥) : - ∃ (m : M), m ∈ P ∧ m ≠ 0 := -begin - have : ¬ P.carrier ⊆ {0}, - { rw semimodule.ne_bot_iff at Pb, - refine λ h, Pb (set.ext (λ x, ⟨λ xP, h xP, _⟩)), - rw set.mem_singleton_iff, - rintros rfl, - exact submodule.zero_mem P }, - obtain ⟨r, rP, r0⟩ := set.not_subset.mp this, - refine ⟨r, rP, _⟩, - rintro rfl, - exact r0 (set.mem_singleton 0), -end +lemma ideal.carrier_bot {R : Type*} [comm_semiring R] : (⊥ : ideal R).carrier = {0} := rfl + +lemma ideal.eq_bot_iff {R : Type*} [comm_semiring R] (P : ideal R) : + P = ⊥ ↔ P.carrier = {0} := +semimodule.eq_bot_iff P lemma ideal.exists_mem_of_ne_bot {R : Type*} [comm_semiring R] {P : ideal R} (Pb : P ≠ ⊥) : ∃ (r : R), r ∈ P ∧ r ≠ 0 := @@ -145,17 +124,35 @@ exists_mem_of_ne_bot Pb lemma submodule.exists_mem_of_ne_bot {R : Type*} [semiring R] {P : submodule R R} (Pb : P ≠ ⊥) : ∃ (r : R), r ∈ P ∧ r ≠ 0 := exists_mem_of_ne_bot Pb +-/ + +lemma semimodule.ne_bot_iff {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] + (P : submodule R M) : + P ≠ ⊥ ↔ P.carrier ≠ {0} := +not_congr (semimodule.eq_bot_iff P) + +lemma exists_mem_of_ne_bot {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] + {P : submodule R M} (Pb : P ≠ ⊥) : + ∃ (m : M), m ∈ P ∧ m ≠ 0 := +begin + have : ¬ P.carrier ⊆ {0}, + { refine λ h, ((semimodule.ne_bot_iff _).mp Pb) (set.ext (λ x, ⟨λ xP, h xP, λ hx, _⟩)), + rw set.mem_singleton_iff.mp hx, + exact submodule.zero_mem P }, + obtain ⟨r, rP, r0⟩ := set.not_subset.mp this, + refine ⟨r, rP, _⟩, + rwa [set.mem_singleton_iff] at r0, +end lemma exists_nonzero {R : Type*} [comm_ring R] {P : ideal (polynomial R)} (Pb : P ≠ ⊥) (hP : ∀ (x : R), C x ∈ P → x = 0) : ∃ p : polynomial R, p ∈ P ∧ (polynomial.map (quotient.mk (P.comap C)) p) ≠ 0 := begin obtain ⟨p, hp, p0⟩ := exists_mem_of_ne_bot Pb, - refine ⟨p, hp, λ pp0, p0 _⟩, - refine (is_add_group_hom.injective_iff (polynomial.map (quotient.mk (P.comap C)))).mp _ p pp0, + refine ⟨p, hp, λ pp0, p0 ((is_add_group_hom.injective_iff _).mp _ p pp0)⟩, refine map_injective _ ((quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr _), - rw [mk_ker, semimodule.eq_bot_iff], - refine set.ext (λ (r : R), ⟨λ h, hP _ h, λ h, _⟩), + rw [mk_ker], + refine (semimodule.eq_bot_iff _).mpr (set.ext (λ (r : R), ⟨λ h, hP _ h, λ h, _⟩)), rw [set.mem_singleton_iff.mp h], exact (P.comap (C : R →+* polynomial R)).zero_mem', end From d198c178d49076c6fb3eeb6111f904cbd6bb143b Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 29 Jan 2021 14:39:55 +0100 Subject: [PATCH 07/14] add module doc-strings --- src/ring_theory/ideal/operations.lean | 2 +- src/ring_theory/jacobson.lean | 146 ++++++++++++++++---------- 2 files changed, 94 insertions(+), 54 deletions(-) diff --git a/src/ring_theory/ideal/operations.lean b/src/ring_theory/ideal/operations.lean index 6499593dff416..ef224b47cdefe 100644 --- a/src/ring_theory/ideal/operations.lean +++ b/src/ring_theory/ideal/operations.lean @@ -1190,7 +1190,7 @@ lemma quotient_map_comp_mk {J : ideal R} {I : ideal S} {f : R →+* S} (H : J (quotient_map I f H).comp (quotient.mk J) = (quotient.mk I).comp f := ring_hom.ext (λ x, by simp only [function.comp_app, ring_hom.coe_comp, ideal.quotient_map_mk]) -/-- `H` and `h` are kept as seperate hypothesis since H is used in constructing the quotient map -/ +/-- `H` and `h` are kept as separate hypothesis since H is used in constructing the quotient map -/ lemma quotient_map_injective' {J : ideal R} {I : ideal S} {f : R →+* S} {H : J ≤ I.comap f} (h : I.comap f ≤ J) : function.injective (quotient_map I f H) := begin diff --git a/src/ring_theory/jacobson.lean b/src/ring_theory/jacobson.lean index 8ffebd9c40023..01a7e7602aee8 100644 --- a/src/ring_theory/jacobson.lean +++ b/src/ring_theory/jacobson.lean @@ -46,6 +46,10 @@ Honestly, I did not spend time to unwind their "meaning", hence the names are li TODO: clean up, move elsewhere -/ +/-- Let `P` be an ideal in `R[x]`. The map +`R[x]/P → (R / (P ∩ R))[x] / (P / (P ∩ R))` +is injective. +-/ lemma injective_quotient_le_comap_map {R : Type*} [comm_ring R] (P : ideal (polynomial R)) : function.injective ((map (map_ring_hom (quotient.mk (P.comap C))) P).quotient_map (map_ring_hom (quotient.mk (P.comap C))) le_comap_map) := @@ -58,8 +62,15 @@ begin simpa only [coeff_map, coe_map_ring_hom] using ext_iff.mp (ideal.mem_bot.mp (mem_comap.mp hp)) n, end -/-- The identity in this lemma is used in the proof of `quotient_mk_comp_C_is_integral_of_jacobson`. -It is isolated, since it speeds up the processing, avoiding a deterministic timeout. -/ +/-- +The identity in this lemma asserts that the "obvious" square +` R → (R / (P ∩ R))` +` ↓ ↓` +`R[x] / P → (R / (P ∩ R))[x] / (P / (P ∩ R))` +commutes. It is used in the proof of `quotient_mk_comp_C_is_integral_of_jacobson`. + +It is isolated, since it speeds up the processing, avoiding a deterministic timeout. +-/ lemma quotient_mk_maps_eq {R : Type*} [comm_ring R] (P : ideal (polynomial R)) : ((quotient.mk (map (map_ring_hom (quotient.mk (P.comap C))) P)).comp C).comp (quotient.mk (P.comap C)) = @@ -72,16 +83,6 @@ begin end /- -lemma quotient.mk_bot_injective_of {R : Type*} [comm_ring R] : - function.injective (quotient.mk (⊥ : ideal R)) := -begin - rw is_add_group_hom.injective_iff, - intros r hr, - admit, -end --/ - - lemma semimodule.carrier_bot {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] : (⊥ : submodule R M).carrier = {0} := rfl @@ -98,7 +99,72 @@ begin { rw [(submodule.mem_bot R).mp xb], exact submodule.zero_mem _ } end -/- + +lemma exists_mem_of_ne_bot {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] + {P : submodule R M} (Pb : P ≠ ⊥) : + ∃ (m : M), m ∈ P ∧ m ≠ 0 := +begin + obtain ⟨m, hm⟩ := submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb), + exact ⟨m, submodule.coe_mem m, λ f, hm (submodule.coe_eq_zero.mp f)⟩, +end + +--does not work +lemma exists_nonzero_1 {R S : Type*} [comm_ring R] [comm_ring S] (f : R →+* S) {P : ideal S} + (Pb : P ≠ ⊥) (hP : ∀ (x : R), f x ∈ P → x = 0) : + ∃ p : S, p ∈ P ∧ (polynomial.map (quotient.mk (P.comap f)) p) ≠ 0 := +begin + obtain ⟨m, hm⟩ := submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb), + refine ⟨m, submodule.coe_mem m, λ pp0, hm (submodule.coe_eq_zero.mp _)⟩, + apply (is_add_group_hom.injective_iff (polynomial.map (quotient.mk (P.comap C)))).mp _ _ pp0, + refine map_injective _ ((quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr _), + rw [mk_ker], + exact (submodule.eq_bot_iff _).mpr (λ x hx, hP x (mem_comap.mp hx)), +end + +lemma exists_nonzero_alone {R : Type*} [comm_ring R] {P : ideal (polynomial R)} + (Pb : P ≠ ⊥) : + ∃ p : polynomial R, p ∈ P ∧ p ≠ 0 := +begin + obtain ⟨m, hm⟩ := submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb), + exact ⟨m, submodule.coe_mem m, λ pp0, hm (submodule.coe_eq_zero.mp pp0)⟩, +end + +lemma exists_nonzero {R : Type*} [comm_ring R] {P : ideal (polynomial R)} + (Pb : P ≠ ⊥) (hP : ∀ (x : R), C x ∈ P → x = 0) : + ∃ p : polynomial R, p ∈ P ∧ (polynomial.map (quotient.mk (P.comap C)) p) ≠ 0 := +begin + obtain ⟨m, hm, m0⟩ := exists_nonzero_alone Pb, + refine ⟨m, hm, λ h, m0 _⟩, + refine (is_add_group_hom.injective_iff (polynomial.map (quotient.mk (P.comap C)))).mp _ _ h, + refine map_injective _ ((quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr _), + rw [mk_ker], + exact (submodule.eq_bot_iff _).mpr (λ x hx, hP x (mem_comap.mp hx)), +end +-/ + +lemma exists_nonzero {R : Type*} [comm_ring R] {P : ideal (polynomial R)} + (Pb : P ≠ ⊥) (hP : ∀ (x : R), C x ∈ P → x = 0) : + ∃ p : polynomial R, p ∈ P ∧ (polynomial.map (quotient.mk (P.comap C)) p) ≠ 0 := +begin + obtain ⟨m, hm⟩ := submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb), + refine ⟨m, submodule.coe_mem m, λ pp0, hm (submodule.coe_eq_zero.mp _)⟩, + refine (is_add_group_hom.injective_iff (polynomial.map (quotient.mk (P.comap C)))).mp _ _ pp0, + refine map_injective _ ((quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr _), + rw [mk_ker], + exact (submodule.eq_bot_iff _).mpr (λ x hx, hP x (mem_comap.mp hx)), +end + +/- unproven +lemma quotient.mk_bot_injective_of {R : Type*} [comm_ring R] : + function.injective (quotient.mk (⊥ : ideal R)) := +begin + rw is_add_group_hom.injective_iff, + intros r hr, + admit, +end +-/ + +/- these lemmas have their proofs, but do not seem to be needed lemma submodule.eq_bot_iff {R : Type*} [semiring R] (P : submodule R R) : P = ⊥ ↔ P.carrier = {0} := semimodule.eq_bot_iff P @@ -124,38 +190,12 @@ exists_mem_of_ne_bot Pb lemma submodule.exists_mem_of_ne_bot {R : Type*} [semiring R] {P : submodule R R} (Pb : P ≠ ⊥) : ∃ (r : R), r ∈ P ∧ r ≠ 0 := exists_mem_of_ne_bot Pb --/ lemma semimodule.ne_bot_iff {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] (P : submodule R M) : P ≠ ⊥ ↔ P.carrier ≠ {0} := not_congr (semimodule.eq_bot_iff P) - -lemma exists_mem_of_ne_bot {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] - {P : submodule R M} (Pb : P ≠ ⊥) : - ∃ (m : M), m ∈ P ∧ m ≠ 0 := -begin - have : ¬ P.carrier ⊆ {0}, - { refine λ h, ((semimodule.ne_bot_iff _).mp Pb) (set.ext (λ x, ⟨λ xP, h xP, λ hx, _⟩)), - rw set.mem_singleton_iff.mp hx, - exact submodule.zero_mem P }, - obtain ⟨r, rP, r0⟩ := set.not_subset.mp this, - refine ⟨r, rP, _⟩, - rwa [set.mem_singleton_iff] at r0, -end - -lemma exists_nonzero {R : Type*} [comm_ring R] {P : ideal (polynomial R)} - (Pb : P ≠ ⊥) (hP : ∀ (x : R), C x ∈ P → x = 0) : - ∃ p : polynomial R, p ∈ P ∧ (polynomial.map (quotient.mk (P.comap C)) p) ≠ 0 := -begin - obtain ⟨p, hp, p0⟩ := exists_mem_of_ne_bot Pb, - refine ⟨p, hp, λ pp0, p0 ((is_add_group_hom.injective_iff _).mp _ p pp0)⟩, - refine map_injective _ ((quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr _), - rw [mk_ker], - refine (semimodule.eq_bot_iff _).mpr (set.ext (λ (r : R), ⟨λ h, hP _ h, λ h, _⟩)), - rw [set.mem_singleton_iff.mp h], - exact (P.comap (C : R →+* polynomial R)).zero_mem', -end +-/ end technical_lemmas @@ -468,15 +508,13 @@ private lemma is_jacobson_polynomial_of_domain (R : Type*) [integral_domain R] [ begin by_cases Pb : (P = ⊥), { exact Pb.symm ▸ jacobson_bot_polynomial_of_jacobson_bot (hR ⊥ radical_bot_of_integral_domain) }, - { obtain ⟨p, pP, p0⟩ : ∃ p, p ∈ P ∧ polynomial.map (quotient.mk (P.comap C)) p ≠ 0 := - exists_nonzero Pb hP, - refine jacobson_eq_iff_jacobson_quotient_eq_bot.mpr _, + { refine jacobson_eq_iff_jacobson_quotient_eq_bot.mpr _, haveI : (P.comap (C : R →+* polynomial R)).is_prime := comap_is_prime C P, + obtain ⟨p, pP, p0⟩ := exists_nonzero Pb hP, refine jacobson_bot_of_integral_localization (quotient_map P C le_rfl) quotient_map_injective _ _ (localization.of (submonoid.powers (p.map (quotient.mk (P.comap C))).leading_coeff)) - (localization.of _) (is_integral_localization_map_polynomial_quotient P _ _ _ _), - rwa [ne.def, leading_coeff_eq_zero], - exact pP, }, + (localization.of _) (is_integral_localization_map_polynomial_quotient P _ pP _ _), + rwa [ne.def, leading_coeff_eq_zero] } end lemma is_jacobson_polynomial_of_is_jacobson (hR : is_jacobson R) : @@ -530,14 +568,16 @@ lemma is_maximal_comap_C_of_is_maximal (hP' : ∀ (x : R), C x ∈ P → x = 0) is_maximal (comap C P : ideal R) := begin haveI hp'_prime : (P.comap C : ideal R).is_prime := comap_is_prime C P, - obtain ⟨pX, hpX, hp0⟩ := - exists_mem_of_ne_bot (ne_of_lt (bot_lt_of_maximal P polynomial_not_is_field)).symm, + obtain ⟨m, hm⟩ := submodule.nonzero_mem_of_bot_lt (bot_lt_of_maximal P polynomial_not_is_field), + have : (m : polynomial R) ≠ 0, rwa [ne.def, submodule.coe_eq_zero], let φ : (P.comap C : ideal R).quotient →+* P.quotient := quotient_map P C le_rfl, let M : submonoid (P.comap C : ideal R).quotient := - submonoid.powers (pX.map (quotient.mk (P.comap C : ideal R))).leading_coeff, + submonoid.powers ((m : polynomial R).map (quotient.mk (P.comap C : ideal R))).leading_coeff, +-- let M : submonoid (P.comap C : ideal R).quotient := +-- submonoid.powers (pX.map (quotient.mk (P.comap C : ideal R))).leading_coeff, rw ← bot_quotient_is_maximal_iff at hP ⊢, - have hp0 : (pX.map (quotient.mk (P.comap C : ideal R))).leading_coeff ≠ 0 := - λ hp0', hp0 $ map_injective (quotient.mk (P.comap C : ideal R)) + have hp0 : ((m : polynomial R).map (quotient.mk (P.comap C : ideal R))).leading_coeff ≠ 0 := + λ hp0', this $ map_injective (quotient.mk (P.comap C : ideal R)) ((quotient.mk (P.comap C : ideal R)).injective_iff.2 (λ x hx, by rwa [quotient.eq_zero_iff_mem, (by rwa eq_bot_iff : (P.comap C : ideal R) = ⊥)] at hx)) (by simpa only [leading_coeff_eq_zero, map_zero] using hp0'), @@ -557,7 +597,7 @@ begin { rw le_antisymm bot_le (comap_bot_le_of_injective _ (map_injective_of_injective _ quotient_map_injective M ϕ ϕ' (le_non_zero_divisors_of_domain hM'))), refine is_maximal_comap_of_is_integral_of_is_maximal' _ _ ⊥ this, - exact is_integral_localization_map_polynomial_quotient P pX hpX ϕ ϕ' }, + refine is_integral_localization_map_polynomial_quotient P _ (submodule.coe_mem m) ϕ ϕ', }, rw (map_bot.symm : (⊥ : ideal (localization M')) = map ϕ'.to_map ⊥), refine map.is_maximal ϕ'.to_map (localization_map_bijective_of_field hM' _ ϕ') hP, rwa [← quotient.maximal_ideal_iff_is_field_quotient, ← bot_quotient_is_maximal_iff], @@ -580,7 +620,7 @@ begin refine ((quotient_map P C le_rfl).is_integral_tower_bot_of_is_integral (localization.of (M.map ↑(quotient_map P C le_rfl))).to_map _ _), { refine ϕ'.injective (le_non_zero_divisors_of_domain (λ hM', hM _)), - exact (let ⟨z, hz⟩ := hM' in (quotient_map_injective (trans hz.2 φ.map_zero.symm)) ▸ hz.1) }, + exact (let ⟨z, zM, z0⟩ := hM' in (quotient_map_injective (trans z0 φ.map_zero.symm)) ▸ zM) }, { let ϕ : localization_map M (localization M) := localization.of M, rw ← (ϕ.map_comp _), refine ring_hom.is_integral_trans ϕ.to_map From d8bd499d4766a671e5f4ce981e60c6b7160d72c4 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 29 Jan 2021 15:08:07 +0100 Subject: [PATCH 08/14] move three lemmas to ring_theory/ideal/over clean up --- src/ring_theory/ideal/over.lean | 52 ++++++++++ src/ring_theory/jacobson.lean | 165 +------------------------------- 2 files changed, 54 insertions(+), 163 deletions(-) diff --git a/src/ring_theory/ideal/over.lean b/src/ring_theory/ideal/over.lean index abf600efd003c..956ee45e42daf 100644 --- a/src/ring_theory/ideal/over.lean +++ b/src/ring_theory/ideal/over.lean @@ -62,6 +62,58 @@ begin refine ⟨i + 1, _, _⟩; simp [hi, mem] } end +/-- Let `P` be an ideal in `R[x]`. The map +`R[x]/P → (R / (P ∩ R))[x] / (P / (P ∩ R))` +is injective. +-/ +lemma injective_quotient_le_comap_map (P : ideal (polynomial R)) : + function.injective ((map (map_ring_hom (quotient.mk (P.comap C))) P).quotient_map + (map_ring_hom (quotient.mk (P.comap C))) le_comap_map) := +begin + refine quotient_map_injective' (le_of_eq _), + rw comap_map_of_surjective + (map_ring_hom (quotient.mk (P.comap C))) (map_surjective _ quotient.mk_surjective), + refine le_antisymm (sup_le le_rfl _) (le_sup_left_of_le le_rfl), + refine λ p hp, polynomial_mem_ideal_of_coeff_mem_ideal P p (λ n, quotient.eq_zero_iff_mem.mp _), + simpa only [coeff_map, coe_map_ring_hom] using ext_iff.mp (ideal.mem_bot.mp (mem_comap.mp hp)) n, +end + +/-- +The identity in this lemma asserts that the "obvious" square +` R → (R / (P ∩ R))` +` ↓ ↓` +`R[x] / P → (R / (P ∩ R))[x] / (P / (P ∩ R))` +commutes. It is used, for instance, in the proof of `quotient_mk_comp_C_is_integral_of_jacobson`, +in the file `ring_theory/jacobson`. +-/ +lemma quotient_mk_maps_eq (P : ideal (polynomial R)) : + ((quotient.mk (map (map_ring_hom (quotient.mk (P.comap C))) P)).comp C).comp + (quotient.mk (P.comap C)) = + ((map (map_ring_hom (quotient.mk (P.comap C))) P).quotient_map + (map_ring_hom (quotient.mk (P.comap C))) le_comap_map).comp ((quotient.mk P).comp C) := +begin + refine ring_hom.ext (λ x, _), + repeat { rw [ring_hom.coe_comp, function.comp_app] }, + rw [quotient_map_mk, coe_map_ring_hom, map_C], +end + +/-- +This technical lemma asserts the existence of a polynomial `p` in an ideal `P ⊂ R[x]` +that is non-zero in the quotient `R / (P ∩ R) [x]`. The assumptions are equivalent to +`P ≠ 0` and `P ∩ R = (0)`. +-/ +lemma exists_nonzero_mem_of_ne_bot {P : ideal (polynomial R)} + (Pb : P ≠ ⊥) (hP : ∀ (x : R), C x ∈ P → x = 0) : + ∃ p : polynomial R, p ∈ P ∧ (polynomial.map (quotient.mk (P.comap C)) p) ≠ 0 := +begin + obtain ⟨m, hm⟩ := submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb), + refine ⟨m, submodule.coe_mem m, λ pp0, hm (submodule.coe_eq_zero.mp _)⟩, + refine (is_add_group_hom.injective_iff (polynomial.map (quotient.mk (P.comap C)))).mp _ _ pp0, + refine map_injective _ ((quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr _), + rw [mk_ker], + exact (submodule.eq_bot_iff _).mpr (λ x hx, hP x (mem_comap.mp hx)), +end + end comm_ring section integral_domain diff --git a/src/ring_theory/jacobson.lean b/src/ring_theory/jacobson.lean index 01a7e7602aee8..ed3e43867099c 100644 --- a/src/ring_theory/jacobson.lean +++ b/src/ring_theory/jacobson.lean @@ -38,167 +38,6 @@ namespace ideal open polynomial -section technical_lemmas -/-! -The following two lemmas are independent of Jacobson. I extracted them from the -original proof of `quotient_mk_comp_C_is_integral_of_jacobson` to speed up processing. -Honestly, I did not spend time to unwind their "meaning", hence the names are likely inappropriate. - -TODO: clean up, move elsewhere --/ -/-- Let `P` be an ideal in `R[x]`. The map -`R[x]/P → (R / (P ∩ R))[x] / (P / (P ∩ R))` -is injective. --/ -lemma injective_quotient_le_comap_map {R : Type*} [comm_ring R] (P : ideal (polynomial R)) : - function.injective ((map (map_ring_hom (quotient.mk (P.comap C))) P).quotient_map - (map_ring_hom (quotient.mk (P.comap C))) le_comap_map) := -begin - refine quotient_map_injective' (le_of_eq _), - rw comap_map_of_surjective - (map_ring_hom (quotient.mk (P.comap C))) (map_surjective _ quotient.mk_surjective), - refine le_antisymm (sup_le le_rfl _) (le_sup_left_of_le le_rfl), - refine λ p hp, polynomial_mem_ideal_of_coeff_mem_ideal P p (λ n, quotient.eq_zero_iff_mem.mp _), - simpa only [coeff_map, coe_map_ring_hom] using ext_iff.mp (ideal.mem_bot.mp (mem_comap.mp hp)) n, -end - -/-- -The identity in this lemma asserts that the "obvious" square -` R → (R / (P ∩ R))` -` ↓ ↓` -`R[x] / P → (R / (P ∩ R))[x] / (P / (P ∩ R))` -commutes. It is used in the proof of `quotient_mk_comp_C_is_integral_of_jacobson`. - -It is isolated, since it speeds up the processing, avoiding a deterministic timeout. --/ -lemma quotient_mk_maps_eq {R : Type*} [comm_ring R] (P : ideal (polynomial R)) : - ((quotient.mk (map (map_ring_hom (quotient.mk (P.comap C))) P)).comp C).comp - (quotient.mk (P.comap C)) = - ((map (map_ring_hom (quotient.mk (P.comap C))) P).quotient_map - (map_ring_hom (quotient.mk (P.comap C))) le_comap_map).comp ((quotient.mk P).comp C) := -begin - refine ring_hom.ext (λ x, _), - repeat { rw [ring_hom.coe_comp, function.comp_app] }, - rw [quotient_map_mk, coe_map_ring_hom, map_C], -end - -/- -lemma semimodule.carrier_bot {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] : - (⊥ : submodule R M).carrier = {0} := rfl - -lemma semimodule.eq_bot_iff {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] - (P : submodule R M) : - P = ⊥ ↔ P.carrier = {0} := -begin - rw ← @semimodule.carrier_bot R, - refine ⟨λ h, congr_arg submodule.carrier h, λ h, submodule.ext (λ x, ⟨λ xP, _, λ xb, _⟩)⟩, - { rcases P with ⟨P_carrier, P0, P_add, P_smul⟩, - refine (λ (h : P_carrier = (⊥ : submodule R M).carrier), _) h, - simp_rw [h] at xP, - exact xP }, - { rw [(submodule.mem_bot R).mp xb], - exact submodule.zero_mem _ } -end - -lemma exists_mem_of_ne_bot {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] - {P : submodule R M} (Pb : P ≠ ⊥) : - ∃ (m : M), m ∈ P ∧ m ≠ 0 := -begin - obtain ⟨m, hm⟩ := submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb), - exact ⟨m, submodule.coe_mem m, λ f, hm (submodule.coe_eq_zero.mp f)⟩, -end - ---does not work -lemma exists_nonzero_1 {R S : Type*} [comm_ring R] [comm_ring S] (f : R →+* S) {P : ideal S} - (Pb : P ≠ ⊥) (hP : ∀ (x : R), f x ∈ P → x = 0) : - ∃ p : S, p ∈ P ∧ (polynomial.map (quotient.mk (P.comap f)) p) ≠ 0 := -begin - obtain ⟨m, hm⟩ := submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb), - refine ⟨m, submodule.coe_mem m, λ pp0, hm (submodule.coe_eq_zero.mp _)⟩, - apply (is_add_group_hom.injective_iff (polynomial.map (quotient.mk (P.comap C)))).mp _ _ pp0, - refine map_injective _ ((quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr _), - rw [mk_ker], - exact (submodule.eq_bot_iff _).mpr (λ x hx, hP x (mem_comap.mp hx)), -end - -lemma exists_nonzero_alone {R : Type*} [comm_ring R] {P : ideal (polynomial R)} - (Pb : P ≠ ⊥) : - ∃ p : polynomial R, p ∈ P ∧ p ≠ 0 := -begin - obtain ⟨m, hm⟩ := submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb), - exact ⟨m, submodule.coe_mem m, λ pp0, hm (submodule.coe_eq_zero.mp pp0)⟩, -end - -lemma exists_nonzero {R : Type*} [comm_ring R] {P : ideal (polynomial R)} - (Pb : P ≠ ⊥) (hP : ∀ (x : R), C x ∈ P → x = 0) : - ∃ p : polynomial R, p ∈ P ∧ (polynomial.map (quotient.mk (P.comap C)) p) ≠ 0 := -begin - obtain ⟨m, hm, m0⟩ := exists_nonzero_alone Pb, - refine ⟨m, hm, λ h, m0 _⟩, - refine (is_add_group_hom.injective_iff (polynomial.map (quotient.mk (P.comap C)))).mp _ _ h, - refine map_injective _ ((quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr _), - rw [mk_ker], - exact (submodule.eq_bot_iff _).mpr (λ x hx, hP x (mem_comap.mp hx)), -end --/ - -lemma exists_nonzero {R : Type*} [comm_ring R] {P : ideal (polynomial R)} - (Pb : P ≠ ⊥) (hP : ∀ (x : R), C x ∈ P → x = 0) : - ∃ p : polynomial R, p ∈ P ∧ (polynomial.map (quotient.mk (P.comap C)) p) ≠ 0 := -begin - obtain ⟨m, hm⟩ := submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb), - refine ⟨m, submodule.coe_mem m, λ pp0, hm (submodule.coe_eq_zero.mp _)⟩, - refine (is_add_group_hom.injective_iff (polynomial.map (quotient.mk (P.comap C)))).mp _ _ pp0, - refine map_injective _ ((quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr _), - rw [mk_ker], - exact (submodule.eq_bot_iff _).mpr (λ x hx, hP x (mem_comap.mp hx)), -end - -/- unproven -lemma quotient.mk_bot_injective_of {R : Type*} [comm_ring R] : - function.injective (quotient.mk (⊥ : ideal R)) := -begin - rw is_add_group_hom.injective_iff, - intros r hr, - admit, -end --/ - -/- these lemmas have their proofs, but do not seem to be needed -lemma submodule.eq_bot_iff {R : Type*} [semiring R] (P : submodule R R) : - P = ⊥ ↔ P.carrier = {0} := -semimodule.eq_bot_iff P - -lemma exists_mem_of_not_subset {R : Type*} {s t : set R} (st : ¬ s ⊆ t) : - ∃ a ∈ s, a ∉ t := -set.not_subset.mp st - -lemma ideal.carrier_bot {R : Type*} [comm_semiring R] : (⊥ : ideal R).carrier = {0} := rfl - -lemma ideal.eq_bot_iff {R : Type*} [comm_semiring R] (P : ideal R) : - P = ⊥ ↔ P.carrier = {0} := -semimodule.eq_bot_iff P - -lemma ideal.exists_mem_of_ne_bot {R : Type*} [comm_semiring R] {P : ideal R} (Pb : P ≠ ⊥) : - ∃ (r : R), r ∈ P ∧ r ≠ 0 := -exists_mem_of_ne_bot Pb - -lemma ideal_v.exists_mem_of_ne_bot {R : Type*} [comm_ring R] {P : ideal R} (Pb : P ≠ ⊥) : - ∃ (r : R), r ∈ P ∧ r ≠ 0 := -exists_mem_of_ne_bot Pb - -lemma submodule.exists_mem_of_ne_bot {R : Type*} [semiring R] {P : submodule R R} (Pb : P ≠ ⊥) : - ∃ (r : R), r ∈ P ∧ r ≠ 0 := -exists_mem_of_ne_bot Pb - -lemma semimodule.ne_bot_iff {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] - (P : submodule R M) : - P ≠ ⊥ ↔ P.carrier ≠ {0} := -not_congr (semimodule.eq_bot_iff P) --/ - -end technical_lemmas - section is_jacobson variables {R S : Type*} [comm_ring R] [comm_ring S] {I : ideal R} @@ -510,7 +349,7 @@ begin { exact Pb.symm ▸ jacobson_bot_polynomial_of_jacobson_bot (hR ⊥ radical_bot_of_integral_domain) }, { refine jacobson_eq_iff_jacobson_quotient_eq_bot.mpr _, haveI : (P.comap (C : R →+* polynomial R)).is_prime := comap_is_prime C P, - obtain ⟨p, pP, p0⟩ := exists_nonzero Pb hP, + obtain ⟨p, pP, p0⟩ := exists_nonzero_mem_of_ne_bot Pb hP, refine jacobson_bot_of_integral_localization (quotient_map P C le_rfl) quotient_map_injective _ _ (localization.of (submonoid.powers (p.map (quotient.mk (P.comap C))).leading_coeff)) (localization.of _) (is_integral_localization_map_polynomial_quotient P _ pP _ _), @@ -611,7 +450,7 @@ begin refine (is_integral_quotient_map_iff _).mp _, let P' : ideal R := P.comap C, obtain ⟨pX, hpX, hp0⟩ := - exists_nonzero (ne_of_lt (bot_lt_of_maximal P polynomial_not_is_field)).symm hP', + exists_nonzero_mem_of_ne_bot (ne_of_lt (bot_lt_of_maximal P polynomial_not_is_field)).symm hP', let M : submonoid P'.quotient := submonoid.powers (pX.map (quotient.mk P')).leading_coeff, let φ : P'.quotient →+* P.quotient := quotient_map P C le_rfl, let ϕ' : localization_map (M.map ↑φ) (localization (M.map ↑φ)) := localization.of (M.map ↑φ), From e09e0d615b1872385f9062ef61ce18f6a482fd15 Mon Sep 17 00:00:00 2001 From: damiano Date: Fri, 29 Jan 2021 18:21:58 +0100 Subject: [PATCH 09/14] Update src/algebra/ring_quot.lean Co-authored-by: Eric Wieser --- src/algebra/ring_quot.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/algebra/ring_quot.lean b/src/algebra/ring_quot.lean index db1d93a0815b2..823efa49f3f37 100644 --- a/src/algebra/ring_quot.lean +++ b/src/algebra/ring_quot.lean @@ -191,7 +191,7 @@ begin refine λ x h, submodule.span_induction h _ _ _ _, { rintro y ⟨a, b, h, su⟩, symmetry' at su, - rw ← ((sub_eq_iff_eq_add)) at su, + rw ←sub_eq_iff_eq_add at su, rw [ ← su, ring_hom.map_sub, mk_ring_hom_rel h, sub_self], }, { simp, }, { intros a b ha hb, simp [ha, hb], }, From da2290171e0ac209d9fddceeb8d5d71a6ba5a876 Mon Sep 17 00:00:00 2001 From: damiano Date: Fri, 29 Jan 2021 18:22:05 +0100 Subject: [PATCH 10/14] Update src/ring_theory/ideal/over.lean Co-authored-by: Eric Wieser --- src/ring_theory/ideal/over.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/ring_theory/ideal/over.lean b/src/ring_theory/ideal/over.lean index 956ee45e42daf..af4a1b06ef008 100644 --- a/src/ring_theory/ideal/over.lean +++ b/src/ring_theory/ideal/over.lean @@ -80,9 +80,11 @@ end /-- The identity in this lemma asserts that the "obvious" square -` R → (R / (P ∩ R))` -` ↓ ↓` -`R[x] / P → (R / (P ∩ R))[x] / (P / (P ∩ R))` +``` + R → (R / (P ∩ R)) + ↓ ↓ +R[x] / P → (R / (P ∩ R))[x] / (P / (P ∩ R)) +``` commutes. It is used, for instance, in the proof of `quotient_mk_comp_C_is_integral_of_jacobson`, in the file `ring_theory/jacobson`. -/ From 26b66afa324b0bb722fb14dd4b3a4ba1de215b58 Mon Sep 17 00:00:00 2001 From: damiano Date: Fri, 29 Jan 2021 18:57:05 +0100 Subject: [PATCH 11/14] Update src/ring_theory/ideal/basic.lean Co-authored-by: Eric Wieser --- src/ring_theory/ideal/basic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/ring_theory/ideal/basic.lean b/src/ring_theory/ideal/basic.lean index 0ebafe268f606..6482a4aea36eb 100644 --- a/src/ring_theory/ideal/basic.lean +++ b/src/ring_theory/ideal/basic.lean @@ -299,7 +299,6 @@ variables [comm_ring α] (I : ideal α) {a b : α} 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 ---λ bi, ⟨λ h, sorry, λ h, ideal.add_mem I h bi⟩ lemma add_mem_iff_right : a ∈ I → (a + b ∈ I ↔ b ∈ I) := I.add_mem_iff_right From 0360340a5d82292d68ffe21276221bb04eac118f Mon Sep 17 00:00:00 2001 From: damiano Date: Fri, 29 Jan 2021 19:58:17 +0100 Subject: [PATCH 12/14] Update src/ring_theory/ideal/basic.lean Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com> --- src/ring_theory/ideal/basic.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/ring_theory/ideal/basic.lean b/src/ring_theory/ideal/basic.lean index 6482a4aea36eb..d6279691ee210 100644 --- a/src/ring_theory/ideal/basic.lean +++ b/src/ring_theory/ideal/basic.lean @@ -211,9 +211,7 @@ eq_iff_le_not_lt.2 ⟨IJ, λ h, hJ (hI.2 _ h)⟩ theorem is_maximal.is_prime {I : ideal α} (H : I.is_maximal) : I.is_prime := ⟨H.1, λ x y hxy, or_iff_not_imp_left.2 $ λ hx, begin let J : ideal α := submodule.span α (insert x ↑I), - have IJ : I ≤ J, - { rw ← span_eq I, - exact (span_mono (subset_insert x ↑I)) }, + have IJ : I ≤ J := (set.subset.trans (subset_insert _ _) subset_span), have oJ : (1 : α) ∈ J, { have H1 := H, cases H1 with Ht Hm, From 327118434c85f438f8c59064b9c187925cd16a0b Mon Sep 17 00:00:00 2001 From: damiano Date: Fri, 29 Jan 2021 19:58:48 +0100 Subject: [PATCH 13/14] Update src/ring_theory/ideal/basic.lean Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com> --- src/ring_theory/ideal/basic.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/ring_theory/ideal/basic.lean b/src/ring_theory/ideal/basic.lean index d6279691ee210..e97451912e902 100644 --- a/src/ring_theory/ideal/basic.lean +++ b/src/ring_theory/ideal/basic.lean @@ -212,13 +212,9 @@ theorem is_maximal.is_prime {I : ideal α} (H : I.is_maximal) : I.is_prime := ⟨H.1, λ x y hxy, or_iff_not_imp_left.2 $ λ hx, begin let J : ideal α := submodule.span α (insert x ↑I), have IJ : I ≤ J := (set.subset.trans (subset_insert _ _) subset_span), - have oJ : (1 : α) ∈ J, - { have H1 := H, - cases H1 with Ht Hm, - obtain ⟨-, F⟩ := is_maximal_iff.mp H, - refine F _ x IJ hx _, - refine mem_span_insert.mpr ⟨(1 : α), 0, submodule.zero_mem (span I.carrier), _⟩, - rw [one_mul, add_zero] }, + have xJ : x ∈ J := ideal.subset_span (set.mem_insert x I), + cases is_maximal_iff.1 H with _ oJ, + specialize oJ J x IJ hx xJ, rcases submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩, obtain (F : y * 1 = y * (a • x + b)) := congr_arg (λ g : α, y * g) oe, rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc], From b0d1dcd0b8275f1ddee87530861c5b570cf28f9f Mon Sep 17 00:00:00 2001 From: damiano Date: Mon, 1 Feb 2021 08:29:17 +0100 Subject: [PATCH 14/14] Apply Bryan's suggestions from code review Co-authored-by: Bryan Gin-ge Chen --- src/ring_theory/ideal/basic.lean | 2 +- src/ring_theory/jacobson.lean | 2 -- src/ring_theory/jacobson_ideal.lean | 2 +- 3 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/ring_theory/ideal/basic.lean b/src/ring_theory/ideal/basic.lean index e97451912e902..d493ef6891307 100644 --- a/src/ring_theory/ideal/basic.lean +++ b/src/ring_theory/ideal/basic.lean @@ -376,7 +376,7 @@ lemma is_integral_domain_iff_prime (I : ideal α) : is_integral_domain I.quotien λ h, by exactI integral_domain.to_is_integral_domain I.quotient⟩ lemma exists_inv {I : ideal α} [hI : I.is_maximal] : - ∀ {a : I.quotient}, a ≠ 0 → ∃ b : I.quotient, a * b = 1 := + ∀ {a : I.quotient}, a ≠ 0 → ∃ b : I.quotient, a * b = 1 := begin rintro ⟨a⟩ h, rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩, diff --git a/src/ring_theory/jacobson.lean b/src/ring_theory/jacobson.lean index ed3e43867099c..b4c5086c3d0d5 100644 --- a/src/ring_theory/jacobson.lean +++ b/src/ring_theory/jacobson.lean @@ -412,8 +412,6 @@ begin let φ : (P.comap C : ideal R).quotient →+* P.quotient := quotient_map P C le_rfl, let M : submonoid (P.comap C : ideal R).quotient := submonoid.powers ((m : polynomial R).map (quotient.mk (P.comap C : ideal R))).leading_coeff, --- let M : submonoid (P.comap C : ideal R).quotient := --- submonoid.powers (pX.map (quotient.mk (P.comap C : ideal R))).leading_coeff, rw ← bot_quotient_is_maximal_iff at hP ⊢, have hp0 : ((m : polynomial R).map (quotient.mk (P.comap C : ideal R))).leading_coeff ≠ 0 := λ hp0', this $ map_injective (quotient.mk (P.comap C : ideal R)) diff --git a/src/ring_theory/jacobson_ideal.lean b/src/ring_theory/jacobson_ideal.lean index c9890fc62a14e..afec95caec7e7 100644 --- a/src/ring_theory/jacobson_ideal.lean +++ b/src/ring_theory/jacobson_ideal.lean @@ -96,7 +96,7 @@ theorem mem_jacobson_iff {x : R} : x ∈ jacobson I ↔ ∀ y, ∃ z, x * y * z λ hx, mem_Inf.2 $ λ M ⟨him, hm⟩, classical.by_contradiction $ λ hxm, let ⟨y, hy⟩ := hm.exists_inv hxm, ⟨z, hz⟩ := hx (-y) in hm.1 $ (eq_top_iff_one _).2 $ sub_sub_cancel (x * -y * z + z) 1 ▸ M.sub_mem - (by {rw [← one_mul z, ← mul_assoc, ← add_mul, mul_one, mul_neg_eq_neg_mul_symm, neg_add_eq_sub, + (by { rw [← one_mul z, ← mul_assoc, ← add_mul, mul_one, mul_neg_eq_neg_mul_symm, neg_add_eq_sub, ← neg_sub, neg_mul_eq_neg_mul_symm, neg_mul_eq_mul_neg, mul_comm x y, mul_comm _ (- z)], rcases hy with ⟨i, hi, df⟩, rw [← (sub_eq_iff_eq_add.mpr df.symm), sub_sub, add_comm, ← sub_sub, sub_self, zero_sub],