Finsupp.total

Stream: mathlib4

[Patrick Massot]

Returning to MIL writing, I need to explain docs#Finsupp.total. But I have no clue why we need to suffer with all those explicit arguments. I understand that a fully unapplied Finsupp.total is fully ambiguous, and I understand we want a linear map so a partially applied one makes sense. But why are the indexing type α and the module type M explicit? Why not keeping only the ring R explicit?

[Patrick Massot]

@Anne Baanen, do you know about this?

[Anne Baanen]

I suspect this is legacy from an old Lean 3 version where failing to fill in all the arguments would block the search for a docs#CoeFun instance. Nowadays I don't see why we can't leave everything implicit and use (R := _) notation if we do need to supply them.

[Patrick Massot]

I think having R implicit is a bit too much. There is no way we can partially apply it without providing R.

[Eric Wieser]

I agree that R should be explicit and the rest implicit

[Patrick Massot]

I will work on refactoring this.

[Patrick Massot]

I’m done. I opened #16221. It touches only 29 files, which is less than what I expected. I think even lines that got longer are now more readable.

[Patrick Massot]

Next I would like to bikeshed a bit the name of this function. I have no idea where this names comes from, and I think it is pretty hard to guess. Is there any downside to renaming it linear_combination (besides the clash with tactic name)?

[Patrick Massot]

or Finsupp.linear_combination

[Eric Wieser]

Finsupp.linearCombination would be the #naming-approved spelling

[Patrick Massot]

Yes, good point.

[Eric Wieser]

That sounds better than total to me, though my (controversial?) take here is that Finsupp.total R v v' (with the second argument present) should not be the simp-normal form and docs#Finsupp.total_apply should be simp.

[Patrick Massot]

That’s yet another question, right?

[Eric Wieser]

Yes, and so I would be happy to merge a rename / deprecation in the meantime

[Patrick Massot]

I’ll wait a bit for more comments about the renaming (and wait for bors to merge the binder PR of course).

[Patrick Massot]

I need to go anyway.

[Eric Wieser]

For reference, we already have docs#Finset.affineCombination

[Frédéric Dupuis]

I would also vote for Finsupp.linearCombination.

[Johan Commelin]

It is also 1 direction of docs#Finsupp.lift fwiw

[Patrick Massot]

New question: do we want to keep Finsupp.linearCombination protected? I’m not sure I see the point. I’m not even sure I understand why the old name was protected.

[Yaël Dillies]

I tend to agree, especially since my convexity refactor would introduce the analogous _root_.convexCombination

[Antoine Chambert-Loir]

@María Inés de Frutos Fernández and I should probably revisit what we did for weight/degree of mv polynomials, because it more or less duplicates docs#Finsupp.total. However, thinking about applications to polynomials, say, I would like that something that just sums all values of the Finsupp exists, and Finsupp.total would be a reasonable name.

[Patrick Massot]

Are you looking for docs#Finsupp.sum ?

[Eric Wieser]

I think it was f.sum fun _ => id?

[Patrick Massot]

I just opened #16277 for the renaming. I hate myself for having volunteered to do that. But the new name really feels better.

[Antoine Chambert-Loir]

Eric Wieser said:

I think it was f.sum fun _ => id?

Yes it is that, but I can't find it reasonable to have to type this all the time.

[Yaël Dillies]

Maybe you are just missing notation?

[Antoine Chambert-Loir]

Yes, maybe, although I tend to prefer names to notation. (My impression is that notation can only be guessed with difficulty from the mathlib docs.)

[Eric Wieser]

A very similar notion is docs#DirectSum.coeAddMonoidHom

[Eric Wieser]

... which in fact, is what in the long run I ended up using instead of f.sum fun _ => id