unique products

Stream: Is there code for X?

[Damiano Testa]

Dear All,

I discovered today that unique products is a thing. I am thinking of implementing them. What do people think of the code below?

Any comments are greatly appreciated!

Thanks!

import algebra.monoid_algebra.basic

/--  `unique_mul G A B a0 b0` means that the element `a0 * b0` can be written
uniquely as a product of an element of `A` and an element of `B`. -/
@[to_additive "`unique_add A B a0 b0` means that the element `a0 + b0` can be written
uniquely as a sum of an element from `A` and an element from `B`."]
def unique_mul {G} [has_mul G] (A B : finset G) (a0 b0 : G) : Prop :=
∀ ⦃a b⦄, a ∈ A → b ∈ B → a * b = a0 * b0 → a = a0 ∧ b = b0

/--  `unique_summands G` asserts that any two non-empty finite subsets of `G`
have the `unique_add` property. -/
class unique_summands (G) [has_add G] : Prop :=
( adds : ∀ {A B : finset G} (hA : A.nonempty) (hB : B.nonempty),
  ∃ (a0 ∈ A) (b0 ∈ B), unique_add A B a0 b0)

/--  `unique_products G` asserts that any two non-empty finite subsets of `G`
have the `unique_mul` property. -/
class unique_products (G) [has_mul G] : Prop :=
( muls : ∀ {A B : finset G} (hA : A.nonempty) (hB : B.nonempty),
  ∃ (a0 ∈ A) (b0 ∈ B), unique_mul A B a0 b0 )

attribute [to_additive unique_summands] unique_products

instance {M : Type*} [has_add M] [unique_summands M] : unique_products (multiplicative M) :=
{ muls := λ A B hA hB, let A' : finset M := A in have hA': A'.nonempty := hA, by
    { obtain ⟨a0, hA0, b0, hB0, J⟩ := unique_summands.adds hA' hB,
      exact ⟨additive.to_mul a0, hA0, additive.to_mul b0, hB0, λ a b aA bB H, J aA bB H⟩ } }

[Yaël Dillies]

This is a thing in additive combinatorics, actually!

[Damiano Testa]

Yes, I put the import of where I was going to use it, but actually it is much lower than that. Anyway, I'm going to make a PR, but do give comments on the definition! I have checked that this would work smoothly with non-zero divisors.

[Damiano Testa]

(The application is fairly direct: if the grading type of an add_monoid_algebra satisfies the unique_summands property, then the add_monoid_algebra has no non-zero zero-divisors as soon as the base ring has no non-zero zero-divisors.

As far as I can tell, this easy result implies easily all(?) the no_zero_divisors instances around add_monoid_algebra, polynomial, mv_polynomial in mathlib.)

[Johan Commelin]

How often is this satisfied in practice? I guess pnat has this property?

[Damiano Testa]

I have a proof of what is below:

@[to_additive covariants.to_unique_summands]
instance covariants.to_unique_products {A} [has_mul A] [linear_order A]
  [covariant_class A A (*) (≤)] [covariant_class A A (function.swap (*)) (<)]
  [contravariant_class A A (*) (≤)] : unique_products A :=

[Damiano Testa]

Basically, if you have a linear order and with an operation and the operation is "sufficiently monotone", then unique_products holds.

[Damiano Testa]

This applies to the grading types of mv_polynomials, for instance.

[Damiano Testa]

Both of these work:

example : unique_summands ℕ := by apply_instance
example : unique_products pnat := by apply_instance
example : unique_summands ℤ := by apply_instance

[Johan Commelin]

Aah, of course ℕ also satisfies it.

[Johan Commelin]

0 is not a problem.

[Damiano Testa]

(I added int above.)

[Johan Commelin]

Wait, I'm still confused. What is the motivation again for these classes? You mentioned something with gradings.
Are we morally more interested in unique_summands or unique_products?

[Damiano Testa]

Btw Johan, while what I wrote is correct, this is what you probably had in mind:

example : unique_summands pnat := by apply_instance

[Yaël Dillies]

By the way, unique_mul is equivalent to (A * B).card = A.card * B.card

[Johan Commelin]

unique_products ℕ is false, right?

[Damiano Testa]

For add_monoid_algebra, summands would make more sense. But in more general group theory, people do study the "unique property" and in that context the operation is not commutative and they tend to use products.

[Damiano Testa]

Johan Commelin said:

unique_products ℕ is false, right?

I guess so!

[Johan Commelin]

Yaël Dillies said:

By the way, unique_mul is equivalent to (A * B).card = A.card * B.card

I don't think so

[Johan Commelin]

You are leaving out a0 and b0

[Johan Commelin]

Rain, so I'm closing my laptop

[Yaël Dillies]

Ah yes, you're talking about a single element. Then you should replace a0 * b0 by a single variable.

[Damiano Testa]

Yaël, so should I should also quantify over 4 elements?

[Damiano Testa]

(or two pairs?)

[Damiano Testa]

@Yaël Dillies here is a concrete proposal:

def unique_mul {G} [has_mul G] (A B : finset G) (x : G) : Prop :=
∀ ⦃a b c d⦄, a ∈ A → b ∈ B → c ∈ A → d ∈ B → a * b = x → c * d = x → a = c ∧ b = d

To me, it seems a little more cumbersome, but maybe I am wrong. Likely, there is a better way of expressing this concept.

[Yaël Dillies]

I'll have time later today to find the correct combinatorial definition.

[Junyan Xu]

unique_products pnat is equivalent to unique_summands (ℕ →₀ ℕ) via a monoid isomorphism. unique_products ℕ is not true since A={0}, B={1,2} admit no unique product.

I don't like the disparity between the names summand and product. Could the former just be sum?

The property could also be phrased to say there is an element of G that has a unique preimage in A×B under multiplication; maybe this is what Yaël means?

class unique_products (G) [has_mul G] : Prop :=
( muls : ∀ {A B : finset G} (hA : A.nonempty) (hB : B.nonempty),
  ∃ g : G, ∃! ab ∈ A ×ˢ B, ab.1 * ab.2 = g )

class unique_products' {G} [has_mul G] : Prop :=
( muls : ∀ {A B : finset G} (hA : A.nonempty) (hB : B.nonempty),
  ∃ g : G, nonempty (unique (function.uncurry has_mul.mul ⁻¹' {g} ∩ A ×ˢ B : set (G × G))))

[Damiano Testa]

Sorry for the sudden silence: I was talking to a student.

Without trying them out, I would say that the last definition unique_products' may be harder to work with than the other candidates.

Does anyone have any strong opinion on which one should be the definition of unique_products?

[Damiano Testa]

@Junyan Xu I am happy to use unique_sum for what is called unique_summads above.

[Yaël Dillies]

That would suggest docs#finset.sum. What about unique_mul/unique_add?

[Damiano Testa]

Unique products is the established name in the literature, so I would rather keep that one.

[Junyan Xu]

Can't we use to_additive on classes? Would the name unique_prod be automatically additivized to unique_sum?

[Damiano Testa]

How about calling them unique_prods and unique_sums? It is easy enough to get to_additive to learn about prods -> sums, the "multiplicative" name would be closer to the usual convention and unique_sums would probably clash less with finset.sum?

[Damiano Testa]

Junyan Xu said:

Can't we use to_additive on classes? Would the name unique_prod be automatically additivized to unique_sum?

From the to_additive doc-module:

This file defines an attribute to_additive that can be used to
automatically transport theorems and definitions (but not inductive
types and structures) from a multiplicative theory to an additive theory.

When I use simply to_additive on the class it creates something with the right name, but adds a single declaration to the environment: there is exactly one declaration with the same prefix.

I will define the two classes separately and will bind them with to_additive after the fact.

[Yaël Dillies]

Yes that's how you should do it.

[Damiano Testa]

Honestly, I am finding

class unique_products (G) [has_mul G] : Prop :=
( muls : ∀ {A B : finset G} (hA : A.nonempty) (hB : B.nonempty),
  ∃ g : G, ∃! ab ∈ A ×ˢ B, ab.1 * ab.2 = g )

very hard to work with. I agree that it looks very nice, but it is a nightmare of proof obligations, angle bracket and repeated fields.

[Damiano Testa]

I am trying to see how workable this definition is

@[to_additive]
def unique_mul' {G} [has_mul G] (A B : finset G) (g : G) : Prop :=
subsingleton { ab : G × G | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = g }

(where I still need to think about how to make sure that there actually is a witness when we want one!)

[Yaël Dillies]

Your original version looks best to me.

[Alex J. Best]

How so? Carrying around these non-empty hypotheses that need to be checked all the time, when the existence isn't really what we are worried about definitely seems onerous to me.

[Alex J. Best]

Maybe using docs#set.image2 in the definition would give you a lot of useful structure to start with?

[Damiano Testa]

I am having difficulties of two kind with the exists ... exists!... definition. First, g is determined by what comes next, ab but you really need to snake your way around angle brackets and rfls to get to a stage where you can use this. I could get used to it, but it seems too much effort for such a simple concept. Second, if you have unique_mul' as your goal and you use rintro? you obtain a mess of hypotheses that are very hard to parse for me, unless I dsimp them and even after that, it is not clear what to do. Here is a sample:

lemma unique_mul_forall {G} [has_mul G] (A B : finset G) {a0 b0 : G} (aA : a0 ∈ A) (bB : b0 ∈ B) :
  unique_mul A B (a0 * b0) → ∀ ⦃a b⦄, a ∈ A → b ∈ B → a * b = a0 * b0 → a = a0 ∧ b = b0 :=
begin
  rintro ⟨⟨ᾰ_w_fst, ᾰ_w_snd⟩, ⟨ᾰ_h_left_w, ᾰ_h_left_h_left, ᾰ_h_left_h_right⟩, ᾰ_h_right⟩ a b ᾰ_1 ᾰ_2 ᾰ_3,
  sorry,
end

leaving as state:

G: Type u_1
_inst_1: has_mul G
AB: finset G
a0b0ab: G
ᾰ_1: a ∈ A
ᾰ_2: b ∈ B
ᾰ_3: a * b = a0 * b0
ᾰ_w_fstᾰ_w_snd: G
ᾰ_h_right: ∀ (y : G × G), (λ (ab : G × G), ∃! (H : ab ∈ A ×ˢ B), ab.fst * ab.snd = a0 * b0) y → y = (ᾰ_w_fst, ᾰ_w_snd)
ᾰ_h_left_w: (ᾰ_w_fst, ᾰ_w_snd) ∈ A ×ˢ B
ᾰ_h_left_h_left: (ᾰ_w_fst, ᾰ_w_snd).fst * (ᾰ_w_fst, ᾰ_w_snd).snd = a0 * b0
ᾰ_h_left_h_right: ∀ (y : (ᾰ_w_fst, ᾰ_w_snd) ∈ A ×ˢ B), (λ (H : (ᾰ_w_fst, ᾰ_w_snd) ∈ A ×ˢ B), (ᾰ_w_fst, ᾰ_w_snd).fst * (ᾰ_w_fst, ᾰ_w_snd).snd = a0 * b0) y → y = ᾰ_h_left_w
⊢ a = a0 ∧ b = b0

[Damiano Testa]

(the rintro is the uncleaned output of rintro?, but, ignoring the weird variable names, the end result is a mess anyway)

[Damiano Testa]

The initial definition that I posted may not be as snappy, but does not expand to something unwieldy if you are not careful to tame it.

The non-empty assertions are fairly common to have in context, at least for my use case. Also, note that

def unique_mul {G} [has_mul G] (A B : finset G) (a0 b0 : G) : Prop :=
∀ ⦃a b⦄, a ∈ A → b ∈ B → a * b = a0 * b0 → a = a0 ∧ b = b0

does not have a proof obligation: you start with elements on G but then the proofs that you need to provide are harmless and are really dealing with the substance of unique_mul.

[Damiano Testa]

As always, this is my impression and it is not set in stone! I am simply reporting that for me, the exists...exists!... definition is hard to use.

[Damiano Testa]

Trying to find slogans why I prefer the other definition:

• it uses more universal quantifiers than existential ones;
• it works with compositions of arrows, instead of products.

In my experience, both of the above provide a smoother user experience.

[Damiano Testa]

In any case, I am also aware that the only thing that is important is that whatever definition is used, there is also a lemma to states that it is equivalent to the one that I like! Thus, if everyone prefers the exists...exists!... one, then all this means is that I will roll my sleeves up, prove that it is equivalent to the one that I want and then never look at the implemented definition again! :upside_down:

[Damiano Testa]

I opened a PR with the initial definition. I can certainly change it, but mostly wanted to have oleans, since modifying to_additive is never easy on the CPU of my computer!

[Damiano Testa]

#16329

[Eric Wieser]

I'm struggling to see how unique_summands holds for nat; if A=B={0,1} and g = 1 then surely there is no unique choice ab?

[Damiano Testa]

The g is bound by an existential quantifier, not a universal one.

[Damiano Testa]

You usually choose the smallest or largest elements and take it from there.

[Damiano Testa]

In your example, g=0 or g=2 work, but g=1 does not.

[Damiano Testa]

But since we are asking for the existence of a good g, all is ok!

[Damiano Testa]

Yaël also thought that it was universal quantification earlier in the thread.

[Damiano Testa]

In case it helps, this is where unique_sums is heading. When you multiply two elements of an add_monoid_algebra, the "generic" monomial in the resulting product is a sum of several contributions. unique_sums isolates, if they exist, the monomials that receive a unique contribution. These monomials are unlikely to be "in the middle", they tend to be "on the boundary". This explains why, when you have an order, you end up seeing either mins or maxs.

I hope that this helps with the intuition!

[Eric Wieser]

Curse android and it not showing ∃ or ∀ in your example and leaving me to guess!

[Damiano Testa]

I pushed two implications relating the definition in the PR with two of the definitions in this thread.

I have not yet thought of what is needed to make them iffs, since I was not yet ready to think about such hard concepts as whether a finset is empty or not.

Also, oleans with the to_additive change are available, I simply stopped CI before it could finish linting/testing, in case you want to experiment yourself.

[Damiano Testa]

#16329 now has a more extensive doc-module and the lemmas that I wanted in (and some more).

Does anyone want more lemmas added to this file? Are there more comments on the definition? I proved the equivalence of Junyan Xu's version and the one that I initially had, so I do not mind swapping the definitions. However, I still find it easier to work with the current one than with the other.

[Yaël Dillies]

I wonder whether we want that to go under combinatorics.additive. @Bhavik Mehta, thoughts?

[Damiano Testa]

Ah, I am glad that you brought the issue of where it goes! I was thinking maybe in finset.

[Mauricio Collares]

Sidon sets are certainly additive combinatorics, but it would say something for all elements, not for a single one

[Yaël Dillies]

So far, everything that's about pointwise operations of finsets is either in data.finset.pointwise or under combinatorics.additive. But I don't know whether this qualifies as additive combinatorics or not.

[Damiano Testa]

While I realize that combinatorics does not only deal with finite sets, unique_prods should fail on any finite set with at least two elements and an operation. This makes me a little skeptical about putting it in combinatorics: I am not sure that I would ever look for it there, whereas I would want to use this for zero-divisors in add_monoid_algebras.

[Damiano Testa]

I think that finset.something is a better fit: I would look there if I were thinking about support of elements of add_monoid_algebras and I guess that combinatorics stuff can easily be found in finset, right?

[Yaël Dillies]

Given that combinatorics is often concerned about finite things embedded into infinite ones, that wouldn't bother me much.