Zulip Chat Archive

Stream: Is there code for X?

Topic: direct_sum.to_add_monoid_apply


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 _ _

view this post on Zulip Julian Külshammer (Apr 14 2021 at 21:23):

mv_polynomial should be sigma \to nat-graded?

view this post on Zulip Kevin Buzzard (Apr 14 2021 at 21:24):

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

view this post on Zulip Kevin Buzzard (Apr 14 2021 at 21:25):

I'm loving the docstring of sum_add_hom_apply too

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Apr 14 2021 at 21:30):

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

view this post on Zulip 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" :-)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 14 2021 at 21:39):

Aah, got it: docs#direct_sum.semiring


Last updated: May 16 2021 at 05:21 UTC