feat(algebra/ring/basic): define non-unital commutative (semi)rings (#…

…13476)

This adds the classes of non-unital commutative (semi)rings. These are necessary to talk about, for example, non-unital commutative C∗-algebras such as `C₀(X, ℂ)` which are vital for the continuous functional calculus.

In addition, we weaken many type class assumptions in `algebra/ring/basic` to `non_unital_non_assoc_ring`.

src/algebra/monoid_algebra/basic.lean

@@ -207,21 +207,25 @@ def lift_nc_ring_hom (f : k →+* R) (g : G →* R) (h_comm : ∀ x y, commute (
 
 end semiring
 
-instance [comm_semiring k] [comm_monoid G] : comm_semiring (monoid_algebra k G) :=
+instance [comm_semiring k] [comm_semigroup G] : non_unital_comm_semiring (monoid_algebra k G) :=
 { mul_comm := assume f g,
   begin
     simp only [mul_def, finsupp.sum, mul_comm],
     rw [finset.sum_comm],
     simp only [mul_comm]
   end,
-  .. monoid_algebra.semiring }
+  .. monoid_algebra.non_unital_semiring }
 
 instance [semiring k] [nontrivial k] [nonempty G]: nontrivial (monoid_algebra k G) :=
 finsupp.nontrivial
 
 /-! #### Derived instances -/
 section derived_instances
 
+instance [comm_semiring k] [comm_monoid G] : comm_semiring (monoid_algebra k G) :=
+{ .. monoid_algebra.non_unital_comm_semiring,
+  .. monoid_algebra.semiring }
+
 instance [semiring k] [subsingleton k] : unique (monoid_algebra k G) :=
 finsupp.unique_of_right
 
@@ -244,8 +248,13 @@ instance [ring k] [monoid G] : ring (monoid_algebra k G) :=
 { .. monoid_algebra.non_unital_non_assoc_ring,
   .. monoid_algebra.semiring }
 
+instance [comm_ring k] [comm_semigroup G] : non_unital_comm_ring (monoid_algebra k G) :=
+{ .. monoid_algebra.non_unital_comm_semiring,
+  .. monoid_algebra.non_unital_ring }
+
 instance [comm_ring k] [comm_monoid G] : comm_ring (monoid_algebra k G) :=
-{ mul_comm := mul_comm, .. monoid_algebra.ring}
+{ .. monoid_algebra.non_unital_comm_ring,
+  .. monoid_algebra.ring }
 
 variables {S : Type*}
 
@@ -1041,16 +1050,21 @@ def lift_nc_ring_hom (f : k →+* R) (g : multiplicative G →* R)
 
 end semiring
 
-instance [comm_semiring k] [add_comm_monoid G] : comm_semiring (add_monoid_algebra k G) :=
+instance [comm_semiring k] [add_comm_semigroup G] :
+  non_unital_comm_semiring (add_monoid_algebra k G) :=
 { mul_comm := @mul_comm (monoid_algebra k $ multiplicative G) _,
-  .. add_monoid_algebra.semiring }
+  .. add_monoid_algebra.non_unital_semiring }
 
 instance [semiring k] [nontrivial k] [nonempty G] : nontrivial (add_monoid_algebra k G) :=
 finsupp.nontrivial
 
 /-! #### Derived instances -/
 section derived_instances
 
+instance [comm_semiring k] [add_comm_monoid G] : comm_semiring (add_monoid_algebra k G) :=
+{ .. add_monoid_algebra.non_unital_comm_semiring,
+  .. add_monoid_algebra.semiring }
+
 instance [semiring k] [subsingleton k] : unique (add_monoid_algebra k G) :=
 finsupp.unique_of_right
 
@@ -1073,8 +1087,13 @@ instance [ring k] [add_monoid G] : ring (add_monoid_algebra k G) :=
 { .. add_monoid_algebra.non_unital_non_assoc_ring,
   .. add_monoid_algebra.semiring }
 
+instance [comm_ring k] [add_comm_semigroup G] : non_unital_comm_ring (add_monoid_algebra k G) :=
+{ .. add_monoid_algebra.non_unital_comm_semiring,
+  .. add_monoid_algebra.non_unital_ring }
+
 instance [comm_ring k] [add_comm_monoid G] : comm_ring (add_monoid_algebra k G) :=
-{ mul_comm := mul_comm, .. add_monoid_algebra.ring}
+{ .. add_monoid_algebra.non_unital_comm_ring,
+  .. add_monoid_algebra.ring }
 
 variables {S : Type*}
 

src/algebra/order/ring.lean

@@ -101,11 +101,13 @@ instance [h : non_unital_non_assoc_semiring α] : non_unital_non_assoc_semiring
 instance [h : non_unital_semiring α] : non_unital_semiring (order_dual α) := h
 instance [h : non_assoc_semiring α] : non_assoc_semiring (order_dual α) := h
 instance [h : semiring α] : semiring (order_dual α) := h
+instance [h : non_unital_comm_semiring α] : non_unital_comm_semiring (order_dual α) := h
 instance [h : comm_semiring α] : comm_semiring (order_dual α) := h
 instance [h : non_unital_non_assoc_ring α] : non_unital_non_assoc_ring (order_dual α) := h
 instance [h : non_unital_ring α] : non_unital_ring (order_dual α) := h
 instance [h : non_assoc_ring α] : non_assoc_ring (order_dual α) := h
 instance [h : ring α] : ring (order_dual α) := h
+instance [h : non_unital_comm_ring α] : non_unital_comm_ring (order_dual α) := h
 instance [h : comm_ring α] : comm_ring (order_dual α) := h
 
 end order_dual

src/algebra/ring/basic.lean

@@ -817,13 +817,53 @@ lemma ring_hom.map_dvd [semiring β] (f : α →+* β) {a b : α} : a ∣ b →
 
 end semiring
 
+/-- A non-unital commutative semiring is a `non_unital_semiring` with commutative multiplication.
+In other words, it is a type with the following structures: additive commutative monoid
+(`add_comm_monoid`), commutative semigroup (`comm_semigroup`), distributive laws (`distrib`), and
+multiplication by zero law (`mul_zero_class`). -/
+@[protect_proj, ancestor non_unital_semiring comm_semigroup]
+class non_unital_comm_semiring (α : Type u) extends non_unital_semiring α, comm_semigroup α
+
+section non_unital_comm_semiring
+variables [non_unital_comm_semiring α] [non_unital_comm_semiring β] {a b c : α}
+
+/-- Pullback a `non_unital_semiring` instance along an injective function.
+See note [reducible non-instances]. -/
+@[reducible]
+protected def function.injective.non_unital_comm_semiring [has_zero γ] [has_add γ] [has_mul γ]
+  [has_scalar ℕ γ] (f : γ → α) (hf : injective f) (zero : f 0 = 0)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) :
+  non_unital_comm_semiring γ :=
+{ .. hf.non_unital_semiring f zero add mul nsmul, .. hf.comm_semigroup f mul }
+
+/-- Pushforward a `non_unital_semiring` instance along a surjective function.
+See note [reducible non-instances]. -/
+@[reducible]
+protected def function.surjective.non_unital_comm_semiring [has_zero γ] [has_add γ] [has_mul γ]
+  [has_scalar ℕ γ] (f : α → γ) (hf : surjective f) (zero : f 0 = 0)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) :
+  non_unital_comm_semiring γ :=
+{ .. hf.non_unital_semiring f zero add mul nsmul, .. hf.comm_semigroup f mul }
+
+lemma has_dvd.dvd.linear_comb {d x y : α} (hdx : d ∣ x) (hdy : d ∣ y) (a b : α) :
+  d ∣ (a * x + b * y) :=
+dvd_add (hdx.mul_left a) (hdy.mul_left b)
+
+end non_unital_comm_semiring
+
 /-- A commutative semiring is a `semiring` with commutative multiplication. In other words, it is a
 type with the following structures: additive commutative monoid (`add_comm_monoid`), multiplicative
 commutative monoid (`comm_monoid`), distributive laws (`distrib`), and multiplication by zero law
 (`mul_zero_class`). -/
 @[protect_proj, ancestor semiring comm_monoid]
 class comm_semiring (α : Type u) extends semiring α, comm_monoid α
 
+@[priority 100] -- see Note [lower instance priority]
+instance comm_semiring.to_non_unital_comm_semiring [comm_semiring α] : non_unital_comm_semiring α :=
+{ .. comm_semiring.to_comm_monoid α, .. comm_semiring.to_semiring α }
+
 @[priority 100] -- see Note [lower instance priority]
 instance comm_semiring.to_comm_monoid_with_zero [comm_semiring α] : comm_monoid_with_zero α :=
 { .. comm_semiring.to_comm_monoid α, .. comm_semiring.to_semiring α }
@@ -854,10 +894,6 @@ protected def function.surjective.comm_semiring [has_zero γ] [has_one γ] [has_
 lemma add_mul_self_eq (a b : α) : (a + b) * (a + b) = a*a + 2*a*b + b*b :=
 by simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]
 
-lemma has_dvd.dvd.linear_comb {d x y : α} (hdx : d ∣ x) (hdy : d ∣ y) (a b : α) :
-  d ∣ (a * x + b * y) :=
-dvd_add (hdx.mul_left a) (hdy.mul_left b)
-
 end comm_semiring
 
 section has_distrib_neg
@@ -1236,6 +1272,15 @@ def mk' {γ} [non_assoc_semiring α] [non_assoc_ring γ] (f : α →* γ)
 
 end ring_hom
 
+/-- A non-unital commutative ring is a `non_unital_ring` with commutative multiplication. -/
+@[protect_proj, ancestor non_unital_ring comm_semigroup]
+class non_unital_comm_ring (α : Type u) extends non_unital_ring α, comm_semigroup α
+
+@[priority 100] -- see Note [lower instance priority]
+instance non_unital_comm_ring.to_non_unital_comm_semiring [s : non_unital_comm_ring α] :
+  non_unital_comm_semiring α :=
+{ ..s }
+
 /-- A commutative ring is a `ring` with commutative multiplication. -/
 @[protect_proj, ancestor ring comm_semigroup]
 class comm_ring (α : Type u) extends ring α, comm_monoid α
@@ -1244,8 +1289,12 @@ class comm_ring (α : Type u) extends ring α, comm_monoid α
 instance comm_ring.to_comm_semiring [s : comm_ring α] : comm_semiring α :=
 { mul_zero := mul_zero, zero_mul := zero_mul, ..s }
 
-section ring
-variables [ring α] {a b c : α}
+@[priority 100] -- see Note [lower instance priority]
+instance comm_ring.to_non_unital_comm_ring [s : comm_ring α] : non_unital_comm_ring α :=
+{ mul_zero := mul_zero, zero_mul := zero_mul, ..s }
+
+section non_unital_ring
+variables [non_unital_ring α] {a b c : α}
 
 theorem dvd_sub (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b - c :=
 by { rw sub_eq_add_neg, exact dvd_add h₁ (dvd_neg_of_dvd h₂) }
@@ -1256,8 +1305,6 @@ theorem dvd_add_iff_left (h : a ∣ c) : a ∣ b ↔ a ∣ b + c :=
 theorem dvd_add_iff_right (h : a ∣ b) : a ∣ c ↔ a ∣ b + c :=
 by rw add_comm; exact dvd_add_iff_left h
 
-theorem two_dvd_bit1 : 2 ∣ bit1 a ↔ (2 : α) ∣ 1 := (dvd_add_iff_right (@two_dvd_bit0 _ _ a)).symm
-
 /-- If an element a divides another element c in a commutative ring, a divides the sum of another
   element b with c iff a divides b. -/
 theorem dvd_add_left (h : a ∣ c) : a ∣ b + c ↔ a ∣ b :=
@@ -1268,14 +1315,6 @@ theorem dvd_add_left (h : a ∣ c) : a ∣ b + c ↔ a ∣ b :=
 theorem dvd_add_right (h : a ∣ b) : a ∣ b + c ↔ a ∣ c :=
 (dvd_add_iff_right h).symm
 
-/-- An element a divides the sum a + b if and only if a divides b.-/
-@[simp] lemma dvd_add_self_left {a b : α} : a ∣ a + b ↔ a ∣ b :=
-dvd_add_right (dvd_refl a)
-
-/-- An element a divides the sum b + a if and only if a divides b.-/
-@[simp] lemma dvd_add_self_right {a b : α} : a ∣ b + a ↔ a ∣ b :=
-dvd_add_left (dvd_refl a)
-
 lemma dvd_iff_dvd_of_dvd_sub {a b c : α} (h : a ∣ (b - c)) : (a ∣ b ↔ a ∣ c) :=
 begin
   split,
@@ -1287,38 +1326,51 @@ begin
     exact eq_add_of_sub_eq rfl }
 end
 
+end non_unital_ring
+
+section ring
+variables [ring α] {a b c : α}
+
+theorem two_dvd_bit1 : 2 ∣ bit1 a ↔ (2 : α) ∣ 1 := (dvd_add_iff_right (@two_dvd_bit0 _ _ a)).symm
+
+/-- An element a divides the sum a + b if and only if a divides b.-/
+@[simp] lemma dvd_add_self_left {a b : α} : a ∣ a + b ↔ a ∣ b :=
+dvd_add_right (dvd_refl a)
+
+/-- An element a divides the sum b + a if and only if a divides b.-/
+@[simp] lemma dvd_add_self_right {a b : α} : a ∣ b + a ↔ a ∣ b :=
+dvd_add_left (dvd_refl a)
+
 end ring
 
-section comm_ring
-variables [comm_ring α] {a b c : α}
+section non_unital_comm_ring
+variables [non_unital_comm_ring α] {a b c : α}
 
 /-- Pullback a `comm_ring` instance along an injective function.
 See note [reducible non-instances]. -/
 @[reducible]
-protected def function.injective.comm_ring
-  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
-  [has_scalar ℕ β] [has_scalar ℤ β] [has_pow β ℕ]
-  (f : β → α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
+protected def function.injective.non_unital_comm_ring
+  [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
+  [has_scalar ℕ β] [has_scalar ℤ β]
+  (f : β → α) (hf : injective f) (zero : f 0 = 0)
   (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
   (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
-  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x)
-  (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) :
-  comm_ring β :=
-{ .. hf.ring f zero one add mul neg sub nsmul zsmul npow, .. hf.comm_semigroup f mul }
+  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x) :
+  non_unital_comm_ring β :=
+{ .. hf.non_unital_ring f zero add mul neg sub nsmul zsmul, .. hf.comm_semigroup f mul }
 
-/-- Pushforward a `comm_ring` instance along a surjective function.
+/-- Pushforward a `non_unital_comm_ring` instance along a surjective function.
 See note [reducible non-instances]. -/
 @[reducible]
-protected def function.surjective.comm_ring
-  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
-  [has_scalar ℕ β] [has_scalar ℤ β] [has_pow β ℕ]
-  (f : α → β) (hf : surjective f) (zero : f 0 = 0) (one : f 1 = 1)
+protected def function.surjective.non_unital_comm_ring
+  [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
+  [has_scalar ℕ β] [has_scalar ℤ β]
+  (f : α → β) (hf : surjective f) (zero : f 0 = 0)
   (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
   (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
-  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x)
-  (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) :
-  comm_ring β :=
-{ .. hf.ring f zero one add mul neg sub nsmul zsmul npow, .. hf.comm_semigroup f mul }
+  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x) :
+  non_unital_comm_ring β :=
+{ .. hf.non_unital_ring f zero add mul neg sub nsmul zsmul, .. hf.comm_semigroup f mul }
 
 local attribute [simp] add_assoc add_comm add_left_comm mul_comm
 
@@ -1343,6 +1395,39 @@ begin
   simp only [sub_eq_add_neg, add_assoc, neg_add_cancel_left],
 end
 
+end non_unital_comm_ring
+
+section comm_ring
+variables [comm_ring α] {a b c : α}
+
+/-- Pullback a `comm_ring` instance along an injective function.
+See note [reducible non-instances]. -/
+@[reducible]
+protected def function.injective.comm_ring
+  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
+  [has_scalar ℕ β] [has_scalar ℤ β] [has_pow β ℕ]
+  (f : β → α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+  (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
+  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x)
+  (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) :
+  comm_ring β :=
+{ .. hf.ring f zero one add mul neg sub nsmul zsmul npow, .. hf.comm_semigroup f mul }
+
+/-- Pushforward a `comm_ring` instance along a surjective function.
+See note [reducible non-instances]. -/
+@[reducible]
+protected def function.surjective.comm_ring
+  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
+  [has_scalar ℕ β] [has_scalar ℤ β] [has_pow β ℕ]
+  (f : α → β) (hf : surjective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+  (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
+  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x)
+  (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) :
+  comm_ring β :=
+{ .. hf.ring f zero one add mul neg sub nsmul zsmul npow, .. hf.comm_semigroup f mul }
+
 end comm_ring
 
 lemma succ_ne_self [non_assoc_ring α] [nontrivial α] (a : α) : a + 1 ≠ a :=
@@ -1376,8 +1461,8 @@ lemma is_regular_of_ne_zero' [non_unital_non_assoc_ring α] [no_zero_divisors α
  is_right_regular_of_non_zero_divisor k
   (λ x h, (no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hk)⟩
 
-lemma is_regular_iff_ne_zero' [nontrivial α] [ring α] [no_zero_divisors α] {k : α} :
-  is_regular k ↔ k ≠ 0 :=
+lemma is_regular_iff_ne_zero' [nontrivial α] [non_unital_non_assoc_ring α] [no_zero_divisors α]
+  {k : α} : is_regular k ↔ k ≠ 0 :=
 ⟨λ h, by { rintro rfl, exact not_not.mpr h.left not_is_left_regular_zero }, is_regular_of_ne_zero'⟩
 
 /-- A ring with no zero divisors is a cancel_monoid_with_zero.

src/algebra/ring/boolean_ring.lean

@@ -270,17 +270,17 @@ iff.rfl
 
 instance [inhabited α] : inhabited (as_boolring α) := ‹inhabited α›
 
-/-- Every generalized Boolean algebra has the structure of a non unital ring with the following
-data:
+/-- Every generalized Boolean algebra has the structure of a non unital commutative ring with the
+following data:
 
 * `a + b` unfolds to `a ∆ b` (symmetric difference)
 * `a * b` unfolds to `a ⊓ b`
 * `-a` unfolds to `a`
 * `0` unfolds to `⊥`
 -/
 @[reducible] -- See note [reducible non-instances]
-def generalized_boolean_algebra.to_non_unital_ring [generalized_boolean_algebra α] :
-  non_unital_ring α :=
+def generalized_boolean_algebra.to_non_unital_comm_ring [generalized_boolean_algebra α] :
+  non_unital_comm_ring α :=
 { add := (∆),
   add_assoc := symm_diff_assoc,
   zero := ⊥,
@@ -293,11 +293,12 @@ def generalized_boolean_algebra.to_non_unital_ring [generalized_boolean_algebra
   add_comm := symm_diff_comm,
   mul := (⊓),
   mul_assoc := λ _ _ _, inf_assoc,
+  mul_comm := λ _ _, inf_comm,
   left_distrib := inf_symm_diff_distrib_left,
   right_distrib := inf_symm_diff_distrib_right }
 
-instance [generalized_boolean_algebra α] : non_unital_ring (as_boolring α) :=
-@generalized_boolean_algebra.to_non_unital_ring α _
+instance [generalized_boolean_algebra α] : non_unital_comm_ring (as_boolring α) :=
+@generalized_boolean_algebra.to_non_unital_comm_ring α _
 
 variables [boolean_algebra α] [boolean_algebra β] [boolean_algebra γ]
 
@@ -315,9 +316,9 @@ def boolean_algebra.to_boolean_ring : boolean_ring α :=
   one_mul := λ _, top_inf_eq,
   mul_one := λ _, inf_top_eq,
   mul_self := λ b, inf_idem,
-  ..generalized_boolean_algebra.to_non_unital_ring }
+  ..generalized_boolean_algebra.to_non_unital_comm_ring }
 
-localized "attribute [instance, priority 100] generalized_boolean_algebra.to_non_unital_ring
+localized "attribute [instance, priority 100] generalized_boolean_algebra.to_non_unital_comm_ring
   boolean_algebra.to_boolean_ring" in boolean_ring_of_boolean_algebra
 
 instance : boolean_ring (as_boolring α) := @boolean_algebra.to_boolean_ring α _