antidiagonals having multiplicity

Stream: general

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

[Notification Bot]

This topic was moved by Mario Carneiro to #PR reviews > antidiagonals having multiplicity #7595