Formalizing Kaplansky's criterion

Stream: new members

[Emilie Uthaiwat]

Hello,

To prove Kaplansky's criterion (i.e. an integral domain is a UFD if and only if every nonzero prime ideal contains a prime element), I have coded and used the following result: given two elements a, b of an integral domain, if a * b can be written as a product of prime elements, then a can be written as a product of a unit and prime elements (please see in the attached screenshot).

I have also created a separate file (https://github.com/riccardobrasca/kaplanski4/blob/master/Kaplanski4/Absorbing.lean) which generalizes this result (the generalization is called ProdProperty) and proves some basic statements related to it. Therefore, I was wondering whether to open a PR for both the file containing the proof of Kaplansky's criterion and the API or only for the file with Kaplansky's criterion. Could I please have your opinion on this matter?

As I did not know how to name the generalization, I have temporarily called it ProdProperty but could you please suggest me a name for it?

result.png

[Patrick Massot]

Especially in your first PRs, it is easier for everybody to have several small PRs rather than one big.

[Emilie Uthaiwat]

I can open 2 PRs then. Thank you! Do you have any suggestions concerning the name of the generalization (please see in the attached screenshot)?
property.png

[Riccardo Brasca]

Emilie's question is rather if we should give a name to this property (for a general submonoid S) and develop a little API or prove directly that the submonoid generated by the primes satisfies it. To prove this theorem we don't need anything beside the definition, and we are not sure it is a useful notion for someone else (the more natural property x * y ∈ S → x ∈ S ∧ y ∈ S is not what we want).

[Patrick Massot]

I am tempted to not define it, but I cannot be sure without saying how convenient it is to have the definition and some API.

[Emilie Uthaiwat]

Perhaps, I can just open 2 PRs. In the worst case, the API will never be used for any other result than Kaplansky's criterion.