Zulip Chat Archive

Stream: Is there code for X?

Topic: Sum is linear


view this post on Zulip 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?

view this post on Zulip Adam Topaz (Mar 05 2021 at 20:50):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 05 2021 at 20:54):

Oh I see.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 05 2021 at 21:09):

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

view this post on Zulip Adam Topaz (Mar 05 2021 at 21:10):

No, not quite.

view this post on Zulip 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,
  simp [finsupp.sum_add_index, hh],
end

view this post on Zulip Adam Topaz (Mar 05 2021 at 21:11):

Note I changed g

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Mar 05 2021 at 23:10):

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

view this post on Zulip Eric Wieser (Mar 05 2021 at 23:15):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Oliver Nash (Mar 06 2021 at 18:05):

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

view this post on Zulip 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:).

view this post on Zulip 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.

view this post on Zulip 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