non-normalizable gcd_monoid

Stream: PR reviews

[Junyan Xu]

#17984

The idea is stated in the module docstring; I guess there also exist examples from commutative rings, but my construction doesn't produce one. If such examples do exist, we'd need to generalize docs#polynomial.normalized_gcd_monoid to account for them; any other examples?

Many lemmas/instances need to moved; I think I know where they should go, but if they are not interesting enough they can stay, and that's the main reason why I ask for review.

I'd like to tag @Ruben Van de Velde, since you removed normalization from gcd_domain in #9443.

[Riccardo Brasca]

I don't know if it's really impossible to find a normalization, but for rings of integers of number fields it seems quite unnatural if the group of units is big.

[Ruben Van de Velde]

It's been a while since I touched that :)

It does seem like some of the results from the start of your file could move into mathlib proper, though I'm not quite sure where

[Junyan Xu]

For noetherian rings like rings of integers, being a gcd_monoid is equivalent to being UFD, and docs#unique_factorization_monoid.normalization_monoid shows there aren't counterexamples when class number is 1, but I don't see immediately whether there can be class number >1 examples that don't admit normalization_monoid structures.

[Riccardo Brasca]

Being UFD is equivalent to being a PID in this case

[Riccardo Brasca]

I am a little confused and with the phone is difficult to read the source, but how we define the normalization on a UFD?

[Riccardo Brasca]

Ah, we just choose a random one

[Riccardo Brasca]

Still using that def for ring of integers can be quite a pain, since for the integers it creates a diamond

[Junyan Xu]

Yeah I proposed using nonempty gcd_monoid etc. in this thread. Maybe we should use nonempty gcd_monoid unless the statement requires gcd_monoid, like how we use finite instead of fintype. Maybe nonempty normalized_gcd_monoid is required sometimes, but I guess most thoerems about normalized_gcd_monoid can simply be generalized to gcd_monoid. I don't know about any interesting theorems that requires nonempty normalization_monoid because it seems to be some mathlib artifact that doesn't appear in math textbooks.

[Junyan Xu]

And I think I can now prove that any ring of integers can be normalized: the group completion of the monoid of associates (minus zero) embeds into the group of fractional ideals, which is freely generated by the prime ideals, and any subgroup of a free abelian group is itself free, hence projective. Then you should be able to apply docs#normalization_monoid_of_monoid_hom_right_inverse.

[Junyan Xu]

Actually I think docs#hahn_series.comm_ring over the M in my PR probably serves as a comm_ring counterexample ...

[Riccardo Brasca]

I agree it's very weird that we normalization gcd contains data. I would be very surprised if something depends on the actual choice and not only on the existence of a normalization

[Eric Wieser]

If so, we should have a normalization_monoid.ext in the style of docs#group.ext

[Junyan Xu]

How could we do that? The normalization data isn't determined by the multiplication (it's basically the choice of a splitting of the nonzero elements as a product of the associates with the unit group), while all the data fields of a group (inv, npow, zpow, etc.) are determined by the multiplication. If the result doesn't depend on the choice, I proposed that we should use nonempty (normalized_gcd_monoid α) instead, and I think nonempty (gcd_monoid α) already suffices for all interesting results. When the unit group is trivial, we do have docs#subsingleton_normalized_gcd_monoid_of_unique_units and docs#unique_normalization_monoid_of_unique_units.