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

#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