# Commit 2021-03-04 14:43 a8d285cc

View on Github →feat(algebra/direct_sum_graded): endow `direct_sum`

with a ring structure (#6053)
To quote the module docstring

This module provides a set of heterogenous typeclasses for defining a multiplicative structure over

`⨁ i, A i`

such that`(*) : A i → A j → A (i + j)`

; that is to say,`A`

forms an additively-graded ring. The typeclasses are:

`direct_sum.ghas_one A`

`direct_sum.ghas_mul A`

`direct_sum.gmonoid A`

`direct_sum.gcomm_monoid A`

Respectively, these imbue the direct sum

`⨁ i, A i`

with:

`has_one`

`mul_zero_class`

,`distrib`

`semiring`

,`ring`

`comm_semiring`

,`comm_ring`

Additionally, this module provides helper functions to construct

`gmonoid`

and`gcomm_monoid`

instances for:

`A : ι → submonoid S`

:`direct_sum.ghas_one.of_submonoids`

,`direct_sum.ghas_mul.of_submonoids`

,`direct_sum.gmonoid.of_submonoids`

,`direct_sum.gcomm_monoid.of_submonoids`

`A : ι → submonoid S`

:`direct_sum.ghas_one.of_subgroups`

,`direct_sum.ghas_mul.of_subgroups`

,`direct_sum.gmonoid.of_subgroups`

,`direct_sum.gcomm_monoid.of_subgroups`

If the

`A i`

are disjoint, these provide a gradation of`⨆ i, A i`

, and the mapping`⨁ i, A i →+ ⨆ i, A i`

can be obtained as`direct_sum.to_monoid (λ i, add_submonoid.inclusion $ le_supr A i)`

.