Extraneous requirement in finprod.smul_finsum?

Stream: maths

[Robert Maxton]

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]

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

What does that mean?

[Yaël Dillies]

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]

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]

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]

PS did you already see docs#multiset.smul_sum ?

[Yaël Dillies]

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

[Robert Maxton]

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]

well, thanks...

[Robert Maxton]

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

[Yaël Dillies]

Do you know how to search for lemmas efficiently?

[Yaël Dillies]

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

[Robert Maxton]

define "efficiently"

[Yaël Dillies]

"usually in under 10s"

[Robert Maxton]

No because my internet connection is awful :V

[Robert Maxton]

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

[Robert Maxton]

forex

[Yaël Dillies]

Yeah

[Robert Maxton]

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

[Robert Maxton]

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

[Robert Maxton]

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

[Robert Maxton]

(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]

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

[Robert Maxton]

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

[Yaël Dillies]

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

[Alex J. Best]

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]

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

[Julian Berman]

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...