Applying a sum of finsupps

Stream: new members

[Stuart Presnell]

Do we already have (something like) this?

import data.finsupp.basic

open_locale big_operators

lemma finsupp_summation_apply {ι α : Type*} {S : finset ι} {p : α} {f : ι → α →₀ ℕ} :
  (S.sum f) p = ∑ (x : ι) in S, (f x) p :=
begin
  classical,
  apply finset.induction_on' S, { simp },
  { intros i T hi hST hiT h, simp [finset.sum_insert hiT, h] },
end

I couldn't find it with library_search or from looking through data/finsupp/basic.

[Yaël Dillies]

This has nothing to do with finsupp, right?

[Yaël Dillies]

I mean that it should be an instance of the general fact that some operation is an add_monoid_hom.

[Stuart Presnell]

Ah, I guess so. When I change f : ι → α →₀ ℕ to f : ι → α → ℕ the proof still works, because it's not using the fact that the f i are finsupps.

[Stuart Presnell]

Oh, but then the place where I'm using this lemma no longer works. Here the f i really are finsupps — they're n.factorization (for some n depending on i).

[Eric Wieser]

docs#finsupp.coe_fn_add_monoid_hom .map_sum?

[Eric Wieser]

Looks like that's missing, we seem to only have it for dfinsupp

[Stuart Presnell]

Coming back to this, I've tried to fill in the sorrys here but can't make any progress

def coe_fn_add_monoid_hom {α M : Type*} [has_zero M]
[add_zero_class (α → M)] [add_zero_class (α →₀ M)] :
 (α →₀ M) →+ (α → M) :=
{ to_fun := sorry,
  map_zero' := sorry,
  map_add' := sorry,
}

It seems like it should be obvious: map_zero' should be finsupp.coe_zero and map_add' should be finsupp.coe_add, but I can't find anything I can put in for to_fun that makes these work. Am I just on completely the wrong track?

[Yaël Dillies]

coe_fn!

[Stuart Presnell]

I tried that, but then map_zero' := finsupp.coe_zero gives:

type mismatch at field 'map_zero''
  coe_zero
has type
  @eq (?m_1 → ?m_2)
    (@coe_fn (@finsupp ?m_1 ?m_2 ?m_3) (λ (_x : @finsupp ?m_1 ?m_2 ?m_3), ?m_1 → ?m_2)
       (@finsupp.has_coe_to_fun ?m_1 ?m_2 ?m_3)
       0)
    0
but is expected to have type
  @eq (α → M)
    (@coe_fn (@finsupp α M _inst_1) (λ (ᾰ : @finsupp α M _inst_1), α → M) (@finsupp.has_coe_to_fun α M _inst_1)
       0)
    0

[Stuart Presnell]

Am I going wrong by saying [add_zero_class (α → M)] [add_zero_class (α →₀ M)]? Is there some single thing from which both of these can be inferred?

[Alex J. Best]

I would think add_zero_class M would suffice (mathematically speaking) whether Lean knows this or not I'm not sure

[Stuart Presnell]

From that Lean can infer [add_zero_class (α → M)] but not [add_zero_class (α →₀ M)].

[Alex J. Best]

This works for me

import data.finsupp.basic

open_locale big_operators
noncomputable
def coe_fn_add_monoid_hom {α M : Type*}
[add_zero_class M] :
 (α →₀ M) →+ (α → M) :=
{ to_fun := λ f, f,
  map_zero' := by simp,
  map_add' := by simp,
}

[Stuart Presnell]

Brilliant, thanks! So it turns out that my problem was the [has_zero M].

[Kevin Buzzard]

Judging by your error message "X is supposed to be X" I suspect that you had more than one zero kicking around (this is just a guess, you could debug if you were interested but now it's working so maybe just move on)

[Stuart Presnell]

Yes, I guess the has_zero M and one of the add_zero_class … were conflicting.

[Sigma]

its at docs#add_monoid_hom.finset_sum_apply

[Sigma]

at least, a very close approximation of it

[Eric Wieser]

(finsupp.apply_add_hom p).map_sum S f?

[Eric Wieser]

Indeed, the statement of docs#finsupp.sum_apply is defeq to a special case of the lemma you ask for, and the proof can be used without modification

[Eric Wieser]

I recommend adding your lemma as finsupp.finset_sum_apply before that lemma, and then proving finsupp.sum_apply with finsupp.finset_sum_apply

[Stuart Presnell]

#11423

[Stuart Presnell]

I've PRed finsupp.finset_sum_apply (and also coe_fn_add_monoid_hom with credit to @Alex J. Best) but I couldn't see how to get a nicer proof of finsupp.sum_apply than the one-liner already present.