Finset version of IsRelPrime

Stream: mathlib4

[Boris Bilich]

In PR #33744 I introduced a definition CommonDivisorsAreUnits for a finite set of elements in a monoid. Upon further review, I realized that this is simply the Finset analogue of IsRelPrime. I would therefore like to rename the definition to Finset.IsRelPrime and relocate it to a more appropriate file.

I see two plausible options:

1. Algebra.Divisibility.Units, where IsRelPrime is currently defined;
2. a new file Algebra.Divisibility.Finset.

Which of these would be preferable, or is there a better alternative?

[Yury G. Kudryashov]

Is it just s.Pairwise IsRelPrime? No, it's about having s.gcd = 1 (but w/o EuclideanDomain).

[Junyan Xu]

Finset.gcd does work for NormalizedGCDMonoid, a typeclass UFDs can be equipped with (docs#instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid).

[Yury G. Kudryashov]

But this Finset.IsRelPrime works for any monoid.

[Yury G. Kudryashov]

• I would define it for a Set, not just a Finset. You use no Finset-specific operations in the definition.
• I would underline in the name that it's not about being pairwise rel prime. I'm not sure what's the right way to do it.

[Junyan Xu]

For the purpose of the PR, it seems to me that Finset.gcd_mul_left is good enough.

[Boris Bilich]

Junyan Xu said:

For the purpose of the PR, it seems to me that Finset.gcd_mul_left is good enough.

I followed you advice and discovered that my proof actually works now for [NormalizedGCDMonoid R] in place of [UniqueFactorizationMonoid R]. Therefore I now have a slightly more general theorem that says that the class group of a Normalized GCD Domain is trivial. I suspect that "normalized" can be dropped here but I am not sure how, everything in Mathlib.Algebra.GCDMonoid.Finset is assumed normalized for some reason that is not immediately clear to me.

[Ruben Van de Velde]

Probably because the Std.Commutative lcm instance needs NormalizedGCDMonoid

[Ruben Van de Velde]

So you need it to fold

[Junyan Xu]

Requiring the normUnit to be a monoid homomorphism makes it sometimes impossible to put a docs#NormalizationMonoid structure on a GCD monoid (see mathlib3#17984). For this reason mathlib doesn't know that the polynomial ring over a GCD domain is a GCD domain even though Polynomial.normalizedGcdMonoid is there. I wonder if the condition is really necessary (maybe the normalization map being idempotent is good for most applications?). Now is probably a good time to investigate such questions again.

[Junyan Xu]

Oh the correct condition is probably a normalize map that is a right inverse of the quotient map M → Associates M. I propose to rename the current NormalizationMonoid to StrongNormalizationMonoid and leave the original name for this condition, and provide an instance from the strong one to the weak one. It would be more convenient to attempt the refactoring after #33851.

[Junyan Xu]

In #34179 I continue the work of @Ruben Van de Velde (2021) in mathlib3#9443 and replace the two conditions

  normUnit_mul : ∀ {a b}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
  normUnit_coe_units : ∀ u : αˣ, normUnit u = u⁻¹

in the definition of docs#NormalizationMonoid by

  normUnit_one : normUnit 1 = 1
  normUnit_mul_units {a : α} (u : αˣ) : a ≠ 0 → normUnit (a * u) = u⁻¹ * normUnit a

and rename the old version to StrongNormalizationMonoid. After this change, every cancellative monoid with zero admits a NormalizationMonoid structure, and every GCDMonoid admits a NormalizedGCDMonoid structure. As a consequence, mathlib finally knows that the polynomial ring over a GCD domain is a GCD domain:

Polynomial.instGCDMonoid.{u_1} {R : Type u_1} [CommRing R] [GCDMonoid R] : GCDMonoid R[X]

Even though one can't generalize Multiset/Finset.gcd to GCDMonoids (it's easy to make gcd commutative by choosing a right inverse to docs#Sym2.mk, but associativity is also needed for docs#Multiset.fold and can't be easily achieved without normalization), we can put an arbitrary NormalizedGCDMonoid structure on any GCDMonoid in order to make use of Finset.gcd:

  letI := Classical.arbitrary (NormalizedGCDMonoid R)

and in #33744, this should be enough to establish the trivial class group result to arbitrary GCDMonoids.

[Ruben Van de Velde]

Huh, I completely forgot I tried that

[Junyan Xu]

I found it via Mathlib Changelog when I tried to track down why NormalizationMonoid was so defined :) It was mathlib3#233 in 2018.