Zulip Chat Archive

Stream: Is there code for X?

Topic: Application of `add_monoid_hom` distributes over `sum`


view this post on Zulip Eric Wieser (Jan 21 2021 at 19:09):

This goal is frustrating me:

import data.finsupp.basic

variables {α β M N P : Type*}

@[simp]
lemma add_monoid_hom.finsupp_sum_apply [has_zero β] [add_comm_monoid N] [add_comm_monoid P]
  (f : α →₀ β) (g : α  β  N →+ P) (x : N) :
  f.sum g x = f.sum (λ i fi, g i fi x) :=
begin
  let app := (add_monoid_hom.apply (λ _ : N, P) x),
  dsimp at app,
  change app (f.sum g : N →+ P) = _,
  convert add_monoid_hom.map_finsupp_sum _ f g,
  -- oops
end

view this post on Zulip Eric Wieser (Jan 21 2021 at 19:16):

Do we have this?

namespace add_monoid_hom

def apply_hom [add_comm_monoid N] [add_comm_monoid P] (x : N) : (N →+ P) →+ P :=
{ to_fun := λ f, f x,
  map_add' := λ f g, add_apply _ _ x,
  map_zero' := zero_apply x }

end add_monoid_hom

We have docs#add_monoid_hom.apply, but that doesn't seem to help here

view this post on Zulip Eric Wieser (Jan 22 2021 at 08:50):

Ah, it's docs#add_monoid_hom.eval


Last updated: May 07 2021 at 18:19 UTC