Squarefreeness and relative primality over the fraction field

Let R be a GCD domain with fraction field K. Every nonzero polynomial over K is, up to a unit, the image of a primitive polynomial over R, and by Gauss's lemma a primitive polynomial divides a polynomial over R as soon as it does so over K. Hence a polynomial over K is a unit as soon as every primitive polynomial whose image divides it is a unit (Polynomial.isUnit_of_forall_isPrimitive_map_dvd).

Consequently squarefreeness and relative primality pass from R[X] to K[X] (Squarefree.map_fraction_map, IsRelPrime.map_fraction_map). No primitivity is assumed: a constant factor of a polynomial over R becomes a unit over K, so these implications only lose information. Over K[X], a principal ideal domain, relative primality is the same as IsCoprime, which makes resultants of the images nonzero; this is how the members of a squarefree basis are shown to have nonzero pairwise resultants (Finset.IsSquarefreeBasis.resultant_ne_zero).

These facts complement Mathlib's Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map and Polynomial.IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map.

theorem Polynomial.isUnit_of_forall_isPrimitive_map_dvd {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsGCDMonoid R] [Field K] [Algebra R K] [IsFractionRing R K] {q : Polynomial K} (hq : q ≠ 0) (h : ∀ (q₀ : Polynomial R), q₀.IsPrimitive → map (algebraMap R K) q₀ ∣ q → IsUnit q₀) : IsUnit q

A nonzero polynomial over the fraction field of a GCD domain is a unit as soon as every primitive polynomial whose image divides it is a unit.

theorem Squarefree.map_fraction_map {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsGCDMonoid R] [Field K] [Algebra R K] [IsFractionRing R K] {p : Polynomial R} (hp : Squarefree p) : Squarefree (Polynomial.map (algebraMap R K) p)

A squarefree polynomial over a GCD domain stays squarefree over the fraction field.

theorem IsRelPrime.map_fraction_map {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsGCDMonoid R] [Field K] [Algebra R K] [IsFractionRing R K] {p q : Polynomial R} (h : IsRelPrime p q) : IsRelPrime (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) q)

Relatively prime polynomials over a GCD domain stay relatively prime over the fraction field.