chore(algebra/ring/defs): refactor is_domain (#17721)

Refactor the definiton of `is_domain` to use `is_cancel_mul_zero` instead of `no_zero_divisors`. This is the correct property for a `semiring` (to do in a future refactor).

Corresponding mathlib4 PR leanprover-community/mathlib4#799.

- [x] depends on #17716

src/algebra/algebra/bilinear.lean

@@ -165,18 +165,27 @@ variables {R A : Type*} [comm_semiring R] [ring A] [algebra R A]
 
 lemma mul_left_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
   function.injective (mul_left R x) :=
-by { letI : is_domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
-     exact mul_right_injective₀ hx }
+begin
+  letI : nontrivial A := ⟨⟨x, 0, hx⟩⟩,
+  letI := no_zero_divisors.to_is_domain A,
+  exact mul_right_injective₀ hx,
+end
 
 lemma mul_right_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
   function.injective (mul_right R x) :=
-by { letI : is_domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
-     exact mul_left_injective₀ hx }
+begin
+  letI : nontrivial A := ⟨⟨x, 0, hx⟩⟩,
+  letI := no_zero_divisors.to_is_domain A,
+  exact mul_left_injective₀ hx,
+end
 
 lemma mul_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
   function.injective (mul R A x) :=
-by { letI : is_domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
-     exact mul_right_injective₀ hx }
+begin
+  letI : nontrivial A := ⟨⟨x, 0, hx⟩⟩,
+  letI := no_zero_divisors.to_is_domain A,
+  exact mul_right_injective₀ hx,
+end
 
 end ring
 

src/algebra/euclidean_domain/basic.lean

@@ -7,6 +7,7 @@ import algebra.euclidean_domain.defs
 import algebra.ring.divisibility
 import algebra.ring.regular
 import algebra.group_with_zero.divisibility
+import algebra.ring.basic
 
 /-!
 # Lemmas about Euclidean domains
@@ -171,12 +172,15 @@ by { have := @xgcd_aux_P _ _ _ a b a b 1 0 0 1
 rwa [xgcd_aux_val, xgcd_val] at this }
 
 @[priority 70] -- see Note [lower instance priority]
-instance (R : Type*) [e : euclidean_domain R] : is_domain R :=
+instance (R : Type*) [e : euclidean_domain R] : no_zero_divisors R :=
 by { haveI := classical.dec_eq R, exact
 { eq_zero_or_eq_zero_of_mul_eq_zero :=
     λ a b h, (or_iff_not_and_not.2 $ λ h0,
-      h0.1 $ by rw [← mul_div_cancel a h0.2, h, zero_div]),
-  ..e }}
+      h0.1 $ by rw [← mul_div_cancel a h0.2, h, zero_div]) }}
+
+@[priority 70] -- see Note [lower instance priority]
+instance (R : Type*) [e : euclidean_domain R] : is_domain R :=
+{ .. e, .. no_zero_divisors.to_is_domain R }
 
 end gcd
 

src/algebra/field/basic.lean

@@ -126,8 +126,7 @@ by rw [(mul_sub_left_distrib (1 / a)), (one_div_mul_cancel ha), mul_sub_right_di
 
 @[priority 100] -- see Note [lower instance priority]
 instance division_ring.is_domain : is_domain K :=
-{ ..‹division_ring K›,
-  ..(by apply_instance : no_zero_divisors K) }
+no_zero_divisors.to_is_domain _
 
 end division_ring
 

src/algebra/hom/ring.lean

@@ -528,9 +528,13 @@ end ring_hom
 
 /-- Pullback `is_domain` instance along an injective function. -/
 protected theorem function.injective.is_domain [ring α] [is_domain α] [ring β] (f : β →+* α)
-  (hf : injective f) :
-  is_domain β :=
-{ .. pullback_nonzero f f.map_zero f.map_one, .. hf.no_zero_divisors f f.map_zero f.map_mul }
+  (hf : injective f) : is_domain β :=
+begin
+  haveI := pullback_nonzero f f.map_zero f.map_one,
+  haveI := is_right_cancel_mul_zero.to_no_zero_divisors α,
+  haveI := hf.no_zero_divisors f f.map_zero f.map_mul,
+  exact no_zero_divisors.to_is_domain β,
+end
 
 namespace add_monoid_hom
 variables [comm_ring α] [is_domain α] [comm_ring β] (f : β →+ α)

src/algebra/order/ring/defs.lean

@@ -784,7 +784,7 @@ instance linear_ordered_ring.to_linear_ordered_add_comm_group : linear_ordered_a
 { ..‹linear_ordered_ring α› }
 
 @[priority 100] -- see Note [lower instance priority]
-instance linear_ordered_ring.is_domain : is_domain α :=
+instance linear_ordered_ring.no_zero_divisors : no_zero_divisors α :=
 { eq_zero_or_eq_zero_of_mul_eq_zero :=
     begin
       intros a b hab,
@@ -795,6 +795,21 @@ instance linear_ordered_ring.is_domain : is_domain α :=
     end,
   .. ‹linear_ordered_ring α› }
 
+@[priority 100] -- see Note [lower instance priority]
+--We don't want to import `algebra.ring.basic`, so we cannot use `no_zero_divisors.to_is_domain`.
+instance linear_ordered_ring.is_domain : is_domain α :=
+{ mul_left_cancel_of_ne_zero := λ a b c ha h,
+  begin
+    rw [← sub_eq_zero, ← mul_sub] at h,
+    exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_left ha)
+  end,
+  mul_right_cancel_of_ne_zero := λ a b c hb h,
+  begin
+    rw [← sub_eq_zero, ← sub_mul] at h,
+    exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hb)
+  end,
+  .. (infer_instance : nontrivial α) }
+
 lemma mul_pos_iff : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 :=
 ⟨pos_and_pos_or_neg_and_neg_of_mul_pos,
   λ h, h.elim (and_imp.2 mul_pos) (and_imp.2 mul_pos_of_neg_of_neg)⟩

src/algebra/quaternion.lean

@@ -572,12 +572,15 @@ by simpa only [le_antisymm_iff, norm_sq_nonneg, and_true] using @norm_sq_eq_zero
 instance : nontrivial ℍ[R] :=
 { exists_pair_ne := ⟨0, 1, mt (congr_arg re) zero_ne_one⟩, }
 
-instance : is_domain ℍ[R] :=
+instance : no_zero_divisors ℍ[R] :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ a b hab,
     have norm_sq a * norm_sq b = 0, by rwa [← norm_sq.map_mul, norm_sq_eq_zero],
     (eq_zero_or_eq_zero_of_mul_eq_zero this).imp norm_sq_eq_zero.1 norm_sq_eq_zero.1,
   ..quaternion.nontrivial, }
 
+instance : is_domain ℍ[R] :=
+no_zero_divisors.to_is_domain _
+
 end linear_ordered_comm_ring
 
 section field

src/algebra/ring/basic.lean

@@ -118,3 +118,55 @@ lemma succ_ne_self [non_assoc_ring α] [nontrivial α] (a : α) : a + 1 ≠ a :=
 
 lemma pred_ne_self [non_assoc_ring α] [nontrivial α] (a : α) : a - 1 ≠ a :=
 λ h, one_ne_zero (neg_injective ((add_right_inj a).mp (by simpa [sub_eq_add_neg] using h)))
+
+section no_zero_divisors
+
+variable (α)
+
+lemma is_left_cancel_mul_zero.to_no_zero_divisors [ring α] [is_left_cancel_mul_zero α] :
+  no_zero_divisors α :=
+begin
+  refine ⟨λ x y h, _⟩,
+  by_cases hx : x = 0,
+  { left, exact hx },
+  { right,
+    rw [← sub_zero (x * y), ← mul_zero x, ← mul_sub] at h,
+    convert (is_left_cancel_mul_zero.mul_left_cancel_of_ne_zero) hx h,
+    rw [sub_zero] }
+end
+
+lemma is_right_cancel_mul_zero.to_no_zero_divisors [ring α] [is_right_cancel_mul_zero α] :
+  no_zero_divisors α :=
+begin
+  refine ⟨λ x y h, _⟩,
+  by_cases hy : y = 0,
+  { right, exact hy },
+  { left,
+    rw [← sub_zero (x * y), ← zero_mul y, ← sub_mul] at h,
+    convert (is_right_cancel_mul_zero.mul_right_cancel_of_ne_zero) hy h,
+    rw [sub_zero] }
+end
+
+@[priority 100]
+instance no_zero_divisors.to_is_cancel_mul_zero [ring α] [no_zero_divisors α] :
+  is_cancel_mul_zero α :=
+{ mul_left_cancel_of_ne_zero := λ a b c ha h,
+  begin
+    rw [← sub_eq_zero, ← mul_sub] at h,
+    exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_left ha)
+  end,
+  mul_right_cancel_of_ne_zero := λ a b c hb h,
+  begin
+    rw [← sub_eq_zero, ← sub_mul] at h,
+    exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hb)
+  end }
+
+lemma no_zero_divisors.to_is_domain [ring α] [h : nontrivial α] [no_zero_divisors α] :
+  is_domain α :=
+{ .. no_zero_divisors.to_is_cancel_mul_zero α, .. h }
+
+@[priority 100]
+instance is_domain.to_no_zero_divisors [ring α] [is_domain α] : no_zero_divisors α :=
+is_right_cancel_mul_zero.to_no_zero_divisors α
+
+end no_zero_divisors

src/algebra/ring/defs.lean

@@ -413,10 +413,12 @@ instance comm_ring.to_comm_semiring [s : comm_ring α] : comm_semiring α :=
 instance comm_ring.to_non_unital_comm_ring [s : comm_ring α] : non_unital_comm_ring α :=
 { mul_zero := mul_zero, zero_mul := zero_mul, ..s }
 
-/-- A domain is a nontrivial ring with no zero divisors, i.e. satisfying
-  the condition `a * b = 0 ↔ a = 0 ∨ b = 0`.
+/-- A domain is a nontrivial ring such multiplication by a non zero element is cancellative,
+  on both sides. In other words, a nontrivial ring `R` satisfying
+  `∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c` and
+  `∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c`.
 
   This is implemented as a mixin for `ring α`.
   To obtain an integral domain use `[comm_ring α] [is_domain α]`. -/
-@[protect_proj, ancestor no_zero_divisors nontrivial]
-class is_domain (α : Type u) [ring α] extends no_zero_divisors α, nontrivial α : Prop
+@[protect_proj, ancestor is_cancel_mul_zero nontrivial]
+class is_domain (α : Type u) [ring α] extends is_cancel_mul_zero α, nontrivial α : Prop

src/algebra/ring/equiv.lean

@@ -601,14 +601,24 @@ variables [has_add R] [has_add S] [has_mul R] [has_mul S]
 @[simp] theorem self_trans_symm (e : R ≃+* S) : e.trans e.symm = ring_equiv.refl R := ext e.3
 @[simp] theorem symm_trans_self (e : R ≃+* S) : e.symm.trans e = ring_equiv.refl S := ext e.4
 
+/-- If two rings are isomorphic, and the second doesn't have zero divisors,
+then so does the first. -/
+protected lemma no_zero_divisors
+  {A : Type*} (B : Type*) [ring A] [ring B] [no_zero_divisors B]
+  (e : A ≃+* B) : no_zero_divisors A :=
+{ eq_zero_or_eq_zero_of_mul_eq_zero := λ x y hxy,
+    have e x * e y = 0, by rw [← e.map_mul, hxy, e.map_zero],
+    by simpa using eq_zero_or_eq_zero_of_mul_eq_zero this }
+
 /-- If two rings are isomorphic, and the second is a domain, then so is the first. -/
 protected lemma is_domain
   {A : Type*} (B : Type*) [ring A] [ring B] [is_domain B]
   (e : A ≃+* B) : is_domain A :=
-{ eq_zero_or_eq_zero_of_mul_eq_zero := λ x y hxy,
-    have e x * e y = 0, by rw [← e.map_mul, hxy, e.map_zero],
-    by simpa using eq_zero_or_eq_zero_of_mul_eq_zero this,
-  exists_pair_ne := ⟨e.symm 0, e.symm 1, e.symm.injective.ne zero_ne_one⟩ }
+begin
+  haveI : nontrivial A := ⟨⟨e.symm 0, e.symm 1, e.symm.injective.ne zero_ne_one⟩⟩,
+  haveI := e.no_zero_divisors B,
+  exact no_zero_divisors.to_is_domain _
+end
 
 end ring_equiv
 

src/algebra/ring/opposite.lean

@@ -81,7 +81,7 @@ instance [has_zero α] [has_mul α] [no_zero_divisors α] : no_zero_divisors α
       (λ hy, or.inr $ unop_injective $ hy) (λ hx, or.inl $ unop_injective $ hx), }
 
 instance [ring α] [is_domain α] : is_domain αᵐᵒᵖ :=
-{ .. mul_opposite.no_zero_divisors α, .. mul_opposite.ring α, .. mul_opposite.nontrivial α }
+no_zero_divisors.to_is_domain _
 
 instance [group_with_zero α] : group_with_zero αᵐᵒᵖ :=
 { mul_inv_cancel := λ x hx, unop_injective $ inv_mul_cancel $ unop_injective.ne hx,
@@ -157,7 +157,7 @@ instance [has_zero α] [has_mul α] [no_zero_divisors α] : no_zero_divisors α
   ((@eq_zero_or_eq_zero_of_mul_eq_zero α _ _ _ _ _) $ op_injective H) }
 
 instance [ring α] [is_domain α] : is_domain αᵃᵒᵖ :=
-{ .. add_opposite.no_zero_divisors α, .. add_opposite.ring α, .. add_opposite.nontrivial α }
+no_zero_divisors.to_is_domain _
 
 instance [group_with_zero α] : group_with_zero αᵃᵒᵖ :=
 { mul_inv_cancel := λ x hx, unop_injective $ mul_inv_cancel $ unop_injective.ne hx,

src/algebra/ring/prod.lean

@@ -252,7 +252,7 @@ end ring_equiv
 lemma false_of_nontrivial_of_product_domain (R S : Type*) [ring R] [ring S]
   [is_domain (R × S)] [nontrivial R] [nontrivial S] : false :=
 begin
-  have := is_domain.eq_zero_or_eq_zero_of_mul_eq_zero
+  have := no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero
     (show ((0 : R), (1 : S)) * (1, 0) = 0, by simp),
   rw [prod.mk_eq_zero,prod.mk_eq_zero] at this,
   rcases this with (⟨_,h⟩|⟨h,_⟩),

src/algebra/ring/regular.lean

@@ -70,7 +70,11 @@ section is_domain
 
 @[priority 100] -- see Note [lower instance priority]
 instance is_domain.to_cancel_monoid_with_zero [ring α] [is_domain α] : cancel_monoid_with_zero α :=
-no_zero_divisors.to_cancel_monoid_with_zero
+{ mul_left_cancel_of_ne_zero := λ a b c ha h,
+    is_cancel_mul_zero.mul_left_cancel_of_ne_zero ha h,
+  mul_right_cancel_of_ne_zero := λ a b c ha h,
+    is_cancel_mul_zero.mul_right_cancel_of_ne_zero ha h,
+  .. semiring.to_monoid_with_zero α }
 
 variables [comm_ring α] [is_domain α]
 

src/algebraic_geometry/properties.lean

@@ -267,20 +267,23 @@ end
 lemma is_integral_of_is_irreducible_is_reduced [is_reduced X] [H : irreducible_space X.carrier] :
   is_integral X :=
 begin
-  split, refine λ U hU, ⟨λ a b e, _,
-    (@@LocallyRingedSpace.component_nontrivial X.to_LocallyRingedSpace U hU).1⟩,
-  simp_rw [← basic_open_eq_bot_iff, ← opens.not_nonempty_iff_eq_bot],
-  by_contra' h,
-  obtain ⟨_, ⟨x, hx₁, rfl⟩, ⟨x, hx₂, e'⟩⟩ := @@nonempty_preirreducible_inter _ H.1
-    (X.basic_open a).2 (X.basic_open b).2
-    h.1 h.2,
-  replace e' := subtype.eq e',
-  subst e',
-  replace e := congr_arg (X.presheaf.germ x) e,
-  rw [ring_hom.map_mul, ring_hom.map_zero] at e,
-  refine zero_ne_one' (X.presheaf.stalk x.1) (is_unit_zero_iff.1 _),
-  convert hx₁.mul hx₂,
-  exact e.symm
+  split, intros U hU,
+  haveI := (@@LocallyRingedSpace.component_nontrivial X.to_LocallyRingedSpace U hU).1,
+  haveI : no_zero_divisors
+    (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (op U)),
+  { refine ⟨λ a b e, _⟩,
+    simp_rw [← basic_open_eq_bot_iff, ← opens.not_nonempty_iff_eq_bot],
+    by_contra' h,
+    obtain ⟨_, ⟨x, hx₁, rfl⟩, ⟨x, hx₂, e'⟩⟩ := @@nonempty_preirreducible_inter _ H.1
+      (X.basic_open a).2 (X.basic_open b).2 h.1 h.2,
+    replace e' := subtype.eq e',
+    subst e',
+    replace e := congr_arg (X.presheaf.germ x) e,
+    rw [ring_hom.map_mul, ring_hom.map_zero] at e,
+    refine zero_ne_one' (X.presheaf.stalk x.1) (is_unit_zero_iff.1 _),
+    convert hx₁.mul hx₂,
+    exact e.symm },
+  exact no_zero_divisors.to_is_domain _
 end
 
 lemma is_integral_iff_is_irreducible_and_is_reduced :

src/data/polynomial/ring_division.lean

@@ -250,8 +250,7 @@ section ring
 variables [ring R] [is_domain R] {p q : R[X]}
 
 instance : is_domain R[X] :=
-{ ..polynomial.no_zero_divisors,
-  ..polynomial.nontrivial, }
+no_zero_divisors.to_is_domain _
 
 end ring
 

src/data/rat/defs.lean

@@ -436,8 +436,7 @@ instance : comm_group_with_zero ℚ :=
   .. rat.comm_ring }
 
 instance : is_domain ℚ :=
-{ .. rat.comm_group_with_zero,
-  .. (infer_instance : no_zero_divisors ℚ) }
+no_zero_divisors.to_is_domain _
 
 /- Extra instances to short-circuit type class resolution -/
 -- TODO(Mario): this instance slows down data.real.basic

src/number_theory/zsqrtd/basic.lean

@@ -696,9 +696,11 @@ protected theorem eq_zero_or_eq_zero_of_mul_eq_zero : Π {a b : ℤ√d}, a * b
        x * x * z = d * -y * (x * w) : by simp [h1, mul_assoc, mul_left_comm]
              ... = d * y * y * z : by simp [h2, mul_assoc, mul_left_comm]
 
+instance : no_zero_divisors ℤ√d :=
+{ eq_zero_or_eq_zero_of_mul_eq_zero := @zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero }
+
 instance : is_domain ℤ√d :=
-{ eq_zero_or_eq_zero_of_mul_eq_zero := @zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero,
-  .. zsqrtd.comm_ring, .. zsqrtd.nontrivial }
+by exact no_zero_divisors.to_is_domain _
 
 protected theorem mul_pos (a b : ℤ√d) (a0 : 0 < a) (b0 : 0 < b) : 0 < a * b := λab,
 or.elim (eq_zero_or_eq_zero_of_mul_eq_zero

src/ring_theory/hahn_series.lean

@@ -783,9 +783,7 @@ instance {Γ} [linear_ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_s
 
 instance {Γ} [linear_ordered_cancel_add_comm_monoid Γ] [ring R] [is_domain R] :
   is_domain (hahn_series Γ R) :=
-{ .. hahn_series.no_zero_divisors,
-  .. hahn_series.nontrivial,
-  .. hahn_series.ring }
+no_zero_divisors.to_is_domain _
 
 @[simp]
 lemma order_mul {Γ} [linear_ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_semiring R]

src/ring_theory/ideal/quotient.lean

@@ -137,18 +137,25 @@ begin
            ⟨a, ha, by rw [← eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi⟩⟩
 end
 
-instance is_domain (I : ideal R) [hI : I.is_prime] : is_domain (R ⧸ I) :=
+instance no_zero_divisors (I : ideal R) [hI : I.is_prime] : no_zero_divisors (R ⧸ I) :=
 { 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.nontrivial hI.1 }
+        (or.inr ∘ eq_zero_iff_mem.2) }
+
+instance is_domain (I : ideal R) [hI : I.is_prime] : is_domain (R ⧸ I) :=
+let _ := quotient.nontrivial hI.1 in by exactI no_zero_divisors.to_is_domain _
 
 lemma is_domain_iff_prime (I : ideal R) : is_domain (R ⧸ I) ↔ I.is_prime :=
-⟨ λ ⟨h1, h2⟩, by { haveI : nontrivial _ := ⟨h2⟩, exact ⟨zero_ne_one_iff.1 zero_ne_one, λ x y h,
-    by { simp only [←eq_zero_iff_mem, (mk I).map_mul] at ⊢ h, exact h1 h}⟩ },
-  λ h, by { resetI, apply_instance }⟩
+begin
+  refine ⟨λ H, ⟨zero_ne_one_iff.1 _, λ x y h, _⟩, λ h, by { resetI, apply_instance }⟩,
+  { haveI : nontrivial (R ⧸ I) := ⟨H.3⟩,
+    exact zero_ne_one },
+  { simp only [←eq_zero_iff_mem, (mk I).map_mul] at ⊢ h,
+    haveI := @is_domain.to_no_zero_divisors (R ⧸ I) _ H,
+    exact eq_zero_or_eq_zero_of_mul_eq_zero h }
+end
 
 lemma exists_inv {I : ideal R} [hI : I.is_maximal] :
   ∀ {a : (R ⧸ I)}, a ≠ 0 → ∃ b : (R ⧸ I), a * b = 1 :=