direct_sum.to_add_monoid_apply

Stream: Is there code for X?

[Kevin Buzzard]

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]

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]

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]

mv_polynomial should be sigma \to nat-graded?

[Kevin Buzzard]

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

[Kevin Buzzard]

I'm loving the docstring of sum_add_hom_apply too

[Eric Wieser]

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

[Eric Wieser]

And it's not defeq because dfinsupp.sum has awful decidability requirements that docs#dfinsupp.sum_add_hom avoids

[Eric Wieser]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

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]

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]

Aah, got it: docs#direct_sum.semiring