# Commit 2021-04-14 18:40 e4edf46d

View on Github →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.