feat(algebra/ring/basic): define non-unital, non-associative rings (#…

…6786)

This introduces the following typeclasses beneath `semiring`:
  * `non_unital_non_assoc_semiring`
  * `non_unital_semiring`
  * `non_assoc_semiring`

The goal is to use these to support a non-unital, non-associative
algebras.

The typeclass requirements of `subring`, `subsemiring`, and `ring_hom` are relaxed from `semiring` to `non_assoc_semiring`.

Instances of these new typeclasses are added for:
* alias types:
  * `opposite`
  * `ulift`
* convolutive types:
  * `(add_)monoid_algebra`
  * `direct_sum`
  * `set_semiring`
  * `hahn_series`
* elementwise types: 
  * `locally_constant`
  * `pi`
  * `prod`
  * `finsupp`



Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/algebra/basic.lean

@@ -1330,7 +1330,7 @@ instance algebra {r : comm_semiring R}
   algebra R (Π i : I, f i) :=
 { commutes' := λ a f, begin ext, simp [algebra.commutes], end,
   smul_def' := λ a f, begin ext, simp [algebra.smul_def''], end,
-  ..pi.ring_hom (λ i, algebra_map R (f i)) }
+  ..(pi.ring_hom (λ i, algebra_map R (f i)) : R →+* Π i : I, f i) }
 
 @[simp] lemma algebra_map_apply {r : comm_semiring R}
   [s : ∀ i, semiring (f i)] [∀ i, algebra R (f i)] (a : R) (i : I) :

src/algebra/big_operators/ring.lean

@@ -26,14 +26,19 @@ variables {s s₁ s₂ : finset α} {a : α} {b : β}  {f g : α → β}
 
 
 section semiring
-variables [semiring β]
+variables [non_unital_non_assoc_semiring β]
 
 lemma sum_mul : (∑ x in s, f x) * b = ∑ x in s, f x * b :=
 (s.sum_hom (λ x, x * b)).symm
 
 lemma mul_sum : b * (∑ x in s, f x) = ∑ x in s, b * f x :=
 (s.sum_hom _).symm
 
+end semiring
+
+section semiring
+variables [non_assoc_semiring β]
+
 lemma sum_mul_boole [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
   (∑ x in s, (f x * ite (a = x) 1 0)) = ite (a ∈ s) (f a) 0 :=
 by simp

src/algebra/category/CommRing/basic.lean

@@ -26,8 +26,15 @@ def SemiRing : Type (u+1) := bundled semiring
 
 namespace SemiRing
 
-instance bundled_hom : bundled_hom @ring_hom :=
-⟨@ring_hom.to_fun, @ring_hom.id, @ring_hom.comp, @ring_hom.coe_inj⟩
+/-- `ring_hom` doesn't actually assume associativity. This alias is needed to make the category
+theory machinery work. We use the same trick in `category_theory.Mon.assoc_monoid_hom`. -/
+abbreviation assoc_ring_hom (M N : Type*) [semiring M] [semiring N] := ring_hom M N
+
+instance bundled_hom : bundled_hom assoc_ring_hom :=
+⟨λ M N [semiring M] [semiring N], by exactI @ring_hom.to_fun M N _ _,
+ λ M [semiring M], by exactI @ring_hom.id M _,
+ λ M N P [semiring M] [semiring N] [semiring P], by exactI @ring_hom.comp M N P _ _ _,
+ λ M N [semiring M] [semiring N], by exactI @ring_hom.coe_inj M N _ _⟩
 
 attribute [derive [has_coe_to_sort, large_category, concrete_category]] SemiRing
 

src/algebra/char_p/pi.lean

@@ -20,7 +20,7 @@ instance pi (ι : Type u) [hi : nonempty ι] (R : Type v) [semiring R] (p : ℕ)
 ⟨λ x, let ⟨i⟩ := hi in iff.symm $ (char_p.cast_eq_zero_iff R p x).symm.trans
 ⟨λ h, funext $ λ j, show pi.eval_ring_hom (λ _, R) j (↑x : ι → R) = 0,
     by rw [ring_hom.map_nat_cast, h],
-  λ h, (pi.eval_ring_hom (λ _, R) i).map_nat_cast x ▸ by rw [h, ring_hom.map_zero]⟩⟩
+  λ h, (pi.eval_ring_hom (λ _: ι, R) i).map_nat_cast x ▸ by rw [h, ring_hom.map_zero]⟩⟩
 
 -- diamonds
 instance pi' (ι : Type u) [hi : nonempty ι] (R : Type v) [comm_ring R] (p : ℕ) [char_p R p] :

src/algebra/direct_sum_graded.lean

@@ -23,14 +23,14 @@ additively-graded ring. The typeclasses are:
 Respectively, these imbue the direct sum `⨁ i, A i` with:
 
 * `direct_sum.has_one`
-* `direct_sum.mul_zero_class`, `direct_sum.distrib`
+* `direct_sum.non_unital_non_assoc_semiring`
 * `direct_sum.semiring`, `direct_sum.ring`
 * `direct_sum.comm_semiring`, `direct_sum.comm_ring`
 
 the base ring `A 0` with:
 
 * `direct_sum.grade_zero.has_one`
-* `direct_sum.grade_zero.mul_zero_class`, `direct_sum.grade_zero.distrib`
+* `direct_sum.grade_zero.non_unital_non_assoc_semiring`
 * `direct_sum.grade_zero.semiring`, `direct_sum.grade_zero.ring`
 * `direct_sum.grade_zero.comm_semiring`, `direct_sum.grade_zero.comm_ring`
 
@@ -86,7 +86,7 @@ variables (A : ι → Type*)
 class ghas_one [has_zero ι] :=
 (one : A 0)
 
-/-- A graded version of `has_mul` that also subsumes `distrib` and `mul_zero_class` by requiring
+/-- A graded version of `has_mul` that also subsumes `non_unital_non_assoc_semiring` by requiring
 the multiplication be an `add_monoid_hom`. Multiplication combines grades additively, like
 `add_monoid_algebra`. -/
 class ghas_mul [has_add ι] [Π i, add_comm_monoid (A i)] :=
@@ -302,20 +302,15 @@ direct_sum.to_add_monoid $ λ i,
   add_monoid_hom.flip $ direct_sum.to_add_monoid $ λ j, add_monoid_hom.flip $
     (direct_sum.of A _).comp_hom.comp ghas_mul.mul
 
-instance : has_mul (⨁ i, A i) :=
-{ mul := λ a b, mul_hom A a b }
-
-instance : mul_zero_class (⨁ i, A i) :=
-{ mul := (*),
+instance : non_unital_non_assoc_semiring (⨁ i, A i) :=
+{ mul := λ a b, mul_hom A a b,
   zero := 0,
-  zero_mul := λ a, by { unfold has_mul.mul, simp only [map_zero, add_monoid_hom.zero_apply]},
-  mul_zero := λ a, by { unfold has_mul.mul, simp only [map_zero] } }
-
-instance : distrib (⨁ i, A i) :=
-{ mul := (*),
   add := (+),
-  left_distrib := λ a b c, by { unfold has_mul.mul, simp only [map_add]},
-  right_distrib := λ a b c, by { unfold has_mul.mul, simp only [map_add, add_monoid_hom.add_apply]}}
+  zero_mul := λ a, by simp only [map_zero, add_monoid_hom.zero_apply],
+  mul_zero := λ a, by simp only [map_zero],
+  left_distrib := λ a b c, by simp only [map_add],
+  right_distrib := λ a b c, by simp only [map_add, add_monoid_hom.add_apply],
+  .. direct_sum.add_comm_monoid _ _}
 
 variables {A}
 
@@ -379,9 +374,7 @@ instance semiring : semiring (⨁ i, A i) := {
   one_mul := one_mul A,
   mul_one := mul_one A,
   mul_assoc := mul_assoc A,
-  ..direct_sum.mul_zero_class A,
-  ..direct_sum.distrib A,
-  ..direct_sum.add_comm_monoid _ _, }
+  ..direct_sum.non_unital_non_assoc_semiring _, }
 
 end semiring
 
@@ -490,13 +483,9 @@ end
 @[simp] lemma of_zero_mul (a b : A 0) : of _ 0 (a * b) = of _ 0 a * of _ 0 b:=
 of_zero_smul A a b
 
-instance grade_zero.mul_zero_class : mul_zero_class (A 0) :=
-function.injective.mul_zero_class (of A 0) dfinsupp.single_injective
-  (of A 0).map_zero (of_zero_mul A)
-
-instance grade_zero.distrib : distrib (A 0) :=
-function.injective.distrib (of A 0) dfinsupp.single_injective
-  (of A 0).map_add (of_zero_mul A)
+instance grade_zero.non_unital_non_assoc_semiring : non_unital_non_assoc_semiring (A 0) :=
+function.injective.non_unital_non_assoc_semiring (of A 0) dfinsupp.single_injective
+  (of A 0).map_zero (of A 0).map_add (of_zero_mul A)
 
 instance grade_zero.smul_with_zero (i : ι) : smul_with_zero (A 0) (A i) :=
 begin

src/algebra/monoid_algebra.lean

@@ -76,34 +76,33 @@ lemma mul_def {f g : monoid_algebra k G} :
   f * g = (f.sum $ λa₁ b₁, g.sum $ λa₂ b₂, single (a₁ * a₂) (b₁ * b₂)) :=
 rfl
 
-instance : distrib (monoid_algebra k G) :=
-{ mul           := (*),
+instance : non_unital_non_assoc_semiring (monoid_algebra k G) :=
+{ zero          := 0,
+  mul           := (*),
   add           := (+),
   left_distrib  := assume f g h, by simp only [mul_def, sum_add_index, mul_add, mul_zero,
     single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_add],
   right_distrib := assume f g h, by simp only [mul_def, sum_add_index, add_mul, mul_zero, zero_mul,
     single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_zero,
     sum_add],
-  .. finsupp.add_comm_monoid }
-
-instance : mul_zero_class (monoid_algebra k G) :=
-{ zero      := 0,
-  mul       := (*),
   zero_mul  := assume f, by simp only [mul_def, sum_zero_index],
-  mul_zero  := assume f, by simp only [mul_def, sum_zero_index, sum_zero] }
+  mul_zero  := assume f, by simp only [mul_def, sum_zero_index, sum_zero],
+  .. finsupp.add_comm_monoid }
 
 end has_mul
 
 section semigroup
 
 variables [semiring k] [semigroup G]
 
-instance : semigroup_with_zero (monoid_algebra k G) :=
-{ mul       := (*),
+instance : non_unital_semiring (monoid_algebra k G) :=
+{ zero          := 0,
+  mul           := (*),
+  add           := (+),
   mul_assoc := assume f g h, by simp only [mul_def, sum_sum_index, sum_zero_index, sum_add_index,
     sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff,
     add_mul, mul_add, add_assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add],
-  .. monoid_algebra.mul_zero_class }
+  .. monoid_algebra.non_unital_non_assoc_semiring}
 
 end semigroup
 
@@ -125,14 +124,16 @@ section mul_one_class
 
 variables [semiring k] [mul_one_class G]
 
-instance : mul_zero_one_class (monoid_algebra k G) :=
+instance : non_assoc_semiring (monoid_algebra k G) :=
 { one       := 1,
   mul       := (*),
+  zero      := 0,
+  add       := (+),
   one_mul   := assume f, by simp only [mul_def, one_def, sum_single_index, zero_mul,
     single_zero, sum_zero, zero_add, one_mul, sum_single],
   mul_one   := assume f, by simp only [mul_def, one_def, sum_single_index, mul_zero,
     single_zero, sum_zero, add_zero, mul_one, sum_single],
-  ..monoid_algebra.mul_zero_class }
+  ..monoid_algebra.non_unital_non_assoc_semiring }
 
 variables {R : Type*} [semiring R]
 
@@ -175,10 +176,8 @@ instance : semiring (monoid_algebra k G) :=
   mul       := (*),
   zero      := 0,
   add       := (+),
-  .. monoid_algebra.mul_zero_one_class,
-  .. monoid_algebra.semigroup_with_zero,
-  .. monoid_algebra.distrib,
-  .. finsupp.add_comm_monoid }
+  .. monoid_algebra.non_unital_semiring,
+  .. monoid_algebra.non_assoc_semiring }
 
 variables {R : Type*} [semiring R]
 
@@ -658,20 +657,21 @@ lemma mul_def {f g : add_monoid_algebra k G} :
   f * g = (f.sum $ λa₁ b₁, g.sum $ λa₂ b₂, single (a₁ + a₂) (b₁ * b₂)) :=
 rfl
 
-instance : distrib (add_monoid_algebra k G) :=
-{ mul           := (*),
+instance : non_unital_non_assoc_semiring (add_monoid_algebra k G) :=
+{ zero          := 0,
+  mul           := (*),
   add           := (+),
   left_distrib  := assume f g h, by simp only [mul_def, sum_add_index, mul_add, mul_zero,
     single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_add],
   right_distrib := assume f g h, by simp only [mul_def, sum_add_index, add_mul, mul_zero, zero_mul,
     single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_zero,
-    sum_add], }
-
-instance : mul_zero_class (add_monoid_algebra k G) :=
-{ zero      := 0,
-  mul       := (*),
+    sum_add],
   zero_mul  := assume f, by simp only [mul_def, sum_zero_index],
-  mul_zero  := assume f, by simp only [mul_def, sum_zero_index, sum_zero] }
+  mul_zero  := assume f, by simp only [mul_def, sum_zero_index, sum_zero],
+  nsmul     := λ n f, n • f,
+  nsmul_zero' := by { intros, ext, simp [-nsmul_eq_mul, add_smul] },
+  nsmul_succ' := by { intros, ext, simp [-nsmul_eq_mul, nat.succ_eq_one_add, add_smul] },
+  .. finsupp.add_comm_monoid }
 
 end has_mul
 
@@ -693,27 +693,31 @@ section semigroup
 
 variables [semiring k] [add_semigroup G]
 
-instance : semigroup_with_zero (add_monoid_algebra k G) :=
-{ mul       := (*),
+instance : non_unital_semiring (add_monoid_algebra k G) :=
+{ zero      := 0,
+  mul       := (*),
+  add       := (+),
   mul_assoc := assume f g h, by simp only [mul_def, sum_sum_index, sum_zero_index, sum_add_index,
     sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff,
     add_mul, mul_add, add_assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add],
-  .. add_monoid_algebra.mul_zero_class }
+  .. add_monoid_algebra.non_unital_non_assoc_semiring }
 
 end semigroup
 
 section mul_one_class
 
 variables [semiring k] [add_zero_class G]
 
-instance : mul_zero_one_class (add_monoid_algebra k G) :=
+instance : non_assoc_semiring (add_monoid_algebra k G) :=
 { one       := 1,
   mul       := (*),
+  zero      := 0,
+  add       := (+),
   one_mul   := assume f, by simp only [mul_def, one_def, sum_single_index, zero_mul,
     single_zero, sum_zero, zero_add, one_mul, sum_single],
   mul_one   := assume f, by simp only [mul_def, one_def, sum_single_index, mul_zero,
     single_zero, sum_zero, add_zero, mul_one, sum_single],
-  .. add_monoid_algebra.mul_zero_class }
+  .. add_monoid_algebra.non_unital_non_assoc_semiring }
 
 variables {R : Type*} [semiring R]
 
@@ -755,13 +759,8 @@ instance : semiring (add_monoid_algebra k G) :=
   mul       := (*),
   zero      := 0,
   add       := (+),
-  nsmul     := λ n f, n • f,
-  nsmul_zero' := by { intros, ext, simp [-nsmul_eq_mul, add_smul] },
-  nsmul_succ' := by { intros, ext, simp [-nsmul_eq_mul, nat.succ_eq_one_add, add_smul] },
-  .. add_monoid_algebra.mul_zero_one_class,
-  .. add_monoid_algebra.semigroup_with_zero,
-  .. add_monoid_algebra.distrib,
-  .. finsupp.add_comm_monoid }
+  .. add_monoid_algebra.non_unital_semiring,
+  .. add_monoid_algebra.non_assoc_semiring, }
 
 variables {R : Type*} [semiring R]
 

src/algebra/opposites.lean

@@ -153,11 +153,23 @@ instance [mul_zero_class α] : mul_zero_class (opposite α) :=
 instance [mul_zero_one_class α] : mul_zero_one_class (opposite α) :=
 { .. opposite.mul_zero_class α, .. opposite.mul_one_class α }
 
+instance [semigroup_with_zero α] : semigroup_with_zero (opposite α) :=
+{ .. opposite.semigroup α, .. opposite.mul_zero_class α }
+
 instance [monoid_with_zero α] : monoid_with_zero (opposite α) :=
 { .. opposite.monoid α, .. opposite.mul_zero_one_class α }
 
+instance [non_unital_non_assoc_semiring α] : non_unital_non_assoc_semiring (opposite α) :=
+{ .. opposite.add_comm_monoid α, .. opposite.mul_zero_class α, .. opposite.distrib α }
+
+instance [non_unital_semiring α] : non_unital_semiring (opposite α) :=
+{ .. opposite.semigroup_with_zero α, .. opposite.non_unital_non_assoc_semiring α }
+
+instance [non_assoc_semiring α] : non_assoc_semiring (opposite α) :=
+{ .. opposite.mul_zero_one_class α, .. opposite.non_unital_non_assoc_semiring α }
+
 instance [semiring α] : semiring (opposite α) :=
-{ .. opposite.add_comm_monoid α, .. opposite.monoid_with_zero α, .. opposite.distrib α }
+{ .. opposite.non_unital_semiring α, .. opposite.non_assoc_semiring α }
 
 instance [ring α] : ring (opposite α) :=
 { .. opposite.add_comm_group α, .. opposite.monoid α, .. opposite.semiring α }

src/algebra/pointwise.lean

@@ -346,27 +346,22 @@ instance set_semiring.add_comm_monoid : add_comm_monoid (set_semiring α) :=
   add_zero := union_empty,
   add_comm := union_comm, }
 
-instance set_semiring.mul_zero_class [has_mul α] : mul_zero_class (set_semiring α) :=
+instance set_semiring.non_unital_non_assoc_semiring [has_mul α] :
+  non_unital_non_assoc_semiring (set_semiring α) :=
 { zero_mul := λ s, empty_mul,
   mul_zero := λ s, mul_empty,
-  ..set.has_mul, ..set_semiring.add_comm_monoid }
-
-instance set_semiring.distrib [has_mul α] : distrib (set_semiring α) :=
-{ left_distrib := λ _ _ _, mul_union,
+  left_distrib := λ _ _ _, mul_union,
   right_distrib := λ _ _ _, union_mul,
   ..set.has_mul, ..set_semiring.add_comm_monoid }
 
-instance set_semiring.mul_zero_one_class [mul_one_class α] : mul_zero_one_class (set_semiring α) :=
-{ ..set_semiring.mul_zero_class, ..set.mul_one_class }
+instance set_semiring.non_assoc_semiring [mul_one_class α] : non_assoc_semiring (set_semiring α) :=
+{ ..set_semiring.non_unital_non_assoc_semiring, ..set.mul_one_class }
 
-instance set_semiring.semigroup_with_zero [semigroup α] : semigroup_with_zero (set_semiring α) :=
-{ ..set_semiring.mul_zero_class, ..set.semigroup }
+instance set_semiring.non_unital_semiring [semigroup α] : non_unital_semiring (set_semiring α) :=
+{ ..set_semiring.non_unital_non_assoc_semiring, ..set.semigroup }
 
 instance set_semiring.semiring [monoid α] : semiring (set_semiring α) :=
-{ ..set_semiring.add_comm_monoid,
-  ..set_semiring.distrib,
-  ..set_semiring.mul_zero_class,
-  ..set.monoid }
+{ ..set_semiring.non_assoc_semiring, ..set_semiring.non_unital_semiring }
 
 instance set_semiring.comm_semiring [comm_monoid α] : comm_semiring (set_semiring α) :=
 { ..set.comm_monoid, ..set_semiring.semiring }