Summing over a Finite type which is not a Fintype

Stream: Is there code for X?

[Stepan Nesterov]

In #34584, I was asked to refactor file#Mathlib/RepresentationTheory/Maschke to only assume [Finite G] instead of [Fintype G]. This file uses a lot of expressions of the form $\sum_{g \in G} f(g)$, which are implemented using Finset.sum.
My understanding is that a Finset is a finite set together with a specified ordering, and Finset.sum is the sum in that order. However, if $f$ takes values in a commutative additive monoid, the order should not matter, and it's really annoying to use Finset.sum, which requires one. Is there another sum function in Mathlib, which sums over finite sets directly instead?
If not, I could always define a new sum which sums over a finite set in the order given by Fintype.ofFinite, and try developing some API for it. Would it be a good design choice?

[Snir Broshi]

I don't think Finset has any order, it's an element of the quotient of lists with no duplicates over the list permutation relation. So while you can take out a representative list (which might be how Lean will compile the code), the Finset itself is all possible orderings at the same time.
docs#Finset.sum already requires commutativity precisely for that reason, otherwise the sum wouldn't be well defined.

[Stepan Nesterov]

Then what is the difference between Finset and Set.Finite?

[Stepan Nesterov]

I need to make sense of $\sum_{x \in X} f(x)$, where (X A : Type*) [Finite X] [AddCommGroup A] (f : X -> A).

[Stepan Nesterov]

And as it currently stands, I need to lift X to a Fintype. If it's not picking an ordering, what does it actually do?

[Snir Broshi]

docs#Finite: a proof that a type is finite, which originated from a specific ordering (a bijection with Fin n for some n), but it's impossible to recover that order
docs#Set.Finite: converts the Set to a Subtype (aka an element + a proof it's in the set), then applies Finite on it
docs#Finset: an equivalence class of lists with no duplicates under the "is a permutation of" relation
docs#Fintype: a Finset plus a proof that it's everything in the type

[Jakub Nowak]

Maybe docs#finsum ?

It says

We define products and sums over types and subsets of types, with no finiteness hypotheses. All infinite products and sums are defined to be junk values (i.e. one or zero). This approach is sometimes easier to use than Finset.sum, when issues arise with Finset and Fintype being data.

so it seems like it was created exactly for your use case?

[Robin Arnez]

Where do you need sums? In the statement or the proof? If it's the statement, use Fintype instead or otherwise you'll get instance diamonds

[Jakub Nowak]

(deleted)

[Stepan Nesterov]

Jakub Nowak said:

Maybe docs#finsum ?

This looks exactly like what I had in mind. Does mathlib have any specific conventions for preferring Finset.sum in some cases?

[Snir Broshi]

Stepan Nesterov said:

If it's not picking an ordering, what does it actually do?

It's summing every possible list with no duplicates, and proving that permutations don't change the result, therefore the sum is well-defined as a function from equivalence classes (aka Finsets)

[Stepan Nesterov]

Robin Arnez said:

Where do you need sums? In the statement or the proof? If it's the statement, use Fintype instead or otherwise you'll get instance diamonds

I guess it's the statement. I need to make heavy use of averages: if $G$ is a finite group, and it acts on $V$, then I look at $\sum_{g \in G} gv$ and prove some things about it. But I'm told that all the modern parts of the group theory library use [Finite G], and I cannot local instance : Fintype G := Fintype.ofFinite G because it'll cause diamonds. So I'm looking to avoid Finset.sum.

[Snir Broshi]

AFAIK you should Fintype for defs and Finite for theorems

[Stepan Nesterov]

But what is the point of having two definitions of the same thing, one for defs and one for theorems?

[Snir Broshi]

It's not two separate defs, only one def

[Snir Broshi]

When you want to prove stuff about it, you can Fintype.ofFinite

[Jakub Nowak]

According to @Oliver Nash you should try to use Finite in def if possible.

[Snir Broshi]

This says: I assumed Finite so surely there's a Finset which contains all the elements, please give me that set so I can sum with it

[Snir Broshi]

You can use Finite in defs but it requires jumping through hoops, e.g. open Classical in

[Stepan Nesterov]

But why couldn't people just choose one of Fintype and Finite and stick with it throughout mathlib? When @Oliver Nash reviewed my PR it sounded like Fintype is just an old thing which shouldn't be used anymore, now I'm confused

[Ruben Van de Velde]

That makes sense, because it's confusing :)

[Ruben Van de Velde]

There's advantages to both. If you're going to be dealing with finite sums, probably the Finset API is better developed

[Stepan Nesterov]

Is it ok to do something like this or is it a diamond?

variable (X : Type*) [Finite X]

lemma something_about_sums [Fintype X] : …

[Stepan Nesterov]

If I’m gonna take this approach seriously, I’m going to have half the lemmas in a file assume Finite and half of them Fintype

[Stepan Nesterov]

And I know that working with a [Monoid G] and then changing your mind in some lemmas to make it a group is very annoying, and you probably had to open a new section when this happens

[Ruben Van de Velde]

That might be fine but redundant

[Stepan Nesterov]

Wha would be a better way to switch between Finite and Fintype assumptions in-between lemmas?

[Eric Wieser]

Group the lemmas by which assumption they need, or just don't use variable?

[Snir Broshi]

You can also omit [Finite X] in but it gets annoying

[Kevin Buzzard]

My take on it would be to use Finite everywhere and finsum everywhere. Finite in definitions is better than Fintype because it's more general -- Fintype implies Finite immediately via typeclass inference with no fuss. If there is missing API in finsum then add it. I would love to see Fintype completely banished from finite group theory.

[Kevin Buzzard]

The history of finsum was that I was proving Sylow's theorems with an undergraduate and we found Fintype/Finset really annoying and confusing to use, so we switched to Finite and Set.finite and then couldn't do finite sums, so we PRed finsum and when making the basic API we ended up deducing everything from Finset.sum and ended up learning the tricks for Finset and Fintype and then found that actually they weren't bad to use after all so I stopped pushing for more finsum stuff. But recently it's begun to bug me again, it's kind of embedded in group homology because this needs a lot of Finsupp :-/ so now I occasionally dream of making a nonconstructive Finsupp :-/

[Kevin Buzzard]

The selling point of Fintype is that you can #eval but given that representation theory traditionally takes place over the complexes you're not going to be able to eval anything anyway. Basically there's a trade off between making things easier for beginners and making things computable.

[Eric Wieser]

I think there's slightly more to the tradeoff than that, but that's certainly the most prominent dimension of it

[Andrew Yang]

IMO the advantage of Finset.sum or Finsupp over finsum is the fact that finiteness is bundled so automation works a lot better. In my experience, when working withfinsums one would need to prove finitely supported again and again by hand and it was quite annoying.

[Thomas Browning]

Should there be a Set.Finite.sum?

[Thomas Browning]

(or a Finite.sum?)

[Kevin Buzzard]

Or classical bundled finite subsets? Or both? :-)

[Jakub Nowak]

Kevin Buzzard said:

Or classical bundled finite subsets? Or both? :-)

I think that's what was discussed here #new members > Why Finset? .