[Merged by Bors] - refactor(ring_theory/ideal/*, ring_theory/jacobson): use comm_semiring instead of comm_ring for ideals

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], },

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,36 @@ 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
+
+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 +317,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 +385,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,17 +440,10 @@ 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
-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
@@ -629,6 +638,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 }
 
@@ -648,11 +659,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 α) ≠ ⊤,

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

src/ring_theory/ideal/over.lean

@@ -62,6 +62,60 @@ 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