Zulip Chat Archive

Stream: general

Topic: antidiagonals having multiplicity


Bolton Bailey (May 12 2021 at 17:15):

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 (May 12 2021 at 17:17):

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 (May 12 2021 at 17:25):

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

Kevin Buzzard (May 12 2021 at 17:26):

an abbreviation

Johan Commelin (May 12 2021 at 17:26):

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

Bolton Bailey (May 12 2021 at 17:30):

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 (May 12 2021 at 17:34):

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 (May 12 2021 at 17:36):

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 (May 12 2021 at 17:37):

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

Bolton Bailey (May 12 2021 at 17:41):

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 (May 12 2021 at 17:42):

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 (May 12 2021 at 17:43):

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 (May 12 2021 at 17:43):

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 (May 12 2021 at 17:56):

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 (May 12 2021 at 17:58):

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 (May 12 2021 at 18:00):

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

Yaël Dillies (May 12 2021 at 18:01):

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

Bolton Bailey (May 12 2021 at 18:13):

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 (May 12 2021 at 18:27):

@Bolton Bailey thanks for chasing through all those definitions!

Johan Commelin (May 12 2021 at 18:28):

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

Bolton Bailey (May 12 2021 at 19:48):

#7595

Mario Carneiro (May 12 2021 at 21:06):

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 (May 12 2021 at 21:08):

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 (May 12 2021 at 21:09):

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 (May 12 2021 at 21:12):

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 (May 12 2021 at 21:28):

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 (May 12 2021 at 22:01):

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 (May 12 2021 at 22:04):

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 (May 13 2021 at 03:11):

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


Last updated: Dec 20 2023 at 11:08 UTC