# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: direct_sum.to_add_monoid_apply

#### Kevin Buzzard (Apr 14 2021 at 21:15):

```
import algebra.direct_sum
open_locale direct_sum big_operators
open_locale classical -- or decidable whatever
variables {ι : Type*}
{β : ι → Type*} [Π (i : ι), add_comm_monoid (β i)]
{γ : Type*} [add_comm_monoid γ]
(f : Π (i : ι), β i →+ γ) (b : ⨁ i, β i)
lemma direct_sum.to_add_monoid_apply :
direct_sum.to_add_monoid f b = dfinsupp.sum b (λ i, f i) := sorry
```

I was expecting the proof to be `rfl`

.

#### Kevin Buzzard (Apr 14 2021 at 21:20):

Background: I'm defining gradings on rings and I'm trying to do some test cases, e.g. a polynomial ring is nat-graded, a mv_polynomial ring is graded by something I've not worked out yet, a monoid ring is graded by the monoid etc.

#### Floris van Doorn (Apr 14 2021 at 21:20):

Not sure why the library wasn't set up in a way that this was `rfl`

, but here are two possible proofs:

```
by simp [direct_sum.to_add_monoid, dfinsupp.lift_add_hom, dfinsupp.sum_add_hom_apply]
```

or

```
dfinsupp.sum_add_hom_apply _ _
```

#### Julian Külshammer (Apr 14 2021 at 21:23):

mv_polynomial should be `sigma \to nat`

-graded?

#### Kevin Buzzard (Apr 14 2021 at 21:24):

Thanks to both of you! This chat rocks :-)

#### Kevin Buzzard (Apr 14 2021 at 21:25):

I'm loving the docstring of `sum_add_hom_apply`

too

#### Eric Wieser (Apr 14 2021 at 21:28):

I think the API is that way because duplicating every dfinsupp lemma to direct_sum would be a massive time sink

#### Eric Wieser (Apr 14 2021 at 21:29):

And it's not defeq because `dfinsupp.sum`

has awful decidability requirements that docs#dfinsupp.sum_add_hom avoids

#### Eric Wieser (Apr 14 2021 at 21:30):

I think I might be partially to blame for the friction here

#### Kevin Buzzard (Apr 14 2021 at 21:32):

Yes I noticed this! That's why I went classical -- I couldn't figure out why I suddenly needed extra decidability hypotheses. The only clues I could find were in that "docstring" :-)

#### Eric Wieser (Apr 14 2021 at 21:32):

I played with examples graded rings a little in docs#mv_polynomial.is_homogeneous.homogeneous_submodule.gcomm_monoid

#### Eric Wieser (Apr 14 2021 at 21:34):

Note the `gmonoid`

API was designed with the (external) direct sum of tensor powers in mind, which is why it needs glue for submodules

#### Kevin Buzzard (Apr 14 2021 at 21:38):

I think that docs#direct_sum.comm_semiring is what I should be putting a grading on (to test the definition). Did you need commutative?

#### Kevin Buzzard (Apr 14 2021 at 21:39):

Aah, got it: docs#direct_sum.semiring

Last updated: May 16 2021 at 05:21 UTC