antidiagonals having multiplicity #7595

Stream: PR reviews

[Bolton Bailey]

I am thinking of making a PR that refactors finsupp.antidiagonal. The current definition of the antidiagonal of a finsupp is in mathlib is

/-- The `finsupp` counterpart of `multiset.antidiagonal`: the antidiagonal of
`s : α →₀ ℕ` consists of all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)` such that `t₁ + t₂ = s`.
The finitely supported function `antidiagonal s` is equal to the multiplicities of these pairs. -/
def antidiagonal (f : α →₀ ℕ) : ((α →₀ ℕ) × (α →₀ ℕ)) →₀ ℕ :=
(f.to_multiset.antidiagonal.map (prod.map multiset.to_finsupp multiset.to_finsupp)).to_finsupp

Usually, though, when we think of the antidiagonal of an object we just think of a set of pairs which sum to that value, rather than a set with multiplicity. The main object of importance seems to be the support of the above defined object. Indeed everywhere this is used, it seems to be prefaced with a .support. So for this reason I would like to change the type of multiset.antidiagonal from ((α →₀ ℕ) × (α →₀ ℕ)) →₀ ℕ tofinset ((α →₀ ℕ) × (α →₀ ℕ)) , and refactor the places where this is used elsewhere.

I am also thinking that multiset.antidiagonal should probably have its type changed from antidiagonal (s : multiset α) : multiset (multiset α × multiset α) to antidiagonal (s : multiset α) : finset (multiset α × multiset α), but I understand less about why this decision was made this way in the first place, so I am more hesitant here.

Any comments on whether I can or should start work on this?

[Johan Commelin]

Why not just add an abbreviation antidiagonal_finset on top of the existing things? That seems better than throwing away the multiplicities for ever.

[Bolton Bailey]

Not sure exactly what an "and abbreviation" is, could you clarify?

[Kevin Buzzard]

an abbreviation

[Johan Commelin]

abbreviation antidiagonal_finset (f) := (antidiagonal f).support

[Bolton Bailey]

Ah ok, yes, something like this would be great, but I would probably still prefer to rename the existing definition to something like "antidiagonal_multiplicity" and then name what is currently (antidiagonal f).support to just antidiagonal f, since I feel it is more fundamental than the other thing.

[Sebastien Gouezel]

If I understand right, the definition you have shown is finsupp.antidiagonal. If you want, you could additionally define finset.antidiagonal, but no need to erase the other ones: depending on the uses, one or the other may be more convenient. Do you have a motivating application for this refactor?

[Bolton Bailey]

Perhaps the issue is that I can't think of a uses for these multiplicities in any context. I'm not sure what they represent. The only reason for this refactor is just so that people don't have to go around writing _support and .support whenever they reference this object.

[Bolton Bailey]

The documentation says "The finitely supported function antidiagonal s is equal to the multiplicities of these pairs". What does this mean?

[Bolton Bailey]

Is the multiplicity simply 1 for every element in (antidiagonal f).support? If so, I think it makes more sense to talk about this object as a set, rather than a finitely supported function which is 1 on some values and 0 elsewhere. If not, some clarification in the documentation would be nice.

[Sebastien Gouezel]

It has probably been defined like that in view of some applications. So if you can locate these applications (for instance by grepping), it might give some clue on why the definition is like that.

[Sebastien Gouezel]

And if you understand this, some clarification in the documentation will definitely be welcome! If you are confused by this, you can be sure you won't be the only one.

[Bolton Bailey]

Well, as I have said, I have not been able to find a use of the antidiagonal anywhere that does not use .support

[Yaël Dillies]

Bolton Bailey said:

Perhaps the issue is that I can't think of a uses for these multiplicities in any context. I'm not sure what they represent. The only reason for this refactor is just so that people don't have to go around writing _support and .support whenever they reference this object.

Well for example polynomial multiplication by expanding out is an example where multiplicity is crucial.

[Bolton Bailey]

But that has to do with the multiplicities of the elements of the internal finsupps. The multiplicity I'm talking about represents something else. I'm trying to parse the definition to understand it now.

[Bolton Bailey]

Notice that even in mv_polynomial.basic, the coeff_mul lemma references (antidiagonal n).support rather than just (antidiagonal n)

[Yaël Dillies]

Hmm... okay, I wasn't aware of that.

[Bolton Bailey]

As far as I can tell, the "multiplicity" ultimately comes out of the powerset_aux function, which is called by multiset.antidiagonal. This function seems to assign multiplicity based on a number of sublists.

For example take a type with two elements A and B and suppose we had the finsupp f which maps A to 2 and B to 1. Then this is transformed into the list [A, A, B]. Then we take sublists [], [B], [A], [A, B], [A], [A, B], [A, A], [A, A, B]. Note that [A} and [A, B] occur twice in this list. So the antidiagonal of f would end up being
(A -> 0, B->0), (A->2, B->1) with multiplicity 1
(A -> 1, B->0), (A->1, B->1) with multiplicity 2
(A -> 2, B->0), (A->0, B->1) with multiplicity 1
(A -> 0, B->1), (A->2, B->0) with multiplicity 1
(A -> 1, B->1), (A->1, B->0) with multiplicity 2
(A -> 2, B->1), (A->0, B->0) with multiplicity 1

Ultimately, the multiplicity of any value (g_1, g_2) in antidiagonal f is just product of (f x choose g_1 k) over all values x in the support of f. So actually the value of this antidiagonal f on (g_1, g_2) can be computed from (g_1, g_2) directly.

[Johan Commelin]

@Bolton Bailey thanks for chasing through all those definitions!

[Johan Commelin]

I agree that in that case it makes sense to have multiset.antidiagonal and finsupp.antidiagonal both return a finset.

[Bolton Bailey]

#7595

[Mario Carneiro]

Johan Commelin said:

I agree that in that case it makes sense to have multiset.antidiagonal and finsupp.antidiagonal both return a finset.

Wait wait how did we get to this point? multiset.antidiagonal is supposed to return a multiset, and of course multiplicities are important

[Mario Carneiro]

similarly finsupp.antidiagonal is a function from finsupps to finsupps, it would be weird if the multiplicities were erased as seems to be the proposal here

[Mario Carneiro]

The only one where no multiplicities makes sense is finset.antidiagonal, which I guess already exists and does the right thing when lifted from multisets

[Mario Carneiro]

The posted definition of finsupp.antidiagonal looks like a not very good one, since it is just translating to and from the multiset definition; I would prefer that it be defined directly in terms of addition and multiplication so that it will work on any ring but will do the same as the existing definition when applied to finsupps to nat

[Mario Carneiro]

One thing that you might not have noticed about multiset.antidiagonal is that it does not require equality on its elements, it is purely a "structural" operation on the multiset without regard for identity of its elements. s.antidiagonal.card = 2 ^ s.card for any multiset s

[Mario Carneiro]

Here is a way to picture what finsupp.antidiagonal does, using the same example as Bolton:
Draw the finsupp as a bar graph like so:

 A
 A  B

Now for every 2-coloring of the letters here, we get a pair of finsupps:

(A)    (A)    (A)    (A)    [A]    [A]    [A]    [A]
(A)(B) (A)[B] [A](B) [A][B] (A)(B) (A)[B] [A](B) [A][B]

In the third one for example we have (A)[A](B) so the parens have A -> 1, B -> 1 and the brackets have A -> 1, B -> 0. Of the 8 finsupps, this one appears twice because there are multiple ways to 2-color the A stack.

[Mario Carneiro]

I think this interpretation is less natural on finsupps than it is on multisets, because we don't normally distinguish these two ways of subsetting A -> 2, B -> 1 to get A -> 1, B -> 1.

[Bolton Bailey]

Mario Carneiro said:

One thing that you might not have noticed about multiset.antidiagonal is that it does not require equality on its elements, it is purely a "structural" operation on the multiset without regard for identity of its elements. s.antidiagonal.card = 2 ^ s.card for any multiset s

Indeed I noticed this when trying to implement this change for multiset.antidiagonal, and failing to do so because of this issue. This seems like a practical reason for leaving multiset.antidiagonal unchanged.

Perhaps we can compromise on making the change for finsupp.antidiagonal only. Let me lay out my full case for why I think it makes more sense for finsupp.antidiagonal to return finset ((α →₀ ℕ) × (α →₀ ℕ)) rather than ((α →₀ ℕ) × (α →₀ ℕ)) →₀ ℕ

• All of the lemmas in mathlib that use finsupp.antidiagonal only deal with the support. This suggests to me that:
  • The concept of the support is fundamental
  • The concept of the multiplicity-retaining finsupp is not very useful.
• Even if it does turn out to be useful, as I have pointed out, it is possible to determine the value of finsupp.antidiagonal combinatorially anyway.
• I was, personally, surprised when I looked at the definition of finsupp.antidiagonalfor the first time because I did not expect it to have this type.
• Besides finsupp.antidiagonal and multiset.antidiagonal, there is a third object in mathlib that goes by the name "antidiagonal", namely nat_antidiagonal which takes a natural as input and returns finset (ℕ × ℕ).
  • This would be analogous in that it makes the output type a finset of products of the input type.
  • This opens the door to further generalizing the antidiagonal to other has_add types to consistently be a set, of pairs summing to the target.
  • It shows that the pattern "finsupp antidiagonals are finsupps" and "multiset antidiagonals are multisets" doesn't generalize anyway.

[Mario Carneiro]

I commented on this on the PR as well: There is a unifying abstraction that generalizes nat.antidiagonal and it returns finset ((α →₀ ℕ) × (α →₀ ℕ)) when applied to finsupps. I don't deny that this is a useful operation, and I'm not sure where finsupp.antidiagonal came from. Maybe it should be renamed to finsupp.antidiagonal' to make room for your version.

[Bolton Bailey]

Just read your comment on the PR and this has_antidiagonal abstraction seems like a good idea. I will shift gears on the PR to try to make this change.

[Bolton Bailey]

(Perhaps an admin could move this discussion to the PR reviews channel)

[Notification Bot]

This topic was moved here from #general > antidiagonals having multiplicity by Mario Carneiro

[Bolton Bailey]

@Mario Carneiro, in your comment on the PR, you propose a class

class has_antidiagonal (α : Type*) [ordered_add_comm_monoid α] :=
(antidiagonal : α → finset (α × α))
(mem_antidiagonal {{a b c : α}} : (a, b) ∈ antidiagonal c ↔ a + b = c)

Any particular reason why you choose an ordered_add_comm_monoid rather than just an add_comm_monoid? For example, it makes sense to me that we should be able to talk about the antidiagonal of an element in a finite additive group.

[Mario Carneiro]

Oh I was assuming that the order agrees with +; the antidiagonal is enumerating everything less than a given element and their "complement"

[Mario Carneiro]

in fact it could probably be upgraded to canonically_ordered_add_comm_monoid