inf_eq_mul_of_coprime

Stream: mathlib4

[Kevin Buzzard]

Let I and J be ideals of a commutative (semi)ring R.

docs#Ideal.mul_eq_inf_of_coprime says I * J = I ⊓ J if I ⊔ J = ⊤. On the other hand, docs#Ideal.inf_eq_mul_of_coprime says I ⊓ J = I * J if IsCoprime I J and furthermore if R is a Dedekind domain :-)
docs#IsCoprime.sup_eq says that I ⊔ J = ⊤ if IsCoprime I J so we have all the ingredients to remove the Dedekind domain assumption from inf_eq_mul_of_coprime:

import Mathlib.RingTheory.DedekindDomain.Ideal

#check Ideal.inf_eq_mul_of_coprime -- a theorem about Dedekind domains

lemma Ideal.inf_eq_mul_of_coprime' (R : Type*) [CommSemiring R] {I J : Ideal R}
    (coprime : IsCoprime I J) : I ⊓ J = I * J := by
  symm
  apply Ideal.mul_eq_inf_of_coprime
  exact IsCoprime.sup_eq coprime

Here are some questions about the fix. Should mul_eq_inf_of_coprime be renamed mul_eq_inf_of_sup_eq_top? It's never used in mathlib anyway, so should I just change its statement to use IsCoprime, or maybe add mul_eq_inf_of_isCoprime? And which do we want -- mul_eq_inf or inf_eq_mul? Or both?

Neither lemma is used much at all BTW. The only place inf_eq_mul_of_coprime is used (ironically with .symm!) is in docs#Ideal.quotientMulEquivQuotientProd , an explicit form of CRT for Dedekind domains, which is the same as docs#quotientInfEquivQuotientProd modulo the replacement of I ⊓ J by I * J and the superfluous Dedekind domain assumption, so probably this should also be dealt with somehow.

[Riccardo Brasca]

The name of Ideal.mul_eq_inf_of_coprime should be changed in my opinion (maybe it is like that because of some historical reason?).

[Antoine Chambert-Loir]

I don't like coprime (and find its name misleading here), but inf_eq_top is heavy. Some French people say comaximal, which is better. Maybe coTop, or cocoatom.

[Ruben Van de Velde]

theorem Ideal.isCoprime_iff_sup_eq {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
IsCoprime I J ↔ I ⊔ J = ⊤

Didn't we decide at some point that IsCoprime is the preferred spelling?