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

#4585

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: Dec 20 2023 at 11:08 UTC