Zulip Chat Archive

Stream: maths

Topic: Extraneous requirement in finprod.smul_finsum?


Robert Maxton (Apr 14 2022 at 13:07):

So, this started with me noticing multiset only has versions on N and Z; but, well, the equivalent proof in finsum requires no_zero_smul_divisors as well. But I've managed to prove in Lean that it's not necessary:

lemma smul_sum {α: Type*} {β: Type*} [semiring α] [add_comm_group β]
  [module α β] {m: multiset β} (k: α):
  (multiset.map (λ b: β, k  b) m).sum = k  m.sum :=
  begin
    set f:= (λ b: β, k  b) with h,
    have:  (a b: β), f (a + b) = f a + f b,
      introv, rw h, finish,
    set fhom := add_monoid_hom.mk' f this,
    exact multiset.sum_hom m fhom,
  end

Upon consideration this makes some amount of sense: if I have some scalar k and module objects r, s, if r + s = 0, then k * (r + s) = 0, but if we let k be non-integer then k * r + k * s is not necessarily zero. But if I have two scalars m, n and a single object r, then no such contradiction is possible, (m + n) * r = 0 iff m * r + n * r = 0 even if the ring of scalars has torsion or the like.

... Of course, this then runs into the fact that by definition, a module has distributive scalar multiplication, so if that first contradiction is possible you didn't actually have a valid module in the first place; so I would expect that it's not necessary in either place. But I assume there's a reason smul instances don't already exist for not-N-or-Z that I just haven't considered yet...?

Yaël Dillies (Apr 14 2022 at 13:43):

So, this started with me noticing multiset only has versions on N and Z

What does that mean?

Yaël Dillies (Apr 14 2022 at 13:45):

Do you understand the distinction between docs#finsum and docs#finset.sum? Do you see why we need no_zero_smul_divisors in docs#smul_finsum?

Alex J. Best (Apr 14 2022 at 13:50):

Your proof has a few extra steps, here's a mahlibified version

import algebra.module.basic
lemma smul_sum {α: Type*} {β: Type*} [semiring α] [add_comm_group β]
  [distrib_mul_action α β] {m : multiset β} (k : α) :
  (multiset.map (λ b: β, k  b) m).sum = k  m.sum :=
multiset.sum_hom m (add_monoid_hom.mk' (() k : β  β) (smul_add _))

note that indeed you only need distrib_mul_action, not even module and there is no need to set f to be the name of a map that already has a nice notation, λ b: β, k • b can be written as (•) k (the partially applied smul operation)

Robert Maxton (Apr 14 2022 at 13:54):

Yaël Dillies said:

So, this started with me noticing multiset only has versions on N and Z

What does that mean?

It means that I rewrote this post and moved a sentence from after the proof (where it made sense) to the beginning, oops. I meant "noticing that 'multiset only has versions of distribute-smul-over-addition for N and Z

Alex J. Best (Apr 14 2022 at 13:54):

PS did you already see docs#multiset.smul_sum ?

Yaël Dillies (Apr 14 2022 at 13:56):

Yeah I still don't know what you mean. multiset.smul_sum distributes scalar multiplication over addition in the maximum generality.

Robert Maxton (Apr 14 2022 at 13:57):

Alex J. Best said:

PS did you already see docs#multiset.smul_sum ?

.... no, and what's it doing there, instead of in the algebra library where it makes sense... -_-

Robert Maxton (Apr 14 2022 at 13:57):

well, thanks...

Robert Maxton (Apr 14 2022 at 13:57):

(I spent a depressing amount of time looking for that lemma first.)

Yaël Dillies (Apr 14 2022 at 14:01):

Do you know how to search for lemmas efficiently?

Yaël Dillies (Apr 14 2022 at 14:02):

I keep a tab of the docs open and type my guess for the lemma name in the search bar.

Robert Maxton (Apr 14 2022 at 14:03):

define "efficiently"

Yaël Dillies (Apr 14 2022 at 14:04):

"usually in under 10s"

Robert Maxton (Apr 14 2022 at 14:04):

No because my internet connection is awful :V

Robert Maxton (Apr 14 2022 at 14:04):

but I pick up the keywords fast enough, so it's mostly just "put multiset, smul, sum into the search box"

Robert Maxton (Apr 14 2022 at 14:04):

forex

Yaël Dillies (Apr 14 2022 at 14:05):

Yeah

Robert Maxton (Apr 14 2022 at 14:05):

... which begs the question why I didn't in fact find it, given it's literally the first result

Robert Maxton (Apr 14 2022 at 14:05):

oh, you know what, it's because I overthought it

Robert Maxton (Apr 14 2022 at 14:05):

I had the multiset page open already, so I just skimmed that page by section

Robert Maxton (Apr 14 2022 at 14:06):

(relatedly, my internet/browser sucks and waiting for the search to actually complete frequently takes longer than finding it by hand in an already-loaded page)

Yaël Dillies (Apr 14 2022 at 14:06):

Yeah, the problem with this approach is that it might very well be in another file, which is what happened here.

Robert Maxton (Apr 14 2022 at 14:07):

yeah... sigh
Well, lesson learned. Though I will still lodge an objection about lemma organization :v

Yaël Dillies (Apr 14 2022 at 14:07):

Scalar actions are used surprisingly widely! No wonder they are spread across many files and folders.

Alex J. Best (Apr 14 2022 at 14:10):

Robert Maxton said:

yeah... sigh
Well, lesson learned. Though I will still lodge an objection about lemma organization :v

Its an ongoing process! feel free to PR moving things to better places.
In general grepping (either with the vscode project search sidebar or with command line tools works well) but it does sometimes miss things like names generated by to_addiitve, or namespaces.
There is also a workspace symbols search in vscode, via ctrl+p, #searchterm.i.want which will actually search the lemmas in the current environment by name, this is very useful too

Eric Wieser (Apr 14 2022 at 19:49):

Note that #13340 moves these lemmas (docs#multiset.smul_sum etc) elsewhere

Julian Berman (Apr 14 2022 at 23:12):

There is also a workspace symbols search in vscode, via ctrl+p, #searchterm.i.want which will actually search the lemmas in the current environment by name, this is very useful too

Eeeenteresting, is that indeed workspace symbol search... I don't think I knew this worked in VSCode. It doesn't in neovim. Probably lean-language-server is missing workspace/symbol, but that must mean that the non-LSP server knows how to do it, hrm...


Last updated: Dec 20 2023 at 11:08 UTC