chore(ring_theory): generalize non_zero_divisors lemmas to `monoid_…

…with_zero` (#8607)

None of the results about `non_zero_divisors` needed a ring structure, just a `monoid_with_zero`. So the generalization is obvious.

Shall we move this file to the `algebra` namespace sometime soon?

src/ring_theory/ideal/over.lean

@@ -257,7 +257,7 @@ begin
   let Rₚ := localization P.prime_compl,
   let Sₚ := localization (algebra.algebra_map_submonoid S P.prime_compl),
   letI : integral_domain (localization (algebra.algebra_map_submonoid S P.prime_compl)) :=
-    is_localization.integral_domain_localization (le_non_zero_divisors_of_domain hP0),
+    is_localization.integral_domain_localization (le_non_zero_divisors_of_no_zero_divisors hP0),
   obtain ⟨Qₚ : ideal Sₚ, Qₚ_maximal⟩ := exists_maximal Sₚ,
   haveI Qₚ_max : is_maximal (comap _ Qₚ) := @is_maximal_comap_of_is_integral_of_is_maximal Rₚ _ Sₚ _
     (localization_algebra P.prime_compl S)

src/ring_theory/jacobson.lean

@@ -333,7 +333,7 @@ lemma jacobson_bot_of_integral_localization {R : Type*} [integral_domain R] [is_
   (⊥ : ideal S).jacobson = (⊥ : ideal S) :=
 begin
   have hM : ((submonoid.powers x).map φ : submonoid S) ≤ non_zero_divisors S :=
-    map_le_non_zero_divisors_of_injective hφ (powers_le_non_zero_divisors_of_domain hx),
+    φ.map_le_non_zero_divisors_of_injective hφ (powers_le_non_zero_divisors_of_no_zero_divisors hx),
   letI : integral_domain Sₘ := is_localization.integral_domain_of_le_non_zero_divisors _ hM,
   let φ' : Rₘ →+* Sₘ := is_localization.map _ φ (submonoid.powers x).le_comap_map,
   suffices : ∀ I : ideal Sₘ, I.is_maximal → (I.comap (algebra_map S Sₘ)).is_maximal,
@@ -464,11 +464,11 @@ begin
   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') :=
-    is_localization.integral_domain_localization (le_non_zero_divisors_of_domain hM'),
+    is_localization.integral_domain_localization (le_non_zero_divisors_of_no_zero_divisors hM'),
   suffices : (⊥ : ideal (localization M')).is_maximal,
   { rw le_antisymm bot_le (comap_bot_le_of_injective _ (is_localization.map_injective_of_injective
       M (localization M) (localization M')
-      quotient_map_injective (le_non_zero_divisors_of_domain hM'))),
+      quotient_map_injective (le_non_zero_divisors_of_no_zero_divisors hM'))),
     refine is_maximal_comap_of_is_integral_of_is_maximal' _ _ ⊥ this,
     apply is_integral_is_localization_polynomial_quotient P _ (submodule.coe_mem m) },
   rw (map_bot.symm : (⊥ : ideal (localization M')) =
@@ -494,7 +494,7 @@ begin
   refine ((quotient_map P C le_rfl).is_integral_tower_bot_of_is_integral
     (algebra_map _ (localization M')) _ _),
   { refine is_localization.injective (localization M')
-      (show M' ≤ _, from le_non_zero_divisors_of_domain (λ hM', hM _)),
+      (show M' ≤ _, from le_non_zero_divisors_of_no_zero_divisors (λ hM', hM _)),
     exact (let ⟨z, zM, z0⟩ := hM' in (quotient_map_injective (trans z0 φ.map_zero.symm)) ▸ zM) },
   { rw ← is_localization.map_comp M.le_comap_map,
     refine ring_hom.is_integral_trans (algebra_map P'.quotient (localization M))

src/ring_theory/localization.lean

@@ -1151,7 +1151,8 @@ end
 
 protected lemma to_map_ne_zero_of_mem_non_zero_divisors [nontrivial R]
   (hM : M ≤ non_zero_divisors R) {x : R} (hx : x ∈ non_zero_divisors R) : algebra_map R S x ≠ 0 :=
-map_ne_zero_of_mem_non_zero_divisors (is_localization.injective S hM) hx
+show (algebra_map R S).to_monoid_with_zero_hom x ≠ 0,
+from (algebra_map R S).map_ne_zero_of_mem_non_zero_divisors (is_localization.injective S hM) hx
 
 variables (S Q M)
 
@@ -1215,7 +1216,8 @@ The localization of an integral domain at the complement of a prime ideal is an
 -/
 instance integral_domain_of_local_at_prime {P : ideal A} (hp : P.is_prime) :
   integral_domain (localization.at_prime P) :=
-integral_domain_localization (le_non_zero_divisors_of_domain (by simpa only [] using P.zero_mem))
+integral_domain_localization (le_non_zero_divisors_of_no_zero_divisors
+  (not_not_intro P.zero_mem))
 
 namespace at_prime
 
@@ -1347,7 +1349,7 @@ lemma localization_map_bijective_of_field {R Rₘ : Type*} [integral_domain R] [
   {M : submonoid R} (hM : (0 : R) ∉ M) (hR : is_field R)
   [algebra R Rₘ] [is_localization M Rₘ] : function.bijective (algebra_map R Rₘ) :=
 begin
-  refine ⟨is_localization.injective _ (le_non_zero_divisors_of_domain hM), λ x, _⟩,
+  refine ⟨is_localization.injective _ (le_non_zero_divisors_of_no_zero_divisors hM), λ x, _⟩,
   obtain ⟨r, ⟨m, hm⟩, rfl⟩ := mk'_surjective M x,
   obtain ⟨n, hn⟩ := hR.mul_inv_cancel (λ hm0, hM (hm0 ▸ hm) : m ≠ 0),
   exact ⟨r * n,
@@ -1467,7 +1469,8 @@ mk'_mk_eq_div s.2
 
 lemma is_unit_map_of_injective (hg : function.injective g)
   (y : non_zero_divisors A) : is_unit (g y) :=
-is_unit.mk0 (g y) $ map_ne_zero_of_mem_non_zero_divisors hg y.2
+is_unit.mk0 (g y) $ show g.to_monoid_with_zero_hom y ≠ 0,
+  from g.map_ne_zero_of_mem_non_zero_divisors hg y.2
 
 /-- Given an integral domain `A` with field of fractions `K`,
 and an injective ring hom `g : A →+* L` where `L` is a field, we get a
@@ -1487,7 +1490,7 @@ begin
   erw submonoid.localization_map.mul_inv_left
   (λ y : non_zero_divisors A, show is_unit (g.to_monoid_hom y), from
     is_unit_map_of_injective hg y),
-  exact (mul_div_cancel' _ (map_ne_zero_of_mem_non_zero_divisors hg y.2)).symm,
+  exact (mul_div_cancel' _ (g.map_ne_zero_of_mem_non_zero_divisors hg y.2)).symm,
 end
 
 /-- Given integral domains `A, B` with fields of fractions `K`, `L`
@@ -1497,7 +1500,7 @@ such that `z = f x * (f y)⁻¹`. -/
 noncomputable def map [algebra B L] [is_fraction_ring B L] {j : A →+* B} (hj : injective j) :
   K →+* L :=
 map L j (show non_zero_divisors A ≤ (non_zero_divisors B).comap j,
-         from λ y hy, map_mem_non_zero_divisors hj hy)
+         from λ y hy, j.map_mem_non_zero_divisors hj hy)
 
 /-- Given integral domains `A, B` and localization maps to their fields of fractions
 `f : A →+* K, g : B →+* L`, an isomorphism `j : A ≃+* B` induces an isomorphism of

src/ring_theory/non_zero_divisors.lean

@@ -23,10 +23,10 @@ def non_zero_divisors (R : Type*) [monoid_with_zero R] : submonoid R :=
     have z * x₁ * x₂ = 0, by rwa mul_assoc,
     hx₁ z $ hx₂ (z * x₁) this }
 
-variables {R A : Type*} [comm_ring R] [integral_domain A]
+variables {M M' M₁ : Type*} [monoid_with_zero M] [monoid_with_zero M'] [comm_monoid_with_zero M₁]
 
-lemma mul_mem_non_zero_divisors {a b : R} :
-  a * b ∈ non_zero_divisors R ↔ a ∈ non_zero_divisors R ∧ b ∈ non_zero_divisors R :=
+lemma mul_mem_non_zero_divisors {a b : M₁} :
+  a * b ∈ non_zero_divisors M₁ ↔ a ∈ non_zero_divisors M₁ ∧ b ∈ non_zero_divisors M₁ :=
 begin
   split,
   { intro h,
@@ -39,42 +39,66 @@ begin
     rw [mul_assoc, hx] },
 end
 
-lemma eq_zero_of_ne_zero_of_mul_right_eq_zero {x y : A} (hnx : x ≠ 0) (hxy : y * x = 0) : y = 0 :=
+lemma eq_zero_of_ne_zero_of_mul_right_eq_zero [no_zero_divisors M]
+  {x y : M} (hnx : x ≠ 0) (hxy : y * x = 0) : y = 0 :=
 or.resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero hxy) hnx
 
-lemma eq_zero_of_ne_zero_of_mul_left_eq_zero {x y : A} (hnx : x ≠ 0) (hxy : x * y = 0) : y = 0 :=
+lemma eq_zero_of_ne_zero_of_mul_left_eq_zero [no_zero_divisors M]
+  {x y : M} (hnx : x ≠ 0) (hxy : x * y = 0) : y = 0 :=
 or.resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero hxy) hnx
 
-lemma mem_non_zero_divisors_iff_ne_zero {x : A} : x ∈ non_zero_divisors A ↔ x ≠ 0 :=
+lemma mem_non_zero_divisors_iff_ne_zero [no_zero_divisors M] [nontrivial M] {x : M} :
+  x ∈ non_zero_divisors M ↔ x ≠ 0 :=
 ⟨λ hm hz, zero_ne_one (hm 1 $ by rw [hz, one_mul]).symm,
-λ hnx z, eq_zero_of_ne_zero_of_mul_right_eq_zero hnx⟩
+ λ hnx z, eq_zero_of_ne_zero_of_mul_right_eq_zero hnx⟩
 
-lemma map_ne_zero_of_mem_non_zero_divisors [nontrivial R] {B : Type*} [ring B] {g : R →+* B}
-  (hg : function.injective g) {x : R} (h : x ∈ non_zero_divisors R) : g x ≠ 0 :=
+lemma monoid_with_zero_hom.map_ne_zero_of_mem_non_zero_divisors [nontrivial M]
+  (g : monoid_with_zero_hom M M') (hg : function.injective g)
+  {x : M} (h : x ∈ non_zero_divisors M) : g x ≠ 0 :=
 λ h0, one_ne_zero (h 1 ((one_mul x).symm ▸ (hg (trans h0 g.map_zero.symm))))
 
-lemma map_mem_non_zero_divisors {B : Type*} [integral_domain B] {g : A →+* B}
-  (hg : function.injective g) {x : A} (h : x ∈ non_zero_divisors A) : g x ∈ non_zero_divisors B :=
-λ z hz, eq_zero_of_ne_zero_of_mul_right_eq_zero
-  (map_ne_zero_of_mem_non_zero_divisors hg h) hz
-
-lemma le_non_zero_divisors_of_domain {M : submonoid A}
-  (hM : ↑0 ∉ M) : M ≤ non_zero_divisors A :=
-λ x hx y hy, or.rec_on (eq_zero_or_eq_zero_of_mul_eq_zero hy)
-  (λ h, h) (λ h, absurd (h ▸ hx : (0 : A) ∈ M) hM)
+lemma ring_hom.map_ne_zero_of_mem_non_zero_divisors {R R' : Type*} [semiring R] [semiring R']
+  [nontrivial R]
+  (g : R →+* R') (hg : function.injective g)
+  {x : R} (h : x ∈ non_zero_divisors R) : g x ≠ 0 :=
+g.to_monoid_with_zero_hom.map_ne_zero_of_mem_non_zero_divisors hg h
 
-lemma powers_le_non_zero_divisors_of_domain {a : A} (ha : a ≠ 0) :
-  submonoid.powers a ≤ non_zero_divisors A :=
-le_non_zero_divisors_of_domain (λ h, absurd (h.rec_on (λ _ hn, pow_eq_zero hn)) ha)
+lemma monoid_with_zero_hom.map_mem_non_zero_divisors [nontrivial M] [no_zero_divisors M']
+  (g : monoid_with_zero_hom M M') (hg : function.injective g)
+  {x : M} (h : x ∈ non_zero_divisors M) : g x ∈ non_zero_divisors M' :=
+λ z hz, eq_zero_of_ne_zero_of_mul_right_eq_zero
+  (g.map_ne_zero_of_mem_non_zero_divisors hg h) hz
 
-lemma map_le_non_zero_divisors_of_injective {B : Type*} [integral_domain B]
-  {f : A →+* B} (hf : function.injective f)
-  {M : submonoid A} (hM : M ≤ non_zero_divisors A) : M.map ↑f ≤ non_zero_divisors B :=
-le_non_zero_divisors_of_domain (λ h, let ⟨x, hx, hx0⟩ := h in
-  zero_ne_one (hM (hf (trans hx0 (f.map_zero.symm)) ▸ hx : 0 ∈ M) 1 (mul_zero 1)).symm)
+lemma ring_hom.map_mem_non_zero_divisors {R R' : Type*} [semiring R] [semiring R']
+  [nontrivial R] [no_zero_divisors R']
+  (g : R →+* R') (hg : function.injective g)
+  {x : R} (h : x ∈ non_zero_divisors R) : g x ∈ non_zero_divisors R' :=
+g.to_monoid_with_zero_hom.map_mem_non_zero_divisors hg h
 
-lemma prod_zero_iff_exists_zero {R : Type*} [comm_semiring R] [no_zero_divisors R] [nontrivial R]
-  {s : multiset R} : s.prod = 0 ↔ ∃ (r : R) (hr : r ∈ s), r = 0 :=
+lemma le_non_zero_divisors_of_no_zero_divisors [no_zero_divisors M] {S : submonoid M}
+  (hS : (0 : M) ∉ S) : S ≤ non_zero_divisors M :=
+λ x hx y hy, or.rec_on (eq_zero_or_eq_zero_of_mul_eq_zero hy)
+  (λ h, h) (λ h, absurd (h ▸ hx : (0 : M) ∈ S) hS)
+
+lemma powers_le_non_zero_divisors_of_no_zero_divisors [no_zero_divisors M]
+  {a : M} (ha : a ≠ 0) : submonoid.powers a ≤ non_zero_divisors M :=
+le_non_zero_divisors_of_no_zero_divisors (λ h, absurd (h.rec_on (λ _ hn, pow_eq_zero hn)) ha)
+
+lemma monoid_with_zero_hom.map_le_non_zero_divisors_of_injective
+  [nontrivial M] [no_zero_divisors M']
+  (f : monoid_with_zero_hom M M') (hf : function.injective f)
+  {S : submonoid M} (hS : S ≤ non_zero_divisors M) : S.map ↑f ≤ non_zero_divisors M' :=
+le_non_zero_divisors_of_no_zero_divisors (λ h, let ⟨x, hx, hx0⟩ := h in
+  zero_ne_one (hS (hf (trans hx0 (f.map_zero.symm)) ▸ hx : 0 ∈ S) 1 (mul_zero 1)).symm)
+
+lemma ring_hom.map_le_non_zero_divisors_of_injective {R R' : Type*} [semiring R] [semiring R']
+  [nontrivial R] [no_zero_divisors R']
+  (f : R →+* R') (hf : function.injective f)
+  {S : submonoid R} (hS : S ≤ non_zero_divisors R) : S.map ↑f ≤ non_zero_divisors R' :=
+f.to_monoid_with_zero_hom.map_le_non_zero_divisors_of_injective hf hS
+
+lemma prod_zero_iff_exists_zero [no_zero_divisors M₁] [nontrivial M₁]
+  {s : multiset M₁} : s.prod = 0 ↔ ∃ (r : M₁) (hr : r ∈ s), r = 0 :=
 begin
   split, swap,
   { rintros ⟨r, hrs, rfl⟩,
@@ -92,5 +116,4 @@ begin
       exact ⟨multiset.mem_cons_of_mem hb₁, hb₂⟩, }, },
 end
 
-
 end non_zero_divisors

src/ring_theory/polynomial/scale_roots.lean

@@ -117,7 +117,7 @@ lemma scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero
 begin
   convert scale_roots_eval₂_eq_zero f hr,
   rw [←mul_div_assoc, mul_comm, mul_div_cancel],
-  exact map_ne_zero_of_mem_non_zero_divisors hf hs
+  exact f.map_ne_zero_of_mem_non_zero_divisors hf hs
 end
 
 lemma scale_roots_aeval_eq_zero_of_aeval_div_eq_zero [algebra A K]