IsCoprime is @[simp]?

Stream: maths

[Kyle Miller]

Is the docs4#IsCoprime definition meant to be marked with the @[simp] attribute? It seems like you would generally want to keep it in IsCoprime x y form rather than immediately converting it to ∃ a b, a * x + b * y = 1.

(It's also @[simp] in mathlib3)

[Ruben Van de Velde]

I believe that was also annoying in mathlib 3

[Yury G. Kudryashov]

BTW, should we have both natural definitions (∃ a b, a * x + b * y = 1 and ∀ x, x ∣ a → x ∣ b → is_unit x a.k.a. disjoint (associates.mk a) (associates.mk b))? If yes, then what should be the names?

[Yaël Dillies]

docs#is_coprime, docs#nat.is_coprime?

[Kyle Miller]

Fyi, docs4#IsCoprime is no longer @[simp], which was a change necessary to get a norm_num extension to actually trigger. This didn't affect any proofs.

[Kyle Miller]

I was thinking about how the definition is very wrong for Nat (the only way to get IsCoprime x y is for x or y to be 1 if you use Bezout's identity as a definition).

Something that came to mind that would work for Nat is to extend the notion of a GCD domain to commutative semirings. That is, you say $x$ and $y$ are coprime in the noncommutative semiring $R$ if $(x)+(y)\subseteq (d)$, with $(d)$ the minimal principal ideal such that this is true, implies $(d)=(1)$. (Or specialized a bit more, if $(x)+(y)\subseteq (d)$ then $(d)=(1)$. No need for "minimal.")

With $\mathbb{N}$, while it's not the case that $(x)+(y)=\mathbb{N}$, at least if $x$ and $y$ are coprime you get almost all of $\mathbb{N}$.

[Kevin Buzzard]

Just to remark that for a general UFD of dimension 2 or more like $\mathbb{C}[X,Y]$, the two definitions aren't the same (eg X and Y don't have a common factor but don't generate the unit ideal either).

[Kyle Miller]

I guess at least this definition of IsCoprime would say $X$ and $Y$ are coprime since the only principal ideal containing $(X,Y)$ is $(1)$.

[Yaël Dillies]

But $X$ and $Y$ should not be coprime.

[Kevin Buzzard]

They're coprime in the sense of having no factors in common, so in a lattice-theoretic sense they're coprime.

[Yury G. Kudryashov]

Kyle Miller said:

I was thinking about how the definition is very wrong for Nat (the only way to get IsCoprime x y is for x or y to be 1 if you use Bezout's identity as a definition).

Something that came to mind that would work for Nat is to extend the notion of a GCD domain to commutative semirings. That is, you say $x$ and $y$ are coprime in the noncommutative semiring $R$ if $(x)+(y)\subseteq (d)$, with $(d)$ the minimal principal ideal such that this is true, implies $(d)=(1)$. (Or specialized a bit more, if $(x)+(y)\subseteq (d)$ then $(d)=(1)$. No need for "minimal.")

With $\mathbb{N}$, while it's not the case that $(x)+(y)=\mathbb{N}$, at least if $x$ and $y$ are coprime you get almost all of $\mathbb{N}$.

Is this definition equivalent to ∀ x, x ∣ a → x ∣ b → is_unit x?

[Yury G. Kudryashov]

Let me repeat my question: are there two names for these two notions?

[Kevin Buzzard]

It's not even clear to me in a general ring that there even exists a minimal principal ideal containing a general ideal. But one can avoid this issue by defining coprimality to simply mean "the only principal ideal containing the ideal $(x,y)$ is (1)". This is literally the same as "if d divides both x and y, then d divides 1" (just unravel the definitions).

[Michael Stoll]

In many applications, you really want the property that you can write 1 as a linear combination of x and y.
I'd be against changing the definition.

[Michael Stoll]

BTW, there is the notion of coprime ideals, which means that sum of the two ideals is the full ring (which specializes to coprimality of elements on principal ideals).

[Michael Stoll]

... and this is what you need, e.g., for the Chinese Remainder Theorem.

[Michael Stoll]

(In German, you can distinguish between "relativ prim" = coprime and "teilerfremd" = no common non-unit divisors.)

[Yaël Dillies]

I guess we could translate that by "coprime" and "factor-free"?

[Yury G. Kudryashov]

Michael Stoll said:

In many applications, you really want the property that you can write 1 as a linear combination of x and y.
I'd be against changing the definition.

That's why I say that we need both definitions.

[Kyle Miller]

There are at least three possible definitions for "$x$ and $y$ are coprime" so far:

1. The intersection of the sets of divisors for $x$ and $y$ consist of units. ("teilerfremd")
2. That $(x) + (y) = R$. (coprime in the ideal sense)
3. That the GCD of the ideal $(x,y)$ is $R$, where a principal ideal $(d)$ is the GCD of an ideal $I$ if it is the minimal principal ideal containing $I$. Or, more simply, if $(x) + (y) \subseteq (d)$ then $(d)=R$. (this is coprime in an ideal gcd sense)

The first two are not equivalent in general. Nat shows that 2 and 3 are not equivalent when you allow commutative semirings (which is what the mathlib IsCoprime is currently allowing), though the $\mathbb{C}[X,Y]$ example also shows these are different (though 1 and 3 are equivalent for it I think). I'd think that 1 and 3 are not equivalent in general, but I do know that 1 => 3.

It would be nice if mathlib had at least one of the variants of IsCoprime that for Nat is equivalent to Nat.gcd x y = 1 (for example both 1 and 3). I'm not sure the current IsCoprime makes any sense for general commutative semirings, and it seems like it should be restricted to commutative rings.

[Kyle Miller]

Are there other definitions of coprime?

[Heather Macbeth]

What about $\exists \ a \ b, ax = by + 1$? That works for $\mathbb{N}$ too.

[Kyle Miller]

Yury G. Kudryashov said:

That's why I say that we need both definitions.

I think Michael might have been saying why 3 shouldn't replace 2. We should definitely have at least 1 and 2 in mathlib.

[Kyle Miller]

@Heather Macbeth Maybe to make it obviously symmetric it could be $\exists a b c d, ax+by=cx+dy+1$?

[Kevin Buzzard]

There is no such thing as "the minimal principal ideal containing I" in general so 3 doesn't make sense as it stands. It should say "the only principal ideal continaing I is R" and then it's trivially the same as 1

[Kyle Miller]

I was careful to state it as "if R is the minimal principal ideal containing I", which doesn't assert that a minimal principal ideal exists

[Kevin Buzzard]

The proof is: (x,y) \subset (d) iff x \in (d) and y \in (d) iff d divides x and d divides y, and (d)=1 iff d divides 1 iff d is a unit.

[Kevin Buzzard]

Kyle Miller said:

I was careful to state it as "if R is the minimal principal ideal containing I", which doesn't assert that a minimal principal ideal exists

Oh OK, I can see that it can be interpreted differently to how I read it.

[Kyle Miller]

Good to know that 1 and 3 are equivalent, I see it's trivial now :smile:

[Kevin Buzzard]

Is Heather-coprime definitely symmetric in general? (on commutative semirings I mean)

[Kyle Miller]

I don't know, which is why I wanted to transform it into something that was symmetric

[Kyle Miller]

It's probably true for commutative semirings that embed in their enveloping commutative ring? I don't know my universal algebra well enough to know what characterizes this, but as we know this holds for Nat and Int.

[Kevin Buzzard]

I guess one considers the universal example, the quotient of $\mathbb{N}[X,Y,A,B]$ by the smallest relation preserving + and * and satisfying AX ~ BY+1, and asks if Y is coprime to X. I have no idea how semirings work though, I have no idea what this quotient looks like

[Kevin Buzzard]

If one wants to remain sane one could just look at the semring generated by X,Y,A,B in Z[X,Y,A,B]/(AX-(BY+1)) (which is perhaps a bit smaller)

[Kevin Buzzard]

Basically if it's true in that one (comm) semiring then it's true in all semirings because the proof will turn into a proof valued in all semirings, and conversely if it's false in any semiring then it will be false in the universal semiring. The advantage of doing the computation in the universal semiring is that it might have more structure than an arbitrary counterexample, e.g. you can try proving things by induction on degree.

[Kyle Miller]

New list for coprime definitions, to summarize everything so far:

1. The set of shared divisors for $x$ and $y$ are units. Equivalently, that the GCD of the ideal $(x) + (y)$ exists and is $(1)$. (coprime in the divisors sense)
2. That $(x)+(y)=R$. (coprime in the ideal sense)
3. That $\exists abcd,ax+by=cx+dy+1$. (coprime in an ideal sense when you know you can extend your commutative semiring to a commutative ring)

Maybe 3 can still be tweaked if someone knows more about enveloping commutative rings of commutative semirings...

[Kevin Buzzard]

Aah, you can solve a1=b0+1 in nat but you can't solve a0=b1+1 so in fact they're not the same for nat after all

[Yury G. Kudryashov]

Do we ever need (2) as opposed to (3)?

[Damiano Testa]

Kevin Buzzard said:

There is no such thing as "the minimal principal ideal containing I" in general /- so 3 doesn't make sense as it stands. It should say "the only principal ideal continaing I is R" and then it's trivially the same as 1 -/

Maybe I am misunderstanding something, but this seems almost exactly the difference between Weil and Cartier divisors. So, even if this literal definition does not make it to mathlib, I hope that some form of it will!

[Yury G. Kudryashov]

Could you please give more information for those of us who are not algebraists?

[Damiano Testa]

Sure, but I just landed: I'll do it in the next couple of hours!

[Damiano Testa]

There is an algebraic theory of dimension that works for most commutative rings with identity of interest. For instance, any finitely generated ring over a field.

This exploits the principle that generators for an ideal are "equations". You expect that each equation decreases the dimension by one, but of course there are issues of dependency that make this subtle. In particular, you would like that every ideal of codimension 1, is generated by a single relation. Even this cannot be the case and here is an example.

[Damiano Testa]

The ring is $R = \mathbb{C}[x,y,z]/(x^2 - yz)$. Geometrically, you can think of this as the vanishing set of $x^2 - yz$ in $\mathbb{C}^3$: for each value of $z$ you get a parabola, except when $z=0$ (or also there, depending on your convention of what is a parabola). The dimension of $R$ is $2$, probably not surprising.

Let $I \subset R$ be the ideal of all polynomials that vanish on the three lines

$$\mathbb{C} \cdot (1,1,1) \qquad {\textrm{and}} \qquad \mathbb{C} \cdot (0,1,0) \qquad {\textrm{and}} \qquad \mathbb{C} \cdot (0,0,1).$$

The three ideals $(x - y), (x - z), (x)$ are principal (i.e. generated by a single element) and they all contain the ideal $I$:

• $(x - y)$ vanishes on the lines with direction $(1,1,1)$ and $(0,0,1)$;
• $(x - z)$ vanishes on the lines with direction $(1,1,1)$ and $(0,0,1)$;
• $(x)$ vanishes on the lines with direction $(0,1,0)$ and $(0,0,1)$.

However, with some work you can show that any non-zero element of $R$ that vanishes on the three lines, must also vanish on another curve (including the possibility that it vanishes with multiplicity at least $2$ along one of those lines).

Thus, a principal ideal containing $I$ must contain at most two of the lines. It follows that each one of the three ideals

$$(x - y) \qquad {\textrm{and}} \qquad (x - z) \qquad {\textrm{and}} \qquad (x)$$

is minimal among the principal ideals vanishing on $I$.

[Damiano Testa]

To connect with Weil and Cartier divisors: the three ideals $(x - y)$, $(x - z)$, $(x)$ vanish on the unique non-zero Cartier divisors contained in the Weil divisor that is vanishing set of $I$.

[Damiano Testa]

[EDIT: Clarified the above.]Ok, what I deleted above is relevant, just the example is more complicated. I'll see if I can find a simpler example and will clarify the situation!

[Damiano Testa]

@Yury G. Kudryashov I updated the posts above with a more pertinent example. I hope that this is clearer, but let me know if you want more details!

The conclusion is that, as Kevin said, there are ideals that are not contained in a unique principal ideal. However, the set of the minimal principal ideals containing a given ideal is still a valuable notion: its elements roughly correspond to the largest Cartier divisors contained in a scheme.

[Michael Stoll]

Yury G. Kudryashov said:

Do we ever need (2) as opposed to (3)?

I would be strongly against replacing the standard definition of "coprime" (elements) by a more complicated one, just to be able to use semirings. I think the pain this causes for the vast majority of applications (which will be for rings) vastly outweighs any benefits here.

[Michael Stoll]

Yury G. Kudryashov said:

Michael Stoll said:

In many applications, you really want the property that you can write 1 as a linear combination of x and y.
I'd be against changing the definition.

That's why I say that we need both definitions.

I'm not against adding another definition, but it should not be called IsCoprime.

[Michael Stoll]

Maybe it could be Semiring.IsCoprime? (With a lemma that says that for a ring both are equivalent...)

[Michael Stoll]

BTW, is there any use case for a semiring other than Nat (where Nat.IsCoprime already exists)?

[Johan Commelin]

@Michael Stoll Ideal R is a semiring that shows up now and then...

[Michael Stoll]

What does coprimality (in the sense discussed above for semirings, i.e. ax + by = cx + dy + 1) correspond to there?

[Michael Stoll]

Is it different from coprimality of ideals?

[Michael Stoll]

(In mathlib(3), coprimality of ideals seems to be written as I ⊔ J = ⊤, so maybe it does not exist as a definition of its own. E.g., docs#ideal.coprime_of_no_prime_ge .)

[Johan Commelin]

Michael Stoll said:

What does coprimality (in the sense discussed above for semirings, i.e. ax + by = cx + dy + 1) correspond to there?

Good question... and I haven't yet thought about it...

[Michael Stoll]

Michael Stoll said:

Is it different from coprimality of ideals?

I think it's the same: The right hand side simplifies to 1 (i.e., R as an ideal of itself), and ax is contained in x and by is contained in y, so the statement is equivalent to x + y = 1.

[Yury G. Kudryashov]

So, is there a good name for the "other" coprime (no common divisors)?

[Kevin Buzzard]

Is there a lattice name for them? "inf of these two things is bot"

[Mario Carneiro]

that's disjoint

[Yury G. Kudryashov]

But it is not disjoint in nat

[Yury G. Kudryashov]

I mean, not w.r.t. the usual inf.

[Yaël Dillies]

I would go for factor_free

[Yury G. Kudryashov]

disjoint_factors?

[Michael Stoll]

without_common_factors ?

[Reid Barton]

or no_common_factors

[Yury G. Kudryashov]

/poll Which name should we use?
disjoint_factors
without_comon_factors
no_common_factors

[Yury G. Kudryashov]

Poll closes in 3 days from now, then I make a PR (possibly in Mathlib 4).

[Yury G. Kudryashov]

So, let it be no_common_factors.

[Yaël Dillies]

Oh, looks like the mobile app didn't cast my vote :sad:

[Timo Carlin-Burns]

Michael Stoll said:

I would be strongly against replacing the standard definition of "coprime" (elements) by a more complicated one, just to be able to use semirings. I think the pain this causes for the vast majority of applications (which will be for rings) vastly outweighs any benefits here.

I'm surprised by this sentiment. Why does changing the definition cause pain in cases where it's provably equivalent to the old one? All of the same lemmas can apply, so it seems like it would only cause pain if you were using tactics like use a, b or obtain ⟨a, b, h⟩ := ... that work on existentials directly on proofs of IsCoprime x y. I thought that kind of thing was considered defeq abuse and frowned upon.

[Michael Stoll]

I admit to defeq abuse in this context. It would probably be OK to replace that by an API lemma (that, if I have not overlooked something, currently does not exist).
Anyway, IIRC, nobody had a convincing use case for a semiring other than the naturals, so nothing was done.
(I think not even the promised PR introducing no_common_factors has materialized.)