Documentation

Mathlib.RingTheory.Polynomial.GaussLemma

Gauss's Lemma #

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

Main Results #

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) :
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) :
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)) :
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) :

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

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 : Polynomial R} {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 : Polynomial R} {q : Polynomial R} (hp : p.Monic) (hq : q.Monic) :

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 : Polynomial R} {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 : Polynomial R} {q : Polynomial R} (hp : p.IsPrimitive) (hq : q.IsPrimitive) :

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