# Zulip Chat Archive

## 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:34):

docs#finsupp.coe_fn_add_monoid_hom .map_sum?

#### 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 `sorry`

s 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 (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*}
[add_zero_class M] :
(α →₀ M) →+ (α → M) :=
{ to_fun := λ f, f,
map_zero' := by simp,
map_add' := 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:23):

its at docs#add_monoid_hom.finset_sum_apply

#### 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`

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

#### 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