Commit 2021-03-04 14:43 a8d285cc

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).