From 4de6527854ef9868a2309b0c7e30885f4d9704e4 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Tue, 26 Apr 2022 02:57:32 +0000 Subject: [PATCH] feat(algebra/ring/basic): define non-unital commutative (semi)rings (#13476) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 31 +++- src/algebra/order/ring.lean | 2 + src/algebra/ring/basic.lean | 159 ++++++++++++++---- src/algebra/ring/boolean_ring.lean | 17 +- src/algebra/ring/equiv.lean | 8 +- src/algebra/ring/opposite.lean | 12 ++ src/algebra/ring/pi.lean | 11 ++ src/algebra/ring/prod.lean | 9 + src/algebra/ring/ulift.lean | 10 ++ src/data/finsupp/pointwise.lean | 7 + src/data/set/pointwise.lean | 4 + src/logic/equiv/transfer_instance.lean | 11 ++ src/ring_theory/hahn_series.lean | 10 +- .../continuous_function/zero_at_infty.lean | 9 + src/topology/locally_constant/algebra.lean | 6 + 15 files changed, 250 insertions(+), 56 deletions(-) diff --git a/src/algebra/monoid_algebra/basic.lean b/src/algebra/monoid_algebra/basic.lean index c16ba8b5eca88..f66f0c170473e 100644 --- a/src/algebra/monoid_algebra/basic.lean +++ b/src/algebra/monoid_algebra/basic.lean @@ -207,14 +207,14 @@ 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 @@ -222,6 +222,10 @@ 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,9 +1050,10 @@ 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 @@ -1051,6 +1061,10 @@ 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*} diff --git a/src/algebra/order/ring.lean b/src/algebra/order/ring.lean index 29c0e3ca1fe2c..fef4937123adf 100644 --- a/src/algebra/order/ring.lean +++ b/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 diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean index 5d9b8db4d1854..efefecdf77c51 100644 --- a/src/algebra/ring/basic.lean +++ b/src/algebra/ring/basic.lean @@ -817,6 +817,42 @@ 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 @@ -824,6 +860,10 @@ commutative monoid (`comm_monoid`), distributive laws (`distrib`), and multiplic @[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. diff --git a/src/algebra/ring/boolean_ring.lean b/src/algebra/ring/boolean_ring.lean index 6f9b16445b0ca..3851071263fab 100644 --- a/src/algebra/ring/boolean_ring.lean +++ b/src/algebra/ring/boolean_ring.lean @@ -270,8 +270,8 @@ 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` @@ -279,8 +279,8 @@ data: * `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 α _ diff --git a/src/algebra/ring/equiv.lean b/src/algebra/ring/equiv.lean index 7c0e8d355380d..ab12a7833c75f 100644 --- a/src/algebra/ring/equiv.lean +++ b/src/algebra/ring/equiv.lean @@ -228,11 +228,11 @@ protected def op {α β} [has_add α] [has_mul α] [has_add β] [has_mul β] : @[simp] protected def unop {α β} [has_add α] [has_mul α] [has_add β] [has_mul β] : (αᵐᵒᵖ ≃+* βᵐᵒᵖ) ≃ (α ≃+* β) := ring_equiv.op.symm -section comm_semiring +section non_unital_comm_semiring -variables (R) [comm_semiring R] +variables (R) [non_unital_comm_semiring R] -/-- A commutative ring is isomorphic to its opposite. -/ +/-- A non-unital commutative ring is isomorphic to its opposite. -/ def to_opposite : R ≃+* Rᵐᵒᵖ := { map_add' := λ x y, rfl, map_mul' := λ x y, mul_comm (op y) (op x), @@ -244,7 +244,7 @@ lemma to_opposite_apply (r : R) : to_opposite R r = op r := rfl @[simp] lemma to_opposite_symm_apply (r : Rᵐᵒᵖ) : (to_opposite R).symm r = unop r := rfl -end comm_semiring +end non_unital_comm_semiring end opposite diff --git a/src/algebra/ring/opposite.lean b/src/algebra/ring/opposite.lean index 05e9e683397ac..8497108915589 100644 --- a/src/algebra/ring/opposite.lean +++ b/src/algebra/ring/opposite.lean @@ -47,6 +47,9 @@ instance [semiring α] : semiring αᵐᵒᵖ := { .. mul_opposite.non_unital_semiring α, .. mul_opposite.non_assoc_semiring α, .. mul_opposite.monoid_with_zero α } +instance [non_unital_comm_semiring α] : non_unital_comm_semiring αᵐᵒᵖ := +{ .. mul_opposite.non_unital_semiring α, .. mul_opposite.comm_semigroup α } + instance [comm_semiring α] : comm_semiring αᵐᵒᵖ := { .. mul_opposite.semiring α, .. mul_opposite.comm_semigroup α } @@ -63,6 +66,9 @@ instance [non_assoc_ring α] : non_assoc_ring αᵐᵒᵖ := instance [ring α] : ring αᵐᵒᵖ := { .. mul_opposite.add_comm_group α, .. mul_opposite.monoid α, .. mul_opposite.semiring α } +instance [non_unital_comm_ring α] : non_unital_comm_ring αᵐᵒᵖ := +{ .. mul_opposite.non_unital_ring α, .. mul_opposite.non_unital_comm_semiring α } + instance [comm_ring α] : comm_ring αᵐᵒᵖ := { .. mul_opposite.ring α, .. mul_opposite.comm_semiring α } @@ -117,6 +123,9 @@ instance [semiring α] : semiring αᵃᵒᵖ := { .. add_opposite.non_unital_semiring α, .. add_opposite.non_assoc_semiring α, .. add_opposite.monoid_with_zero α } +instance [non_unital_comm_semiring α] : non_unital_comm_semiring αᵃᵒᵖ := +{ .. add_opposite.non_unital_semiring α, .. add_opposite.comm_semigroup α } + instance [comm_semiring α] : comm_semiring αᵃᵒᵖ := { .. add_opposite.semiring α, .. add_opposite.comm_semigroup α } @@ -133,6 +142,9 @@ instance [non_assoc_ring α] : non_assoc_ring αᵃᵒᵖ := instance [ring α] : ring αᵃᵒᵖ := { .. add_opposite.add_comm_group α, .. add_opposite.monoid α, .. add_opposite.semiring α } +instance [non_unital_comm_ring α] : non_unital_comm_ring αᵃᵒᵖ := +{ .. add_opposite.non_unital_ring α, .. add_opposite.non_unital_comm_semiring α } + instance [comm_ring α] : comm_ring αᵃᵒᵖ := { .. add_opposite.ring α, .. add_opposite.comm_semiring α } diff --git a/src/algebra/ring/pi.lean b/src/algebra/ring/pi.lean index 33af3ec66d4b0..7b0ff31115171 100644 --- a/src/algebra/ring/pi.lean +++ b/src/algebra/ring/pi.lean @@ -42,6 +42,11 @@ by refine_struct { zero := (0 : Π i, f i), one := 1, add := (+), mul := (*), nsmul := add_monoid.nsmul, npow := monoid.npow }; tactic.pi_instance_derive_field +instance non_unital_comm_semiring [∀ i, non_unital_comm_semiring $ f i] : + non_unital_comm_semiring (Π i : I, f i) := +by refine_struct { zero := (0 : Π i, f i), add := (+), mul := (*), nsmul := add_monoid.nsmul }; +tactic.pi_instance_derive_field + instance comm_semiring [∀ i, comm_semiring $ f i] : comm_semiring (Π i : I, f i) := by refine_struct { zero := (0 : Π i, f i), one := 1, add := (+), mul := (*), nsmul := add_monoid.nsmul, npow := monoid.npow }; @@ -71,6 +76,12 @@ by refine_struct { zero := (0 : Π i, f i), one := 1, add := (+), mul := (*), npow := monoid.npow }; tactic.pi_instance_derive_field +instance non_unital_comm_ring [∀ i, non_unital_comm_ring $ f i] : + non_unital_comm_ring (Π i : I, f i) := +by refine_struct { zero := (0 : Π i, f i), add := (+), mul := (*), neg := has_neg.neg, + nsmul := add_monoid.nsmul, zsmul := sub_neg_monoid.zsmul }; +tactic.pi_instance_derive_field + instance comm_ring [∀ i, comm_ring $ f i] : comm_ring (Π i : I, f i) := by refine_struct { zero := (0 : Π i, f i), one := 1, add := (+), mul := (*), neg := has_neg.neg, nsmul := add_monoid.nsmul, zsmul := sub_neg_monoid.zsmul, diff --git a/src/algebra/ring/prod.lean b/src/algebra/ring/prod.lean index 472ecee75591b..e3b5c9b826518 100644 --- a/src/algebra/ring/prod.lean +++ b/src/algebra/ring/prod.lean @@ -49,6 +49,11 @@ instance [non_assoc_semiring R] [non_assoc_semiring S] : instance [semiring R] [semiring S] : semiring (R × S) := { .. prod.add_comm_monoid, .. prod.monoid_with_zero, .. prod.distrib } +/-- Product of two `non_unital_comm_semiring`s is a `non_unital_comm_semiring`. -/ +instance [non_unital_comm_semiring R] [non_unital_comm_semiring S] : + non_unital_comm_semiring (R × S) := +{ .. prod.non_unital_semiring, .. prod.comm_semigroup } + /-- Product of two commutative semirings is a commutative semiring. -/ instance [comm_semiring R] [comm_semiring S] : comm_semiring (R × S) := { .. prod.semiring, .. prod.comm_monoid } @@ -69,6 +74,10 @@ instance [non_assoc_ring R] [non_assoc_ring S] : instance [ring R] [ring S] : ring (R × S) := { .. prod.add_comm_group, .. prod.semiring } +/-- Product of two `non_unital_comm_ring`s is a `non_unital_comm_ring`. -/ +instance [non_unital_comm_ring R] [non_unital_comm_ring S] : non_unital_comm_ring (R × S) := +{ .. prod.non_unital_ring, .. prod.comm_semigroup } + /-- Product of two commutative rings is a commutative ring. -/ instance [comm_ring R] [comm_ring S] : comm_ring (R × S) := { .. prod.ring, .. prod.comm_monoid } diff --git a/src/algebra/ring/ulift.lean b/src/algebra/ring/ulift.lean index 7037131e5a7ce..d09849d02ccc1 100644 --- a/src/algebra/ring/ulift.lean +++ b/src/algebra/ring/ulift.lean @@ -59,6 +59,11 @@ def ring_equiv [non_unital_non_assoc_semiring α] : ulift α ≃+* α := left_inv := by tidy, right_inv := by tidy, } +instance non_unital_comm_semiring [non_unital_comm_semiring α] : + non_unital_comm_semiring (ulift α) := +by refine_struct { zero := (0 : ulift α), add := (+), mul := (*), nsmul := add_monoid.nsmul }; +tactic.pi_instance_derive_field + instance comm_semiring [comm_semiring α] : comm_semiring (ulift α) := by refine_struct { zero := (0 : ulift α), one := 1, add := (+), mul := (*), nsmul := add_monoid.nsmul, npow := monoid.npow }; @@ -88,6 +93,11 @@ by refine_struct { zero := (0 : ulift α), one := 1, add := (+), mul := (*), sub zsmul := sub_neg_monoid.zsmul }; tactic.pi_instance_derive_field +instance non_unital_comm_ring [non_unital_comm_ring α] : non_unital_comm_ring (ulift α) := +by refine_struct { zero := (0 : ulift α), add := (+), mul := (*), sub := has_sub.sub, + neg := has_neg.neg, nsmul := add_monoid.nsmul, zsmul := sub_neg_monoid.zsmul }; +tactic.pi_instance_derive_field + instance comm_ring [comm_ring α] : comm_ring (ulift α) := by refine_struct { zero := (0 : ulift α), one := 1, add := (+), mul := (*), sub := has_sub.sub, neg := has_neg.neg, nsmul := add_monoid.nsmul, npow := monoid.npow, diff --git a/src/data/finsupp/pointwise.lean b/src/data/finsupp/pointwise.lean index ac57f2d91ff7f..17a4c91e3e405 100644 --- a/src/data/finsupp/pointwise.lean +++ b/src/data/finsupp/pointwise.lean @@ -62,6 +62,9 @@ finsupp.coe_fn_injective.non_unital_non_assoc_semiring _ coe_zero coe_add coe_mu instance [non_unital_semiring β] : non_unital_semiring (α →₀ β) := finsupp.coe_fn_injective.non_unital_semiring _ coe_zero coe_add coe_mul (λ _ _, rfl) +instance [non_unital_comm_semiring β] : non_unital_comm_semiring (α →₀ β) := +finsupp.coe_fn_injective.non_unital_comm_semiring _ coe_zero coe_add coe_mul (λ _ _, rfl) + instance [non_unital_non_assoc_ring β] : non_unital_non_assoc_ring (α →₀ β) := finsupp.coe_fn_injective.non_unital_non_assoc_ring _ coe_zero coe_add coe_mul coe_neg coe_sub (λ _ _, rfl) (λ _ _, rfl) @@ -70,6 +73,10 @@ instance [non_unital_ring β] : non_unital_ring (α →₀ β) := finsupp.coe_fn_injective.non_unital_ring _ coe_zero coe_add coe_mul coe_neg coe_sub (λ _ _, rfl) (λ _ _, rfl) +instance [non_unital_comm_ring β] : non_unital_comm_ring (α →₀ β) := +finsupp.coe_fn_injective.non_unital_comm_ring _ + coe_zero coe_add coe_mul coe_neg coe_sub (λ _ _, rfl) (λ _ _, rfl) + -- TODO can this be generalized in the direction of `pi.has_scalar'` -- (i.e. dependent functions and finsupps) -- TODO in theory this could be generalised, we only really need `smul_zero` for the definition diff --git a/src/data/set/pointwise.lean b/src/data/set/pointwise.lean index 27cadc02865a8..da6cd0863be49 100644 --- a/src/data/set/pointwise.lean +++ b/src/data/set/pointwise.lean @@ -1042,6 +1042,10 @@ instance set_semiring.non_unital_semiring [semigroup α] : non_unital_semiring ( instance set_semiring.semiring [monoid α] : semiring (set_semiring α) := { ..set_semiring.non_assoc_semiring, ..set_semiring.non_unital_semiring } +instance set_semiring.non_unital_comm_semiring [comm_semigroup α] : + non_unital_comm_semiring (set_semiring α) := +{ ..set_semiring.non_unital_semiring, ..set.comm_semigroup } + instance set_semiring.comm_semiring [comm_monoid α] : comm_semiring (set_semiring α) := { ..set.comm_monoid, ..set_semiring.semiring } diff --git a/src/logic/equiv/transfer_instance.lean b/src/logic/equiv/transfer_instance.lean index 9063a16cb87bf..60ed443084927 100644 --- a/src/logic/equiv/transfer_instance.lean +++ b/src/logic/equiv/transfer_instance.lean @@ -206,6 +206,11 @@ let zero := e.has_zero, add := e.has_add, one := e.has_one, mul := e.has_mul, nsmul := e.has_scalar ℕ, npow := e.has_pow ℕ in by resetI; apply e.injective.semiring _; intros; exact e.apply_symm_apply _ +/-- Transfer `non_unital_comm_semiring` across an `equiv` -/ +protected def non_unital_comm_semiring [non_unital_comm_semiring β] : non_unital_comm_semiring α := +let zero := e.has_zero, add := e.has_add, mul := e.has_mul, nsmul := e.has_scalar ℕ in +by resetI; apply e.injective.non_unital_comm_semiring _; intros; exact e.apply_symm_apply _ + /-- Transfer `comm_semiring` across an `equiv` -/ protected def comm_semiring [comm_semiring β] : comm_semiring α := let zero := e.has_zero, add := e.has_add, one := e.has_one, mul := e.has_mul, @@ -239,6 +244,12 @@ let zero := e.has_zero, add := e.has_add, one := e.has_one, mul := e.has_mul, ne sub := e.has_sub, nsmul := e.has_scalar ℕ, zsmul := e.has_scalar ℤ, npow := e.has_pow ℕ in by resetI; apply e.injective.ring _; intros; exact e.apply_symm_apply _ +/-- Transfer `non_unital_comm_ring` across an `equiv` -/ +protected def non_unital_comm_ring [non_unital_comm_ring β] : non_unital_comm_ring α := +let zero := e.has_zero, add := e.has_add, mul := e.has_mul, neg := e.has_neg, + sub := e.has_sub, nsmul := e.has_scalar ℕ, zsmul := e.has_scalar ℤ in +by resetI; apply e.injective.non_unital_comm_ring _; intros; exact e.apply_symm_apply _ + /-- Transfer `comm_ring` across an `equiv` -/ protected def comm_ring [comm_ring β] : comm_ring α := let zero := e.has_zero, add := e.has_add, one := e.has_one, mul := e.has_mul, neg := e.has_neg, diff --git a/src/ring_theory/hahn_series.lean b/src/ring_theory/hahn_series.lean index 74db2ffa13ecc..37d7efe8c1191 100644 --- a/src/ring_theory/hahn_series.lean +++ b/src/ring_theory/hahn_series.lean @@ -732,7 +732,7 @@ instance [semiring R] : semiring (hahn_series Γ R) := .. hahn_series.non_assoc_semiring, .. hahn_series.non_unital_semiring } -instance [comm_semiring R] : comm_semiring (hahn_series Γ R) := +instance [non_unital_comm_semiring R] : non_unital_comm_semiring (hahn_series Γ R) := { mul_comm := λ x y, begin ext, simp_rw [mul_coeff, mul_comm], @@ -751,6 +751,10 @@ instance [comm_semiring R] : comm_semiring (hahn_series Γ R) := ne.def, set.mem_set_of_eq] at ha ⊢, exact ⟨(add_comm _ _).trans ha.1, ha.2.2, ha.2.1⟩ } end, + .. hahn_series.non_unital_semiring } + +instance [comm_semiring R] : comm_semiring (hahn_series Γ R) := +{ .. hahn_series.non_unital_comm_semiring, .. hahn_series.semiring } instance [non_unital_non_assoc_ring R] : non_unital_non_assoc_ring (hahn_series Γ R) := @@ -769,6 +773,10 @@ instance [ring R] : ring (hahn_series Γ R) := { .. hahn_series.semiring, .. hahn_series.add_comm_group } +instance [non_unital_comm_ring R] : non_unital_comm_ring (hahn_series Γ R) := +{ .. hahn_series.non_unital_comm_semiring, + .. hahn_series.non_unital_ring } + instance [comm_ring R] : comm_ring (hahn_series Γ R) := { .. hahn_series.comm_semiring, .. hahn_series.ring } diff --git a/src/topology/continuous_function/zero_at_infty.lean b/src/topology/continuous_function/zero_at_infty.lean index 22dd60256e6ea..38d780ee2f4b3 100644 --- a/src/topology/continuous_function/zero_at_infty.lean +++ b/src/topology/continuous_function/zero_at_infty.lean @@ -231,6 +231,10 @@ instance [non_unital_semiring β] [topological_semiring β] : non_unital_semiring C₀(α, β) := fun_like.coe_injective.non_unital_semiring _ coe_zero coe_add coe_mul (λ _ _, rfl) +instance [non_unital_comm_semiring β] [topological_semiring β] : + non_unital_comm_semiring C₀(α, β) := +fun_like.coe_injective.non_unital_comm_semiring _ coe_zero coe_add coe_mul (λ _ _, rfl) + instance [non_unital_non_assoc_ring β] [topological_ring β] : non_unital_non_assoc_ring C₀(α, β) := fun_like.coe_injective.non_unital_non_assoc_ring _ coe_zero coe_add coe_mul coe_neg coe_sub @@ -241,6 +245,11 @@ instance [non_unital_ring β] [topological_ring β] : fun_like.coe_injective.non_unital_ring _ coe_zero coe_add coe_mul coe_neg coe_sub (λ _ _, rfl) (λ _ _, rfl) +instance [non_unital_comm_ring β] [topological_ring β] : + non_unital_comm_ring C₀(α, β) := +fun_like.coe_injective.non_unital_comm_ring _ coe_zero coe_add coe_mul coe_neg coe_sub (λ _ _, rfl) + (λ _ _, rfl) + instance {R : Type*} [semiring R] [non_unital_non_assoc_semiring β] [topological_semiring β] [module R β] [has_continuous_const_smul R β] [is_scalar_tower R β β] : is_scalar_tower R C₀(α, β) C₀(α, β) := diff --git a/src/topology/locally_constant/algebra.lean b/src/topology/locally_constant/algebra.lean index 577481f4ec6cf..e811f342f3805 100644 --- a/src/topology/locally_constant/algebra.lean +++ b/src/topology/locally_constant/algebra.lean @@ -133,6 +133,9 @@ instance [semiring Y] : semiring (locally_constant X Y) := { .. locally_constant.add_comm_monoid, .. locally_constant.monoid, .. locally_constant.distrib, .. locally_constant.mul_zero_class } +instance [non_unital_comm_semiring Y] : non_unital_comm_semiring (locally_constant X Y) := +{ .. locally_constant.non_unital_semiring, .. locally_constant.comm_semigroup } + instance [comm_semiring Y] : comm_semiring (locally_constant X Y) := { .. locally_constant.semiring, .. locally_constant.comm_monoid } @@ -149,6 +152,9 @@ instance [non_assoc_ring Y] : non_assoc_ring (locally_constant X Y) := instance [ring Y] : ring (locally_constant X Y) := { .. locally_constant.semiring, .. locally_constant.add_comm_group } +instance [non_unital_comm_ring Y] : non_unital_comm_ring (locally_constant X Y) := +{ .. locally_constant.non_unital_comm_semiring, .. locally_constant.non_unital_ring } + instance [comm_ring Y] : comm_ring (locally_constant X Y) := { .. locally_constant.comm_semiring, .. locally_constant.ring }