primes associated of dvd

Stream: Is there code for X?

[Julien Marquet]

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]

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]

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]

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]

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]

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

[Julien Marquet]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Julien Marquet]

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]

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]

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

[Kevin Buzzard]

docs#exists_associated_mem_of_dvd_prod

[Kevin Buzzard]

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]

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]

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

[Julien Marquet]

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]

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