corprime and is_coprime

Stream: maths

[Joachim Breitner]

We currently have nat.coprime, for Nat only and defined via the gcd, and is_coprime , defined via the existence of a and b such that a * x + b * y = 1, for any commutative semiring.

I wonder if there is a way to unify the two? The nats even form a commutative semiring, but unless I'm missing something there (for lack of negative coefficients) the is_prime definition doesn't work.

Is there a definition for coprimality that's general enough to cover commutative semirings, and even works for natural numbers?

Maybe something like “there exists a and b so that a * x and b * y have an absolute different 1” (if absolute difference is a useful notion here)?

[Kevin Buzzard]

the issue here is that you have to decide whether $X$ and $Y$ are coprime in $\mathbb{C}[X,Y]$. They're coprime in the sense that the ring is a UFD and their highest common factor is 1; however they're not coprime in the sense that the ideal they generate isn't the unit ideal; it is a maximal ideal so it's contained in no principal prime but because the ring is 2-dimensional that doesn't mean it's the whole thing. Similarly you can ask whether $2$ and $1+\sqrt{-5}$ are coprime in $\mathbb{Z}[\sqrt{-5}]$. There is no prime or irreducible element that divides both of them so they're coprime in some sense, but again the ideal generated by them isn't the whole ring. The problem is that our basic definition of coprimality on $\mathbb{Z}$ generalises in several ways not all of which coincide, so it's difficult to know which one deserves the moniker "coprime".

[Joachim Breitner]

And I guess these generalization don't have good distinct names?

I see, and the fact that they differ for natural numbers is an unavoidable issue.

If I'm still bothered next time I think of this while at the computer (and not the phone) I'll maybe PR some documentation tweaks to explain this for people like me.

[Kevin Buzzard]

What's going on with the $\sqrt{-5}$ example is that the ring is a Dedekind domain but not a unique factorization domain; 2 and 1+sqrt(-5) "morally" have a common divisor, but it's the "prime" (2,1+sqrt(5)) which is a non-principal prime ideal. Ideals factor uniquely into prime ideals but because not all prime ideals are principal you have problems if you restrict your thinking to elements. This kind of example was how ideals got invented -- they were "ideals of numbers" instead of numbers, because they should be numbers but weren't.

[Joachim Breitner]

This is tickling stuff I knew 10 years ago at uni :-)