dfinsupp.to_finsupp

Stream: Is there code for X?

[Kevin Buzzard]

I'm developing an API for graded rings as part of the liquid project, so I'm having to learn about dfinsupp (and about time too). @Eric Wieser has already done a lot of the groundwork -- thanks Eric. I realised yesterday that actually in some cases I want to switch back from dfinsupp to finsupp, but I don't know how to do it. Here's a little API I've been building but the very top definition and theorem are sorried. Am I approaching this correctly? Is there a slick way of filling in the top sorries? I am still a bit scared of quotients, although I'm much more confident now having taught a workshop on them!

import data.dfinsupp
import data.finsupp
import algebra.direct_sum_graded

variables {ι : Type*}
  {B : Type*} [has_zero B]

-- This would probably be enough for me to get started
def dfinsupp.to_finsupp : (Π₀ (i : ι), B) → (ι →₀ B) := sorry

-- defining property
theorem dfinsupp.to_finsupp_apply (f : Π₀ (i : ι), B) (j : ι) : f.to_finsupp j = f j := sorry

-- monoid variant
variables {M : Type*} [add_comm_monoid M]

noncomputable def dfinsupp.to_finsupp.add_monoid_hom : (Π₀ (i : ι), M) →+ (ι →₀ M) :=
{ to_fun := dfinsupp.to_finsupp,
  map_zero' := begin ext, rw dfinsupp.to_finsupp_apply, refl, end,
  map_add' := λ x y, begin ext, simp [dfinsupp.to_finsupp_apply] end }

variables {β : ι → Type*} [Π i, add_comm_monoid (β i)]

open_locale direct_sum

-- This seems natural
noncomputable def dfinsupp.to_finsupp_monoid_hom (φ : Π i, β i →+ M) : (⨁ i, β i) →+ (ι →₀ M) :=
add_monoid_hom.comp dfinsupp.to_finsupp.add_monoid_hom (dfinsupp.map_range.add_monoid_hom φ)

variables {A : ι → add_submonoid M}

-- the definition I actually want
noncomputable def direct_sum.add_submonoid_to_finsupp : (⨁ i, A i) →+ (ι →₀ M) :=
dfinsupp.to_finsupp_monoid_hom (λ i, (A i).subtype)

[Eric Wieser]

I have a PR that adds precisely the definition in the title of this thread

[Eric Wieser]

#7311

[Kevin Buzzard]

I'm really sorry! I find the PR queue a bit overwhelming. Many thanks!

I think that direct_sum.add_submonoid_to_finsupp is somehow a fundamental thing: for example direct_sum.to_add_monoid is just finsupp.sum of direct_sum.add_submonoid_to_finsupp.

[Eric Wieser]

I started with that definition too in #7217, but Johan made me question whether it was really more fundamental than plain to_finsupp

[Eric Wieser]

Also there are computability and elaborator dragons all over the place

[Eric Wieser]

dfinsupp is entirely computable, finsupp is almost entirely not