Gauss's Lemma

Gauss's Lemma is one of a few results pertaining to irreducibility of primitive polynomials.

Main Results

• IsIntegrallyClosed.eq_map_mul_C_of_dvd: if R is integrally closed, K = Frac(R) and g : K[X] divides a monic polynomial with coefficients in R, then g * (C g.leadingCoeff⁻¹) has coefficients in R
• Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map: A monic polynomial over an integrally closed domain is irreducible iff it is irreducible in a fraction field
• isIntegrallyClosed_iff': Integrally closed domains are precisely the domains for in which Gauss's lemma holds for monic polynomials
• Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map: A primitive polynomial over a GCD domain is irreducible iff it is irreducible in a fraction field
• Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast: A primitive polynomial over ℤ is irreducible iff it is irreducible over ℚ.
• Polynomial.IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map: Two primitive polynomials over a GCD domain divide each other iff they do in a fraction field.
• Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast: Two primitive polynomials over ℤ divide each other if they do in ℚ.

theorem integralClosure.mem_lifts_of_monic_of_dvd_map {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] {f : Polynomial R} (hf : f.Monic) {g : Polynomial K} (hg : g.Monic) (hd : Dvd.dvd g (Polynomial.map (algebraMap R K) f)) : Membership.mem (Polynomial.lifts (algebraMap (Subtype fun (x : K) => Membership.mem (integralClosure R K) x) K)) g

theorem IsIntegrallyClosed.eq_map_mul_C_of_dvd {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsIntegrallyClosed R] {f : Polynomial R} (hf : f.Monic) {g : Polynomial K} (hg : Dvd.dvd g (Polynomial.map (algebraMap R K) f)) : Exists fun (g' : Polynomial R) => Eq (HMul.hMul (Polynomial.map (algebraMap R K) g') (DFunLike.coe Polynomial.C g.leadingCoeff)) g

If K = Frac(R) and g : K[X] divides a monic polynomial with coefficients in R, then g * (C g.leadingCoeff⁻¹) has coefficients in R

theorem Polynomial.IsPrimitive.isUnit_iff_isUnit_map_of_injective {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [IsDomain S] {φ : RingHom R S} (hinj : Function.Injective (DFunLike.coe φ)) {f : Polynomial R} (hf : f.IsPrimitive) : Iff (IsUnit f) (IsUnit (map φ f))

theorem Polynomial.IsPrimitive.irreducible_of_irreducible_map_of_injective {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [IsDomain S] {φ : RingHom R S} (hinj : Function.Injective (DFunLike.coe φ)) {f : Polynomial R} (hf : f.IsPrimitive) (h_irr : Irreducible (map φ f)) : Irreducible f

theorem Polynomial.IsPrimitive.isUnit_iff_isUnit_map {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {p : Polynomial R} (hp : p.IsPrimitive) : Iff (IsUnit p) (IsUnit (map (algebraMap R K) p))

theorem Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsIntegrallyClosed R] {p : Polynomial R} (h : p.Monic) : Iff (Irreducible p) (Irreducible (Polynomial.map (algebraMap R K) p))

Gauss's Lemma for integrally closed domains states that a monic polynomial is irreducible iff it is irreducible in the fraction field.

theorem Polynomial.isIntegrallyClosed_iff' {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] : Iff (IsIntegrallyClosed R) (∀ (p : Polynomial R), p.Monic → Iff (Irreducible p) (Irreducible (map (algebraMap R K) p)))

Integrally closed domains are precisely the domains for in which Gauss's lemma holds for monic polynomials

theorem Polynomial.Monic.dvd_of_fraction_map_dvd_fraction_map {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsIntegrallyClosed R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (h : Dvd.dvd (Polynomial.map (algebraMap R K) q) (Polynomial.map (algebraMap R K) p)) : Dvd.dvd q p

theorem Polynomial.Monic.dvd_iff_fraction_map_dvd_fraction_map {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsIntegrallyClosed R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) : Iff (Dvd.dvd (Polynomial.map (algebraMap R K) q) (Polynomial.map (algebraMap R K) p)) (Dvd.dvd q p)

theorem Polynomial.isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial K} (h0 : Ne p 0) (h : IsUnit (IsLocalization.integerNormalization (nonZeroDivisors R) p).primPart) : IsUnit p

theorem Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} (hp : p.IsPrimitive) : Iff (Irreducible p) (Irreducible (map (algebraMap R K) p))

Gauss's Lemma for GCD domains states that a primitive polynomial is irreducible iff it is irreducible in the fraction field.

theorem Polynomial.IsPrimitive.dvd_of_fraction_map_dvd_fraction_map {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q.IsPrimitive) (h_dvd : Dvd.dvd (map (algebraMap R K) p) (map (algebraMap R K) q)) : Dvd.dvd p q

theorem Polynomial.IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q.IsPrimitive) : Iff (Dvd.dvd p q) (Dvd.dvd (map (algebraMap R K) p) (map (algebraMap R K) q))

theorem Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast {p : Polynomial Int} (hp : p.IsPrimitive) : Iff (Irreducible p) (Irreducible (map (Int.castRingHom Rat) p))

Gauss's Lemma for ℤ states that a primitive integer polynomial is irreducible iff it is irreducible over ℚ.

theorem Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (p q : Polynomial Int) (hp : p.IsPrimitive) (hq : q.IsPrimitive) : Iff (Dvd.dvd p q) (Dvd.dvd (map (Int.castRingHom Rat) p) (map (Int.castRingHom Rat) q))