Coprime if product is squarefree

Stream: Is there code for X?

[Arend Mellendijk]

Am I right to say that we don't have the following lemma? It should hold more generally for PIDs or unique factorisation monoids depending on the definition of coprime you use.

import Mathlib.Data.Nat.Squarefree

theorem coprime_of_mul_squarefree (x y : ℕ) (h : Squarefree $ x * y) : x.coprime y := by
  by_contra h_ncop
  cases' Nat.Prime.not_coprime_iff_dvd.mp h_ncop with p hp
  exact (Nat.squarefree_iff_prime_squarefree.mp h) p hp.1 $ Nat.mul_dvd_mul hp.2.1 hp.2.2

[Yaël Dillies]

We seem to have exactly one lemma relating coprime and squarefree: nat.squarefree_mul

[Arend Mellendijk]

#5669

[Yury G. Kudryashov]

@Yaël Dillies Why do you keep posting links to mathlib3 docs even if the thread is about mathlib4?

[Kyle Miller]

Mathlib3: docs3#nat.squarefree_mul, Mathlib4: docs#Nat.squarefree_mul (Note these are both linkifiers Yaël. No need to make your own links)

[Yaël Dillies]

because that's the docs I have open and it's easy to figure out the mathlib4 declaration from there.

[Kevin Buzzard]

It's easier for everyone else if you post a less confusing message

[Junyan Xu]

Wow, a language model rewrote your proof: https://wolfia.com/query/01H4J8BPAGH5RQ0F2NEGZY1KSB (see here for context)
It seems to know Lean (3) pretty well and was able to informalize the proof (or maybe it already knew the proof); probably GPT(-4)?

[Scott Morrison]

That link doesn't seem germane to this thread?

[Junyan Xu]

Thanks, fixed

[Eric Rodriguez]

Can it generalise it?

[Junyan Xu]

I asked it to generalize (two of the attempts) but the results were disappointing. Anyway, here's a generalization by myself of the PR to arbitrary "decomposition monoids", which include all gcd monoids: https://gist.github.com/alreadydone/0ad7fb42db30711c4540ac92e37f6655 (probably golfable)

[Arend Mellendijk]

With that definition of RelPrime the original lemma actually holds for arbitrary commutative monoids!

import Mathlib.Algebra.Squarefree

theorem relPrime_of_squarefree_mul {M : Type _} [CommMonoid M]
  (x y : M) (h : Squarefree (x*y)) :
    ∀ (p : M), p ∣ x → p ∣ y → IsUnit p :=
  fun p hx hy => h p $ mul_dvd_mul hx hy

[Arend Mellendijk]

Ah sorry, I missed that you proved it too

[Oliver Nash]

Junyan Xu said:

I asked it to generalize (two of the attempts) but the results were disappointing. Anyway, here's a generalization by myself of the PR to arbitrary "decomposition monoids", which include all gcd monoids: https://gist.github.com/alreadydone/0ad7fb42db30711c4540ac92e37f6655 (probably golfable)

Did any of these lemmas make it to Mathlib? I just needed essentially these exact results and proved them in #10170 I'd like to know if I can weaken the hypotheses in this:

import Mathlib.Algebra.SquareFree.Basic
import Mathlib.RingTheory.PrincipalIdealDomain

variable {R : Type*} [CommRing R] [IsDomain R] {x y p : R}

variable [IsPrincipalIdealRing R] [GCDMonoid R] -- Too strong?
-- variable [UniqueFactorizationMonoid R] -- Sufficient?

theorem squarefree_mul_iff :
    Squarefree (x * y) ↔ IsCoprime x y ∧ Squarefree x ∧ Squarefree y := by
  sorry -- See #10170

[Oliver Nash]

I've just used up my final minute for the day so I'll have to run now.

[Kevin Buzzard]

Something like this is certainly true only under the UniqueFactorizationMonoid R assuption, but then IsCoprime doesn't work. I thought Something like Disjoint x y should work instead, with the preorder on R being divisibility (so 1 is a bottom element and 0 is a top element), but then we run into two problems: Disjoint x y seems to need a partial order (even though it shouldn't, you can just ask that every inf is a bottom element), and also it's going to be hard putting this preorder on an arbitrary UFM, because the naturals and integers already have a totally different order. So really the question about whether we can weaken the hypotheses, for me right now, is more the question of how to state the result for UFMs. In other words, I guess this will be true:

variable {A : Type*} [CancelCommMonoidWithZero A] [UniqueFactorizationMonoid A] {x y : A}

theorem squarefree_mul_iff' :
    Squarefree (x * y) ↔ (∀ a, a ∣ x → a ∣ y → a ∣ 1) ∧ Squarefree x ∧ Squarefree y := by
  sorry

and #10172 (if it compiles!) will let us use docs#Disjoint on preorders. I don't however know how to solve the problem of putting the preorder I want on a unique factorization monoid without creating non-defeq diamonds for (at least) Nat, Int, Rat and Real.

[Yury G. Kudryashov]

We have docs#Associated with the right pre-order

[Yury G. Kudryashov]

Sorry, it's the relation but we have the quotient too

[Yury G. Kudryashov]

Also, I think that we should add this kind of coprime as a definition with API. What would be a good name?

[Kevin Buzzard]

Coprime :-/

[Yury G. Kudryashov]

Having both Coprime and IsCoprime with different meaning is not good.

[Kevin Buzzard]

We had a long discussion about the meaning of this term for commutative rings, with the key observation being that $X$ and $Y$ were obviously coprime in $\R[X,Y]$ but the ideal they generated was not the whole ring, so the literature says they're not coprime. However this time the discussion is about monoids so the ideal objection does not apply. Except for the fact that lots of UFMs are rings anyway :-/

[Oliver Nash]

Thanks for all of this, it's very helpful. I think I'll probably rework #10170 so that it is a result about elements of unique factorization domains but using an inline "correct" definition of coprime in the context of UFDs rather than using docs#IsCoprime (similar to what I see in docs#UniqueFactorizationMonoid.induction_on_coprime for example).

This doesn't solve the question of how best to have both types of coprimeness in the library but does at least mean I can prove my result in the generality I desire.

[Yaël Dillies]

I don't understand why we haven't simply already defined FactorFree

[Oliver Nash]

The answer may very well be the usual one: nobody's got round to it yet.

[Kevin Buzzard]

I've just tried to do a literature search on the books in my office: it seems to me that none of Matsumura commutative ring theory, Matsumura commutative algebra, and Eisenbud Commutative Algebra define coprime elements of a ring (although coprime ideals are defined to mean $I+J=(1)$). So perhaps we're at liberty to refactor Coprime to mean "no common non-unit divisor"?

[Kevin Buzzard]

Oh I've just got a dodgy pdf copy of Matsumura's commutative ring theory so I can search for words, and of the 8 times the word "coprime" is occurring in the text, 7 times it applies to ideals and the 8th time it's talking about elements of the field of fractions of a UFD and it says they can be written as $x/y$ with $x,y$ coprime (no defintion supplied ;-) ), and this would not be true for our definition of coprime. So I'm leaning towards a redefinition of coprime; we lose the assertion that if a,b are coprime then the ideals generated by a,b are coprime, but I suspect that commutative algebraists would be happy to lose this.

[Junyan Xu]

I suggest using the word "comaximal" for notions around I + J = 1.

[Junyan Xu]

Did any of these lemmas make it to Mathlib? I just needed essentially these exact results and proved them in #10170 I'd like to know if I can weaken the hypotheses in this:

Sorry I didn't see this. I have not PR'd the gist. The implications are
IsPrincipalIdealRing -> UniqueFactorizationMonoid -> GCDMonoid -> DecompositionMonoid.
So I think my version is the most general one.

[Oliver Nash]

Interesting! I just updated #10170, upgrading it from PID to UFM. It was a surprising amount of effort.

[Junyan Xu]

Wikipedia has this nice list
image.png
but apparently DecompositionMonoid isn't that well known.

[Oliver Nash]

I was just looking at this picture.

[Oliver Nash]

I'm out of time for today. I think #10170 is still a reasonable proposal but if you have the appetite I encourage you to generalise it further.

[Oliver Nash]

(feel free to push commits etc.)

[Junyan Xu]

Okay! I think even if you don't introduce DecompositionMonoid, proving it for GCDMonoid first would still be easier. We'd also like a UFD version because there isn't a canonical GCDMonoid instance on a UFD (GCD is data and involves choice).
But since I already proved it for DecompositionMonoid, I'd just go ahead to add the typeclass to mathlib (it can go into the file where docs#semigroupDvd is defined). I think it only makes sense for CommMonoid or maybe CommSemigroup.
Coprimality could be add to that file as well; to avoid conflict should we call it IsRelPrime for now? I incline to use the definition ∀ c, c ∣ a → c ∣ b → IsUnit c and it will be almost defeq to Disjoint (Associates.mk a) (Associates.mk b) except for a docs#isUnit_iff_dvd_one.

[Johan Commelin]

@Junyan Xu Do you agree with merging #10170, so that Oliver Nash can continue his Jordan-Chevalley-Dunford quest? And then we can golf it with your proof at a later stage?

[Junyan Xu]

Sounds good!

[Johan Commelin]

@Junyan Xu Just looked at your gist. Very slick development! Please PR it :smiley: