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: Dec 20 2023 at 11:08 UTC