Gauss's Lemma #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Gauss's Lemma is one of a few results pertaining to irreducibility of primitive polynomials.
Main Results #
is_integrally_closed.eq_map_mul_C_of_dvd: ifRis integrally closed,K = Frac(R)andg : K[X]divides a monic polynomial with coefficients inR, theng * (C g.leading_coeff⁻¹)has coefficients inRpolynomial.monic.irreducible_iff_irreducible_map_fraction_map: A monic polynomial over an integrally closed domain is irreducible iff it is irreducible in a fraction fieldis_integrally_closed_iff': Integrally closed domains are precisely the domains for in which Gauss's lemma holds for monic polynomialspolynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map: A primitive polynomial over a GCD domain is irreducible iff it is irreducible in a fraction fieldpolynomial.is_primitive.int.irreducible_iff_irreducible_map_cast: A primitive polynomial overℤis irreducible iff it is irreducible overℚ.polynomial.is_primitive.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.is_primitive.int.dvd_iff_map_cast_dvd_map_cast: Two primitive polynomials overℤdivide each other if they do inℚ.
theorem
integral_closure.mem_lifts_of_monic_of_dvd_map
{R : Type u_1}
[comm_ring 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 (algebra_map R K) f) :
g ∈ polynomial.lifts (algebra_map ↥(integral_closure R K) K)
theorem
is_integrally_closed.eq_map_mul_C_of_dvd
{R : Type u_1}
[comm_ring R]
(K : Type u_2)
[field K]
[algebra R K]
[is_domain R]
[is_fraction_ring R K]
[is_integrally_closed R]
{f : polynomial R}
(hf : f.monic)
{g : polynomial K}
(hg : g ∣ polynomial.map (algebra_map R K) f) :
∃ (g' : polynomial R), polynomial.map (algebra_map R K) g' * ⇑polynomial.C g.leading_coeff = g
If K = Frac(R) and g : K[X] divides a monic polynomial with coefficients in R, then
g * (C g.leading_coeff⁻¹) has coefficients in R
theorem
polynomial.is_primitive.is_unit_iff_is_unit_map_of_injective
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
[is_domain S]
{φ : R →+* S}
(hinj : function.injective ⇑φ)
{f : polynomial R}
(hf : f.is_primitive) :
is_unit f ↔ is_unit (polynomial.map φ f)
theorem
polynomial.is_primitive.irreducible_of_irreducible_map_of_injective
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
[is_domain S]
{φ : R →+* S}
(hinj : function.injective ⇑φ)
{f : polynomial R}
(hf : f.is_primitive)
(h_irr : irreducible (polynomial.map φ f)) :
theorem
polynomial.is_primitive.is_unit_iff_is_unit_map
{R : Type u_1}
[comm_ring R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
{p : polynomial R}
(hp : p.is_primitive) :
is_unit p ↔ is_unit (polynomial.map (algebra_map R K) p)
theorem
polynomial.monic.irreducible_iff_irreducible_map_fraction_map
{R : Type u_1}
[comm_ring R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
[is_domain R]
[is_integrally_closed R]
{p : polynomial R}
(h : p.monic) :
irreducible p ↔ irreducible (polynomial.map (algebra_map 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.is_integrally_closed_iff'
{R : Type u_1}
[comm_ring R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
[is_domain R] :
is_integrally_closed R ↔ ∀ (p : polynomial R), p.monic → (irreducible p ↔ irreducible (polynomial.map (algebra_map 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}
[comm_ring R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
[is_domain R]
[is_integrally_closed R]
{p q : polynomial R}
(hp : p.monic)
(hq : q.monic)
(h : polynomial.map (algebra_map R K) q ∣ polynomial.map (algebra_map R K) p) :
q ∣ p
theorem
polynomial.monic.dvd_iff_fraction_map_dvd_fraction_map
{R : Type u_1}
[comm_ring R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
[is_domain R]
[is_integrally_closed R]
{p q : polynomial R}
(hp : p.monic)
(hq : q.monic) :
polynomial.map (algebra_map R K) q ∣ polynomial.map (algebra_map R K) p ↔ q ∣ p
theorem
polynomial.is_unit_or_eq_zero_of_is_unit_integer_normalization_prim_part
{R : Type u_1}
[comm_ring R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
[is_domain R]
[normalized_gcd_monoid R]
{p : polynomial K}
(h0 : p ≠ 0)
(h : is_unit (is_localization.integer_normalization (non_zero_divisors R) p).prim_part) :
is_unit p
theorem
polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map
{R : Type u_1}
[comm_ring R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
[is_domain R]
[normalized_gcd_monoid R]
{p : polynomial R}
(hp : p.is_primitive) :
irreducible p ↔ irreducible (polynomial.map (algebra_map 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.is_primitive.dvd_of_fraction_map_dvd_fraction_map
{R : Type u_1}
[comm_ring R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
[is_domain R]
[normalized_gcd_monoid R]
{p q : polynomial R}
(hp : p.is_primitive)
(hq : q.is_primitive)
(h_dvd : polynomial.map (algebra_map R K) p ∣ polynomial.map (algebra_map R K) q) :
p ∣ q
theorem
polynomial.is_primitive.dvd_iff_fraction_map_dvd_fraction_map
{R : Type u_1}
[comm_ring R]
(K : Type u_2)
[field K]
[algebra R K]
[is_fraction_ring R K]
[is_domain R]
[normalized_gcd_monoid R]
{p q : polynomial R}
(hp : p.is_primitive)
(hq : q.is_primitive) :
p ∣ q ↔ polynomial.map (algebra_map R K) p ∣ polynomial.map (algebra_map R K) q
theorem
polynomial.is_primitive.int.irreducible_iff_irreducible_map_cast
{p : polynomial ℤ}
(hp : p.is_primitive) :
Gauss's Lemma for ℤ states that a primitive integer polynomial is irreducible iff it is
irreducible over ℚ.
theorem
polynomial.is_primitive.int.dvd_iff_map_cast_dvd_map_cast
(p q : polynomial ℤ)
(hp : p.is_primitive)
(hq : q.is_primitive) :
p ∣ q ↔ polynomial.map (int.cast_ring_hom ℚ) p ∣ polynomial.map (int.cast_ring_hom ℚ) q