## Stream: new members

### Topic: Applying a sum of finsupps

#### Stuart Presnell (Jan 12 2022 at 08:57):

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 (Jan 12 2022 at 08:58):

This has nothing to do with finsupp, right?

#### Yaël Dillies (Jan 12 2022 at 09:00):

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

#### Stuart Presnell (Jan 12 2022 at 09:06):

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 (Jan 12 2022 at 09:13):

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 (Jan 12 2022 at 09:35):

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

#### Stuart Presnell (Jan 12 2022 at 11:03):

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]
(α →₀ M) →+ (α → M) :=
{ to_fun := sorry,
map_zero' := 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 (Jan 12 2022 at 11:04):

coe_fn!

#### Stuart Presnell (Jan 12 2022 at 11:10):

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 (Jan 12 2022 at 11:13):

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 (Jan 12 2022 at 11:16):

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

#### Stuart Presnell (Jan 12 2022 at 11:18):

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

#### Alex J. Best (Jan 12 2022 at 11:20):

This works for me

import data.finsupp.basic

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


#### Stuart Presnell (Jan 12 2022 at 11:34):

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

#### Kevin Buzzard (Jan 12 2022 at 11:37):

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 (Jan 12 2022 at 11:50):

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

#### Sigma (Jan 12 2022 at 21:24):

at least, a very close approximation of it

#### Eric Wieser (Jan 12 2022 at 23:02):

(finsupp.apply_add_hom p).map_sum S f?

#### Eric Wieser (Jan 12 2022 at 23:04):

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 (Jan 12 2022 at 23:05):

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

#11423

#### Stuart Presnell (Jan 13 2022 at 11:55):

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.

Last updated: Dec 20 2023 at 11:08 UTC