## Stream: Is there code for X?

### Topic: Sum is linear

#### Oliver Nash (Mar 05 2021 at 20:47):

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 (Mar 05 2021 at 20:50):

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

#### Oliver Nash (Mar 05 2021 at 20:54):

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 (Mar 05 2021 at 20:54):

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

Oh I see.

#### Adam Topaz (Mar 05 2021 at 21:05):

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 (Mar 05 2021 at 21:09):

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

No, not quite.

#### Adam Topaz (Mar 05 2021 at 21:11):

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,
end


#### Adam Topaz (Mar 05 2021 at 21:11):

Note I changed g

#### Oliver Nash (Mar 05 2021 at 22:36):

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 (Mar 05 2021 at 23:10):

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

#### Eric Wieser (Mar 05 2021 at 23:15):

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

#### Eric Wieser (Mar 05 2021 at 23:31):

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

#### Oliver Nash (Mar 06 2021 at 18:04):

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 (Mar 06 2021 at 18:05):

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

#### Oliver Nash (Mar 06 2021 at 18:05):

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 (Mar 06 2021 at 18:07):

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 (Mar 06 2021 at 18:53):

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

Last updated: May 16 2021 at 05:21 UTC