Sum is linear

Stream: Is there code for X?

[Oliver Nash]

I'm a bit surprised that I can't find the following lemma anywhere:

import data.finsupp.basic

variables {α R M N : Type*}
variables [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N]
variables {f : α →₀ M} {g : α → M → N}

-- TODO Convenient coercion to state using `g : α → M →[R] N` instead of the unbundled hypothesis ?
@[simp] lemma finsupp.smul_sum' (h : ∀ (t : R) a m, g a (t • m) = t • g a m) (t : R) :
  (t • f).sum g = t • (f.sum g) := sorry

I have a (horrid) proof that I can tidy up and push but I thought I'd check here first. Any ideas?

[Adam Topaz]

Isn't it possible to make docs#finsupp.smul_sum work here?

[Oliver Nash]

Maybe but I don’t think so: it doesn’t use the scalar action on f, but rather only on the module M.

[Oliver Nash]

It seems totally ridiculous but I had to fuss about quite a bit to get a proof.

[Adam Topaz]

Oh I see.

[Adam Topaz]

Here's a sketch, but I can't find anything like finsupp.foo either:

import linear_algebra
import data.finsupp.basic

variables {α R M N : Type*}
variables [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N]
variables {f : α →₀ M} {g : α → M → N}

lemma finsupp.foo (f1 f2 : α →₀ M) : (f1 + f2).sum g = f1.sum g + f2.sum g := sorry

-- TODO Convenient coercion to state using `g : α → M →[R] N` instead of the unbundled hypothesis ?
@[simp] lemma finsupp.smul_sum' (h : ∀ (t : R) a m, g a (t • m) = t • g a m) (t : R) :
  (t • f).sum g = t • (f.sum g) :=
begin
  apply finsupp.induction f,
  simp,
  intros a b f ha hb hh,
  simp [finsupp.foo, hh],
  congr,
  rw [finsupp.sum_single_index, finsupp.sum_single_index, h],
  sorry, sorry -- follows from linearity
end

[Adam Topaz]

oh, maybe this is it? docs#finsupp.sum_smul_index

[Adam Topaz]

No, not quite.

[Adam Topaz]

Ok, here it is golfed a bit:

import linear_algebra
import data.finsupp.basic

variables {α R M N : Type*}
variables [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N]
variables {f : α →₀ M} {g : α → M →ₗ[R] N}

-- TODO Convenient coercion to state using `g : α → M →[R] N` instead of the unbundled hypothesis ?
@[simp] lemma finsupp.smul_sum' (t : R) :
  (t • f).sum (λ a, g a) = t • (f.sum (λ a, g a)) :=
begin
  apply finsupp.induction f,
  simp only [finsupp.sum_zero_index, smul_zero],
  intros a b f ha hb hh,
  simp [finsupp.sum_add_index, hh],
end

[Adam Topaz]

Note I changed g

[Oliver Nash]

Thanks, this is great :-) My horrid proof only assumed g to be a family of mul_action_homs but in my application I have full linearity so I'll go with this.

[Eric Wieser]

There's definitely a one-line proof for this...

[Eric Wieser]

What's the statement for a general add_monoid_hom, not just t \smul

[Eric Wieser]

docs#add_monoid_hom.map_finsupp_sum applied to docs#smul_add_hom should be half of the puzzle I think

[Oliver Nash]

Eric Wieser said:

docs#add_monoid_hom.map_finsupp_sum applied to docs#smul_add_hom should be half of the puzzle I think

If I'm reading it right, docs#add_monoid_hom.map_finsupp_sum does not apply here. The smul on the LHS of my (t • f).sum g = t • (f.sum g) is a scalar action on α →₀ M whereas the LHS of map_finsupp_sum consumes f.sum g which is an element of N.

[Oliver Nash]

(Note also that I require a semimodule structure for my statement to make sense.)

[Oliver Nash]

I wouldn't be surprised if there is a one-line proof and I would love if someone could find it (maybe GPTf :thinking:).

[Oliver Nash]

Eric Wieser said:

What's the statement for a general add_monoid_hom, not just t \smul

This is a great point of course but if this result really is missing (as I now believe) then I think the corresponding general statement would use it, rather than the other way around. Anyway, I only have a few minutes so I'd better stop waffling and see if I can PR Adam's proof.

[Oliver Nash]

https://github.com/leanprover-community/mathlib/pull/6565