Zulip Chat Archive

You need docs#unique_factorization_monoid.normalization_monoid to choose a normalization. ~~(It seems this construction can be generalized to any monoid ...)~~

Riccardo Brasca (Oct 11 2022 at 17:12):

Mmm, if it is an instance it risks to conflict with the normalized one

Riccardo Brasca (Oct 11 2022 at 17:13):

So annoying

Junyan Xu (Oct 11 2022 at 20:05):

I think it doesn't hurt to add unique_factorization_monoid -> nonempty (gcd_monoid / normalization_monoid / normalized_gcd_monoid) instances, and then you can use choice (or just destruct the nonempty when in a proof) to get the desired (normalized)_(gcd)_monoid.

Filippo A. E. Nuccio (Oct 11 2022 at 21:15):

Well, but then if you need to use choice, or destruct nonempty in a proof, isn't it the same as doing haveI : blabla and add the local instance? By "the same" I mean "equally annoying".

Junyan Xu (Oct 11 2022 at 21:24):

Maybe some theorems could be changed to use the nonempty gcd_monoid etc. hypothesis, if gcd doesn't appear in the statement? If you want the gcd data you have to make some choice, right? If you're working with explicit types there may already be gcd_monoid instances like docs#polynomial.normalized_gcd_monoid. I don't know about your use case so maybe this is a #xy.

Filippo A. E. Nuccio (Oct 11 2022 at 21:27):

Well, my use case is for $\mathbb{Z}_p$ but in general I would like to have @Riccardo Brasca 's proof that the minimal polynomial does not change when passing to the field of fractions for arbitrary PID's. Now we have it for $\mathbb{Z}$ and for $k[T]$ but this sounds strange.

Filippo A. E. Nuccio (Oct 11 2022 at 21:28):

At any rate, I will use PID->UFM->normalized_gcd using haveI for the second step for the time being.

Junyan Xu (Oct 11 2022 at 21:36):

docs#minpoly.gcd_domain_eq_field_fractions is a theorem that could have [normalized_gcd_monoid R] replaced by [nonempty (normalized_gcd_monoid R)] as far as I can see.

We certainly don't want to end up with two non-defeq instances on the same type. We could use forgetful inheritance and demand that unique_factorization_monoid carries the data of gcd and normalization, but it seems to me there's no good way to normalize in a consistent way in e.g. a number ring of class number one.

Filippo A. E. Nuccio (Oct 11 2022 at 21:38):

Yes, I think you are right. Yet I wonder if there is a mathematical reason for these troubles: the theorem should hold for a PID, right? The choice of normalization is only needed to allow the greater generality of gcd_monoids instead of UFD's, am I wrong?

Junyan Xu (Oct 11 2022 at 21:41):

Actually I think this particular theorem could simply be generalized to use docs#is_integrally_closed as I mention in another thread, which is a Prop, then typeclass inference through the instances docs#unique_factorization_monoid.is_integrally_closed and docs#principal_ideal_ring.to_unique_factorization_monoid should be automatic.

Before that happens, PID->UFM->normalized_gcd is probably the easiest way to go.

Actually right now if you want to use docs#adjoin_root.minpoly.equiv_adjoin for R a field you have to go through that ordeal as well.

Filippo A. E. Nuccio (Oct 11 2022 at 21:45):

Actually, I tried but I am stuck with normalization_monoid ℤ_[p] which seems to be needed for docs#unique_factorization_monoid.to_normalized_gcd_monoid But this cannot be inferred by PID/UFD automatically.

Filippo A. E. Nuccio (Oct 11 2022 at 21:46):

But I agree that integrally_closed seems the right generality, I hope it will get PR'd soon.

Junyan Xu (Oct 11 2022 at 21:51):

This is what you are missing:
Junyan Xu said:

You need docs#unique_factorization_monoid.normalization_monoid to choose a normalization. ~~(It seems this construction can be generalized to any monoid ...)~~

Filippo A. E. Nuccio (Oct 11 2022 at 21:53):

Ah, thanks! As a last question: where does this "normalization" idea come from? Do we have an example in nature of something having several normalizations? And why is it called a "normalization" (the norm_unit gadget in docs#normalization_monoid looks completely obscure to me, what is it meant to represent?)

Junyan Xu (Oct 11 2022 at 22:00):

The first example is multiplying the inverse of the leading coefficient of a polynomial to make it monic (over a field; over a general normalized_monoid you may still normalize the leading coefficient the same way you normalize it in the base monoid), and in the integers you multiply by the sign; the other examples tend to have trivial group of units so the docs#normalize map is just identity.

Filippo A. E. Nuccio (Oct 11 2022 at 22:03):

Oh, I see. I think I need to understand this better, I will come back if I have any further questions. But thanks so much!

Last updated: Dec 20 2023 at 11:08 UTC