Stream: Is there code for X?

Topic: primes associated of dvd

Julien Marquet (Feb 09 2021 at 14:46):

I'm searching for a lemma with like this :

lemma associated_of_dvd {α} [comm_monoid_with_zero α] {p q: α}
(p_prime: prime p) (q_prime: prime q) (dvd: p ∣ q): associated p q := sorry


I did not find it in mathlib, and I was wondering what was the best way to prove it
(maybe using associated_of_dvd_dvd and the definition of primes ?

Kevin Buzzard (Feb 09 2021 at 15:16):

associated_of_dvd_dvd needs something stronger than a comm_monoid_with_zero, it needs some cancellation property. I have no immediate feeling for whether what you're asking is true in the generality in which it can be stated :-)

Kevin Buzzard (Feb 09 2021 at 15:19):

I have these vague nightmare memories from undergraduate times about p dividing q and q dividing p but p and q not being associated because the cofactors weren't units...

Kevin Buzzard (Feb 09 2021 at 15:25):

Let X be the free comm monoid with 0 generated by four variables p q a b, subject to the relations p * a = q and q * b = p. Is this a counterexample?

Kevin Buzzard (Feb 09 2021 at 15:29):

My memory from UG is that one can even do this with commutative rings. Consider $\R[a,b,p]/(pab-p)$. This is not an integral domain so nobody in their right mind would be trying to factor stuff, but it might be the case that p and pa are both prime. I might be wrong though, I'm just talking from a vague memory.

Kevin Buzzard (Feb 09 2021 at 15:31):

One thing is for sure though -- Lean keeps you honest :-)

Julien Marquet (Feb 09 2021 at 15:31):

I just stated the lemma in the largest class of structure that could hold the statement :sweat_smile:
Actually I only need it in a principal ideal domain

Kevin Buzzard (Feb 09 2021 at 15:37):

lol :-) It's true for comm_cancel_monoid_with_zero, which is "integral domain but without the addition".

Kevin Buzzard (Feb 09 2021 at 15:37):

You should prove it and make a PR! Do you have a github userid?

Kevin Buzzard (Feb 09 2021 at 15:38):

And you should construct a counterexample without the hypothesis of cancellation and add to the evidence that we should have a dictionary of counterexamples in mathlib (this came up in the ordered semiring fiasco).

Kevin Buzzard (Feb 09 2021 at 15:38):

because my vague undergrad memory won't be around forever.

Julien Marquet (Feb 09 2021 at 15:39):

Kevin Buzzard said:

You should prove it and make a PR! Do you have a github userid?

Yes, I got one :)
I was just wondering what was the most elegant way to prove this, I'll figure out something :)

Julien Marquet (Feb 09 2021 at 15:40):

Kevin Buzzard said:

And you should construct a counterexample without the hypothesis of cancellation and add to the evidence that we should have a dictionary of counterexamples in mathlib (this came up in the ordered semiring fiasco).

I'm searching for a counterexample :)

Riccardo Brasca (Feb 09 2021 at 15:50):

Note that there is exists_associated_mem_of_dvd_prod that is a small generalization of what you want.

Kevin Buzzard (Feb 09 2021 at 16:15):

docs#exists_associated_mem_of_dvd_prod

Kevin Buzzard (Feb 09 2021 at 16:17):

I still think that there's an argument for putting in this special case, it's still a slight kerfuffle to get it from that

Julien Marquet (Feb 09 2021 at 16:34):

Kevin Buzzard said:

Let X be the free comm monoid with 0 generated by four variables p q a b, subject to the relations p * a = q and q * b = p. Is this a counterexample?

I thing have a counterexample but in the non-commutative case -- I might be mistaken, I do not know monoids very well.
Let's consider finite and "left-infinite" words : a; b and p = ...ababab; q = ...bababa
To compute u * v : if v is finite, then we just concatenate, else we say that u * v = v.
We get then get a monoid where pa = q and qb = p, but p and w aren't associated (the only unit being the empty word).

Kevin Buzzard (Feb 09 2021 at 16:46):

Who knows -- you'll have to check the axioms. It might well work though!

Julien Marquet (Feb 10 2021 at 14:42):

Done.
I took inspiration from exists_associated_mem_of_dvd_prod.

import algebra.associated

lemma associated_of_dvd {α} [comm_cancel_monoid_with_zero α] {p q: α}
(p_prime: prime p) (q_prime: prime q) (dvd: p ∣ q): associated p q :=
begin
cases dvd with c hc,
cases ((irreducible_of_prime q_prime).is_unit_or_is_unit hc)
.resolve_left p_prime.not_unit with u hu,
exact ⟨ u, by rw [hu, hc] ⟩,
end


I'll PR this to mathlib :)

Kevin Buzzard (Feb 10 2021 at 19:33):

Nice proof! It's about half the length of the one I knocked up the other day. Yes definitely PR!

Last updated: May 16 2021 at 05:21 UTC