feat(algebra/direct_sum_graded): A 0 is a ring, A i is an A 0-module, and direct_sum.of A 0 is a ring_hom (#6851)

In a graded ring, grade 0 is itself a ring, and grade `i` (and therefore, the overall direct_sum) is a module over elements of grade 0.
This stops just short of the structure necessary to make a graded ring a graded algebra over elements of grade 0; this requires some extra assumptions and probably a new typeclass, so is best left to its own PR.

The main results here are `direct_sum.grade_zero.comm_ring`, `direct_sum.grade_zero.semimodule`, and `direct_sum.of_zero_ring_hom`.

Note that we have no way to let the user provide their own ring structure on `A 0`, as `[Π i, add_comm_monoid (A i)] [semiring (A 0)]` provides `add_comm_monoid (A 0)` twice.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: eric-wieser

src/algebra/direct_sum_graded.lean

@@ -22,10 +22,31 @@ additively-graded ring. The typeclasses are:
 
 Respectively, these imbue the direct sum `⨁ i, A i` with:
 
-* `has_one`
-* `mul_zero_class`, `distrib`
-* `semiring`, `ring`
-* `comm_semiring`, `comm_ring`
+* `direct_sum.has_one`
+* `direct_sum.mul_zero_class`, `direct_sum.distrib`
+* `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.semiring`, `direct_sum.grade_zero.ring`
+* `direct_sum.grade_zero.comm_semiring`, `direct_sum.grade_zero.comm_ring`
+
+and the `i`th grade `A i` with `A 0`-actions (`•`) defined as left-multiplication:
+
+* (nothing)
+* `direct_sum.grade_zero.has_scalar (A 0)`, `direct_sum.grade_zero.smul_with_zero (A 0)`
+* `direct_sum.grade_zero.semimodule (A 0)`
+* (nothing)
+
+Note that in the presence of these instances, `⨁ i, A i` itself inherits an `A 0`-action.
+
+`direct_sum.of_zero_ring_hom : A 0 →+* ⨁ i, A i` provides `direct_sum.of A 0` as a ring
+homomorphism.
+
+## Direct sums of subobjects
 
 Additionally, this module provides helper functions to construct `gmonoid` and `gcomm_monoid`
 instances for:
@@ -236,9 +257,10 @@ gcomm_monoid.of_add_submonoids (λ i, (carriers i).to_add_submonoid) one_mem mul
 
 end shorthands
 
+variables (A : ι → Type*)
+
 /-! ### Instances for `⨁ i, A i` -/
 
-variables (A : ι → Type*)
 
 section one
 variables [has_zero ι] [ghas_one A] [Π i, add_comm_monoid (A i)]
@@ -433,6 +455,130 @@ instance comm_ring : comm_ring (⨁ i, A i) := {
 
 end comm_ring
 
+
+/-! ### Instances for `A 0`
+
+The various `g*` instances are enough to promote the `add_comm_monoid (A 0)` structure to various
+types of multiplicative structure.
+-/
+
+section grade_zero
+
+section one
+variables [has_zero ι] [ghas_one A] [Π i, add_comm_monoid (A i)]
+
+/-- `1 : A 0` is the value provided in `direct_sum.ghas_one.one`. -/
+@[nolint unused_arguments]
+instance grade_zero.has_one : has_one (A 0) :=
+⟨ghas_one.one⟩
+
+@[simp] lemma of_zero_one : of _ 0 (1 : A 0) = 1 := rfl
+
+end one
+
+section mul
+variables [add_monoid ι] [Π i, add_comm_monoid (A i)] [ghas_mul A]
+
+/-- `(•) : A 0 → A i → A i` is the value provided in `direct_sum.ghas_mul.mul`, composed with
+an `eq.rec` to turn `A (0 + i)` into `A i`.
+-/
+instance grade_zero.has_scalar (i : ι) : has_scalar (A 0) (A i) :=
+{ smul := λ x y, (zero_add i).rec (ghas_mul.mul x y) }
+
+/-- `(*) : A 0 → A 0 → A 0` is the value provided in `direct_sum.ghas_mul.mul`, composed with
+an `eq.rec` to turn `A (0 + 0)` into `A 0`.
+-/
+instance grade_zero.has_mul : has_mul (A 0) :=
+{ mul := (•) }
+
+@[simp]lemma grade_zero.smul_eq_mul (a b : A 0) : a • b = a * b := rfl
+
+@[simp] lemma of_zero_smul {i} (a : A 0) (b : A i) : of _ _ (a • b) = of _ _ a * of _ _ b :=
+begin
+  rw of_mul_of,
+  dsimp [has_mul.mul, direct_sum.of, dfinsupp.single_add_hom_apply],
+  congr' 1,
+  rw zero_add,
+  apply eq_rec_heq,
+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.smul_with_zero (i : ι) : smul_with_zero (A 0) (A i) :=
+begin
+  letI := smul_with_zero.comp_hom (⨁ i, A i) (of A 0).to_zero_hom,
+  refine dfinsupp.single_injective.smul_with_zero (of A i).to_zero_hom (of_zero_smul A),
+end
+
+end mul
+
+section semiring
+variables [Π i, add_comm_monoid (A i)] [add_monoid ι] [gmonoid A]
+
+/-- The `semiring` structure derived from `gmonoid A`. -/
+instance grade_zero.semiring : semiring (A 0) :=
+function.injective.semiring (of A 0) dfinsupp.single_injective
+  (of A 0).map_zero (of_zero_one A) (of A 0).map_add (of_zero_mul A)
+
+/-- `of A 0` is a `ring_hom`, using the `direct_sum.grade_zero.semiring` structure. -/
+def of_zero_ring_hom : A 0 →+* (⨁ i, A i) :=
+{ map_one' := of_zero_one A, map_mul' := of_zero_mul A, ..(of _ 0) }
+
+/-- Each grade `A i` derives a `A 0`-semimodule structure from `gmonoid A`. Note that this results
+in an overall `semimodule (A 0) (⨁ i, A i)` structure via `direct_sum.semimodule`.
+-/
+instance grade_zero.semimodule {i} : semimodule (A 0) (A i) :=
+begin
+  letI := semimodule.comp_hom (⨁ i, A i) (of_zero_ring_hom A),
+  exact dfinsupp.single_injective.semimodule (A 0) (of A i) (λ a, of_zero_smul A a),
+end
+
+end semiring
+
+section comm_semiring
+
+variables [Π i, add_comm_monoid (A i)] [add_comm_monoid ι] [gcomm_monoid A]
+
+/-- The `comm_semiring` structure derived from `gcomm_monoid A`. -/
+instance grade_zero.comm_semiring : comm_semiring (A 0) :=
+function.injective.comm_semiring (of A 0) dfinsupp.single_injective
+  (of A 0).map_zero (of_zero_one A) (of A 0).map_add (of_zero_mul A)
+
+end comm_semiring
+
+section ring
+variables [Π i, add_comm_group (A i)] [add_comm_monoid ι] [gmonoid A]
+
+/-- The `ring` derived from `gmonoid A`. -/
+instance grade_zero.ring : ring (A 0) :=
+function.injective.ring (of A 0) dfinsupp.single_injective
+  (of A 0).map_zero (of_zero_one A) (of A 0).map_add (of_zero_mul A)
+  (of A 0).map_neg (of A 0).map_sub
+
+end ring
+
+section comm_ring
+variables [Π i, add_comm_group (A i)] [add_comm_monoid ι] [gcomm_monoid A]
+
+/-- The `comm_ring` derived from `gcomm_monoid A`. -/
+instance grade_zero.comm_ring : comm_ring (A 0) :=
+function.injective.comm_ring (of A 0) dfinsupp.single_injective
+  (of A 0).map_zero (of_zero_one A) (of A 0).map_add (of_zero_mul A)
+  (of A 0).map_neg (of A 0).map_sub
+
+end comm_ring
+
+end grade_zero
+
 end direct_sum
 
 /-! ### Concrete instances -/