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 : g ∣ Polynomial.map (algebraMap R K) f) : g ∈ Polynomial.lifts (algebraMap (↥(integralClosure R K)) K)

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 : g ∣ Polynomial.map (algebraMap R K) f) : ∃ (g' : Polynomial R), Polynomial.map (algebraMap R K) g' * 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] {φ : R →+* S} (hinj : Function.Injective ⇑φ) {f : Polynomial R} (hf : f.IsPrimitive) : IsUnit f ↔ IsUnit (Polynomial.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] {φ : R →+* S} (hinj : Function.Injective ⇑φ) {f : Polynomial R} (hf : f.IsPrimitive) (h_irr : Irreducible (Polynomial.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) : IsUnit p ↔ IsUnit (Polynomial.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) : 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] : IsIntegrallyClosed R ↔ ∀ (p : Polynomial R), p.Monic → (Irreducible p ↔ Irreducible (Polynomial.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 : Polynomial.map (algebraMap R K) q ∣ Polynomial.map (algebraMap R K) p) : 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) : Polynomial.map (algebraMap R K) q ∣ Polynomial.map (algebraMap R K) p ↔ 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 : 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) : Irreducible p ↔ Irreducible (Polynomial.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 : Polynomial.map (algebraMap R K) p ∣ Polynomial.map (algebraMap R K) q) : 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) : p ∣ q ↔ Polynomial.map (algebraMap R K) p ∣ Polynomial.map (algebraMap R K) q

theorem Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast {p : Polynomial ℤ} (hp : p.IsPrimitive) : Irreducible p ↔ Irreducible (Polynomial.map (Int.castRingHom ℚ) 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 ℤ) (hp : p.IsPrimitive) (hq : q.IsPrimitive) : p ∣ q ↔ Polynomial.map (Int.castRingHom ℚ) p ∣ Polynomial.map (Int.castRingHom ℚ) q