## Stream: Is there code for X?

#### 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)]
(f : Π (i : ι), β i →+ γ) (b : ⨁ i, β i)

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