# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: finsupp.sum commutes with monoid_hom

#### Eric Wieser (Oct 12 2020 at 16:00):

Does this exist?

```
def finsupp.sum {α : Type} {β : Type} {γ : Type} {δ : Type}
[has_zero β] [add_comm_monoid γ] [add_comm_monoid δ]
(f : α →₀ β) (g : α → β → γ) (h : γ →+ δ) : h (f.sum g) = f.sum (λ a b, h (g a b)) := sorry
```

#### Eric Wieser (Oct 12 2020 at 16:12):

I can prove it as:

```
def monoid_hom.map_finsupp_sum {α : Type} {β : Type} {γ : Type} {δ : Type}
[has_zero β] [add_comm_monoid γ] [add_comm_monoid δ]
(f : α →₀ β) (g : α → β → γ) (h : γ →+ δ) : h (f.sum g) = f.sum (λ a b, h (g a b)) := begin
rw finsupp.sum,
rw h.map_sum,
set g2 := λ a b, h (g a b),
conv_lhs {
congr,
skip,
funext,
change g2 x (f x),
},
rw ←finsupp.sum,
end
```

#### Yury G. Kudryashov (Oct 12 2020 at 16:39):

```
lemma add_monoid_hom.map_finsupp_sum {α : Type} {β : Type} {γ : Type} {δ : Type}
[has_zero β] [add_comm_monoid γ] [add_comm_monoid δ]
(f : α →₀ β) (g : α → β → γ) (h : γ →+ δ) : h (f.sum g) = f.sum (λ a b, h (g a b)) :=
h.map_sum _ _
```

#### Yury G. Kudryashov (Oct 12 2020 at 16:40):

Or better

```
@[to_additive]
lemma monoid_hom.map_finsupp_prod {α β γ δ : Type*}
[has_zero β] [comm_monoid γ] [comm_monoid δ]
(f : α →₀ β) (g : α → β → γ) (h : γ →* δ) : h (f.prod g) = f.prod (λ a b, h (g a b)) :=
h.map_prod _ _
```

#### Yury G. Kudryashov (Oct 12 2020 at 16:41):

I failed to find it in `data/finsupp/basic`

#### Eric Wieser (Oct 12 2020 at 17:07):

Are you happy to PR those?

#### Yury G. Kudryashov (Oct 12 2020 at 17:22):

Feel free to PR. I won't have time for this (I mean, monitoring the status of the PR) today.

#### Adam Topaz (Oct 12 2020 at 17:24):

It's Canadian Thanksgiving!

#### Heather Macbeth (Oct 12 2020 at 17:25):

That explains why all our favourite Canadians are online at once! @Frédéric Dupuis @Yury G. Kudryashov @Adam Topaz

#### Heather Macbeth (Oct 12 2020 at 17:27):

Oh, is @Jacques Carette Canadian?

#### Adam Topaz (Oct 12 2020 at 17:27):

Yeah

#### Adam Topaz (Oct 12 2020 at 17:29):

(I think so)

#### Eric Wieser (Oct 12 2020 at 19:47):

#### Eric Wieser (Oct 12 2020 at 19:48):

Not included is `alg_hom.map_finsupp_prod`

and `alg_hom.map_finsupp_sum`

because I'm not sure where to put them

#### Eric Wieser (Oct 13 2020 at 10:39):

^ Those are now done in #4603. It's annoying how when you extend a structure, you have to manually copy across all the lemmas about the base structure.

#### Jacques Carette (Oct 13 2020 at 13:21):

Yes, I am Canadian.

#### Eric Wieser (Oct 15 2020 at 10:09):

It looks like this already existed as docs#finsupp.sum_hom

#### Eric Wieser (Oct 15 2020 at 10:09):

Should I revert those PRs?

Last updated: May 07 2021 at 19:12 UTC