feat(algebra/graded_monoid): Split out graded monoids from graded rin…

…gs (#9586)

This cleans up the `direct_sum.gmonoid` typeclass to not contain a bundled morphism, which allows it to be used to describe graded monoids too, via the alias for `sigma` `graded_monoid`. Essentially, this:

* Renames:
  * `direct_sum.ghas_one` to `graded_monoid.has_one`
  * `direct_sum.ghas_mul` to `direct_sum.gnon_unital_non_assoc_semiring`
  * `direct_sum.gmonoid` to `direct_sum.gsemiring`
  * `direct_sum.gcomm_monoid` to `direct_sum.gcomm_semiring`
* Introduces new typeclasses which represent what the previous names should have been:
  * `graded_monoid.ghas_mul`
  * `graded_monoid.gmonoid`
  * `graded_monoid.gcomm_monoid` 

This doesn't do as much deduplication as I'd like, but it at least manages some.
There's not much in the way of new definitions here either, and most of the names are just copied from the graded ring case.

src/algebra/direct_sum/algebra.lean

@@ -40,21 +40,19 @@ open_locale direct_sum
 variables (R : Type uR) (A : ι → Type uA) {B : Type uB} [decidable_eq ι]
 
 variables [comm_semiring R] [Π i, add_comm_monoid (A i)] [Π i, module R (A i)]
-variables [add_monoid ι] [gmonoid A]
+variables [add_monoid ι] [gsemiring A]
 
 section
 
-local attribute [instance] ghas_one.to_sigma_has_one
-local attribute [instance] ghas_mul.to_sigma_has_mul
-
 /-- A graded version of `algebra`. An instance of `direct_sum.galgebra R A` endows `(⨁ i, A i)`
 with an `R`-algebra structure. -/
 class galgebra :=
 (to_fun : R →+ A 0)
-(map_one : to_fun 1 = ghas_one.one)
-(map_mul : ∀ r s, (⟨_, to_fun (r * s)⟩ : Σ i, A i) = ⟨_, ghas_mul.mul (to_fun r) (to_fun s)⟩)
-(commutes : ∀ r x, (⟨_, to_fun (r)⟩ : Σ i, A i) * x = x * ⟨_, to_fun (r)⟩)
-(smul_def : ∀ r (x : Σ i, A i), (⟨x.1, r • x.2⟩ : Σ i, A i) = ⟨_, to_fun (r)⟩ * x)
+(map_one : to_fun 1 = graded_monoid.ghas_one.one)
+(map_mul : ∀ r s,
+  graded_monoid.mk _ (to_fun (r * s)) = ⟨_, graded_monoid.ghas_mul.mul (to_fun r) (to_fun s)⟩)
+(commutes : ∀ r x, graded_monoid.mk _ (to_fun r) * x = x * ⟨_, to_fun r⟩)
+(smul_def : ∀ r (x : graded_monoid A), graded_monoid.mk x.1 (r • x.2) = ⟨_, to_fun (r)⟩ * x)
 
 end
 
@@ -106,7 +104,7 @@ instance galgebra.of_submodules
   (carriers : ι → submodule R B)
   (one_mem : (1 : B) ∈ carriers 0)
   (mul_mem : ∀ ⦃i j⦄ (gi : carriers i) (gj : carriers j), (gi * gj : B) ∈ carriers (i + j)) :
-  by haveI : gmonoid (λ i, carriers i) := gmonoid.of_submodules carriers one_mem mul_mem; exact
+  by haveI : gsemiring (λ i, carriers i) := gsemiring.of_submodules carriers one_mem mul_mem; exact
   galgebra R (λ i, carriers i) :=
 by exact {
   to_fun := begin
@@ -130,8 +128,8 @@ coercions such as `submodule.subtype (A i)`, and the `[gmonoid A]` structure ori
 can be discharged by `rfl`. -/
 @[simps]
 def to_algebra
-  (f : Π i, A i →ₗ[R] B) (hone : f _ (ghas_one.one) = 1)
-  (hmul : ∀ {i j} (ai : A i) (aj : A j), f _ (ghas_mul.mul ai aj) = f _ ai * f _ aj)
+  (f : Π i, A i →ₗ[R] B) (hone : f _ (graded_monoid.ghas_one.one) = 1)
+  (hmul : ∀ {i j} (ai : A i) (aj : A j), f _ (graded_monoid.ghas_mul.mul ai aj) = f _ ai * f _ aj)
   (hcommutes : ∀ r, (f 0) (galgebra.to_fun r) = (algebra_map R B) r) :
   (⨁ i, A i) →ₐ[R] B :=
 { to_fun := to_semiring (λ i, (f i).to_add_monoid_hom) hone @hmul,