Zulip Chat Archive

Stream: new members

Topic: Formalizing Kaplansky's criterion

Emilie Uthaiwat (Sep 13 2023 at 14:42):


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?


Patrick Massot (Sep 13 2023 at 14:44):

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

Emilie Uthaiwat (Sep 13 2023 at 14:56):

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)?

Riccardo Brasca (Sep 13 2023 at 14:56):

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 (Sep 13 2023 at 15:04):

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 (Sep 13 2023 at 15:17):

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.

Last updated: Dec 20 2023 at 11:08 UTC