From 7a030ab8eb5d99f05a891dccc49c5b5b90c947d3 Mon Sep 17 00:00:00 2001 From: Paul Lezeau <72892199+Paul-Lez@users.noreply.github.com> Date: Sat, 14 Jan 2023 15:15:21 +0000 Subject: [PATCH] feat(ring_theory/polynomial/gauss_lemma): Prove Gauss's Lemma for integrally closed rings (#18147) In this PR, we prove Gauss's lemma for integrally closed rings. See #18021 and #11523 for previous discussion on the topic. We also show that integrally closed domains are precisely the domains in which Gauss's lemma holds for monic polynomials. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2318021.20generalizing.20theory.20of.20minpoly) Co-authored-by: Junyan Xu Co-authored-by: Paul Lezeau --- src/data/polynomial/splits.lean | 11 ++ src/ring_theory/integral_closure.lean | 4 + src/ring_theory/integrally_closed.lean | 74 +++++++++++- src/ring_theory/polynomial/content.lean | 12 +- .../polynomial/cyclotomic/basic.lean | 2 +- src/ring_theory/polynomial/gauss_lemma.lean | 107 ++++++++++++++---- 6 files changed, 177 insertions(+), 33 deletions(-) diff --git a/src/data/polynomial/splits.lean b/src/data/polynomial/splits.lean index 107a88897b602..a28f5272e3995 100644 --- a/src/data/polynomial/splits.lean +++ b/src/data/polynomial/splits.lean @@ -5,6 +5,7 @@ Authors: Chris Hughes -/ import data.list.prime import data.polynomial.field_division +import data.polynomial.lifts /-! # Split polynomials @@ -311,6 +312,16 @@ begin simp, end +theorem mem_lift_of_splits_of_roots_mem_range (R : Type*) [comm_ring R] [algebra R K] {f : K[X]} + (hs : f.splits (ring_hom.id K)) (hm : f.monic) + (hr : ∀ a ∈ f.roots, a ∈ (algebra_map R K).range) : f ∈ polynomial.lifts (algebra_map R K) := +begin + rw [eq_prod_roots_of_monic_of_splits_id hm hs, lifts_iff_lifts_ring], + refine subring.multiset_prod_mem _ _ (λ P hP, _), + obtain ⟨b, hb, rfl⟩ := multiset.mem_map.1 hP, + exact subring.sub_mem _ (X_mem_lifts _) (C'_mem_lifts (hr _ hb)) +end + section UFD local attribute [instance, priority 10] principal_ideal_ring.to_unique_factorization_monoid diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean index 230d8cbd0aa29..ffc6cb0bbd557 100644 --- a/src/ring_theory/integral_closure.lean +++ b/src/ring_theory/integral_closure.lean @@ -1031,4 +1031,8 @@ variables {R S : Type*} [comm_ring R] [comm_ring S] [is_domain S] [algebra R S] instance : is_domain (integral_closure R S) := infer_instance +theorem roots_mem_integral_closure {f : R[X]} (hf : f.monic) {a : S} + (ha : a ∈ (f.map $ algebra_map R S).roots) : a ∈ integral_closure R S := +⟨f, hf, (eval₂_eq_eval_map _).trans $ (mem_roots $ (hf.map _).ne_zero).1 ha⟩ + end is_domain diff --git a/src/ring_theory/integrally_closed.lean b/src/ring_theory/integrally_closed.lean index c22a258256162..a2483b48c5dc0 100644 --- a/src/ring_theory/integrally_closed.lean +++ b/src/ring_theory/integrally_closed.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Anne Baanen. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Anne Baanen -/ +import field_theory.splitting_field import ring_theory.integral_closure import ring_theory.localization.integral @@ -20,9 +21,13 @@ integral over `R`. A special case of integrally closed domains are the Dedekind * `is_integrally_closed_iff K`, where `K` is a fraction field of `R`, states `R` is integrally closed iff it is the integral closure of `R` in `K` +* `eq_map_mul_C_of_dvd`: 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` -/ -open_locale non_zero_divisors +open_locale non_zero_divisors polynomial + +open polynomial /-- `R` is integrally closed if all integral elements of `Frac(R)` are also elements of `R`. @@ -124,8 +129,33 @@ namespace integral_closure open is_integrally_closed -variables {R : Type*} [comm_ring R] [is_domain R] -variables (K : Type*) [field K] [algebra R K] [is_fraction_ring R K] +variables {R : Type*} [comm_ring R] +variables (K : Type*) [field K] [algebra R K] + +theorem mem_lifts_of_monic_of_dvd_map + {f : R[X]} (hf : f.monic) {g : K[X]} (hg : g.monic) (hd : g ∣ f.map (algebra_map R K)) : + g ∈ lifts (algebra_map (integral_closure R K) K) := +begin + haveI : is_scalar_tower R K g.splitting_field := splitting_field_aux.is_scalar_tower _ _ _, + have := mem_lift_of_splits_of_roots_mem_range (integral_closure R g.splitting_field) + ((splits_id_iff_splits _).2 $ splitting_field.splits g) (hg.map _) + (λ a ha, (set_like.ext_iff.mp (integral_closure R g.splitting_field).range_algebra_map _).mpr $ + roots_mem_integral_closure hf _), + { rw [lifts_iff_coeff_lifts, ←ring_hom.coe_range, subalgebra.range_algebra_map] at this, + refine (lifts_iff_coeff_lifts _).2 (λ n, _), + rw [← ring_hom.coe_range, subalgebra.range_algebra_map], + obtain ⟨p, hp, he⟩ := (set_like.mem_coe.mp (this n)), use [p, hp], + rw [is_scalar_tower.algebra_map_eq R K, coeff_map, ← eval₂_map, eval₂_at_apply] at he, + rw eval₂_eq_eval_map, apply (injective_iff_map_eq_zero _).1 _ _ he, + { apply ring_hom.injective } }, + rw [is_scalar_tower.algebra_map_eq R K _, ← map_map], + refine multiset.mem_of_le (roots.le_of_dvd ((hf.map _).map _).ne_zero _) ha, + { apply_instance }, + { exact map_dvd (algebra_map K g.splitting_field) hd }, + { apply splitting_field_aux.is_scalar_tower }, +end + +variables [is_domain R] [is_fraction_ring R K] variables {L : Type*} [field L] [algebra K L] [algebra R L] [is_scalar_tower R K L] -- Can't be an instance because you need to supply `K`. @@ -137,3 +167,41 @@ begin end end integral_closure + +namespace is_integrally_closed + +open integral_closure + +variables {R : Type*} [comm_ring R] [is_domain R] +variables (K : Type*) [field K] [algebra R K] [is_fraction_ring R K] + +/-- 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` -/ +lemma eq_map_mul_C_of_dvd [is_integrally_closed R] {f : R[X]} (hf : f.monic) + {g : K[X]} (hg : g ∣ f.map (algebra_map R K)) : + ∃ g' : R[X], (g'.map (algebra_map R K)) * (C $ leading_coeff g) = g := +begin + have g_ne_0 : g ≠ 0 := ne_zero_of_dvd_ne_zero (monic.ne_zero $ hf.map (algebra_map R K)) hg, + suffices lem : ∃ g' : R[X], g'.map (algebra_map R K) = g * (C g.leading_coeff⁻¹), + { obtain ⟨g', hg'⟩ := lem, + use g', + rw [hg', mul_assoc, ← C_mul, inv_mul_cancel (leading_coeff_ne_zero.mpr g_ne_0), C_1, mul_one] }, + + have g_mul_dvd : g * (C g.leading_coeff⁻¹) ∣ f.map (algebra_map R K), + { rwa associated.dvd_iff_dvd_left (show associated (g * (C (g.leading_coeff⁻¹))) g, from _), + rw associated_mul_is_unit_left_iff, + exact is_unit_C.mpr (inv_ne_zero $ leading_coeff_ne_zero.mpr g_ne_0).is_unit }, + let algeq := (subalgebra.equiv_of_eq _ _ $ integral_closure_eq_bot R _).trans + (algebra.bot_equiv_of_injective $ is_fraction_ring.injective R $ K), + have : (algebra_map R _).comp algeq.to_alg_hom.to_ring_hom = + (integral_closure R _).to_subring.subtype, + { ext, conv_rhs { rw ← algeq.symm_apply_apply x }, refl }, + have H := ((mem_lifts _ ).1 + (mem_lifts_of_monic_of_dvd_map K hf (monic_mul_leading_coeff_inv g_ne_0) g_mul_dvd)), + refine ⟨map algeq.to_alg_hom.to_ring_hom _, _⟩, + use classical.some H, + rw [map_map, this], + exact classical.some_spec H +end + +end is_integrally_closed diff --git a/src/ring_theory/polynomial/content.lean b/src/ring_theory/polynomial/content.lean index 0a614943c463c..89250e33b1380 100644 --- a/src/ring_theory/polynomial/content.lean +++ b/src/ring_theory/polynomial/content.lean @@ -58,6 +58,9 @@ begin exact (hp 0 (dvd_zero (C 0))).ne_zero rfl, end +lemma is_primitive_of_dvd {p q : R[X]} (hp : is_primitive p) (hq : q ∣ p) : is_primitive q := +λ a ha, is_primitive_iff_is_unit_of_C_dvd.mp hp a (dvd_trans ha hq) + end primitive variables {R : Type*} [comm_ring R] [is_domain R] @@ -382,15 +385,6 @@ begin ring, end -lemma is_primitive.is_primitive_of_dvd {p q : R[X]} (hp : p.is_primitive) (hdvd : q ∣ p) : - q.is_primitive := -begin - rcases hdvd with ⟨r, rfl⟩, - rw [is_primitive_iff_content_eq_one, ← normalize_content, normalize_eq_one, is_unit_iff_dvd_one], - apply dvd.intro r.content, - rwa [is_primitive_iff_content_eq_one, content_mul] at hp, -end - lemma is_primitive.dvd_prim_part_iff_dvd {p q : R[X]} (hp : p.is_primitive) (hq : q ≠ 0) : p ∣ q.prim_part ↔ p ∣ q := diff --git a/src/ring_theory/polynomial/cyclotomic/basic.lean b/src/ring_theory/polynomial/cyclotomic/basic.lean index 7ec13bdc53eed..c983afb708475 100644 --- a/src/ring_theory/polynomial/cyclotomic/basic.lean +++ b/src/ring_theory/polynomial/cyclotomic/basic.lean @@ -840,7 +840,7 @@ end lemma cyclotomic.irreducible_rat {n : ℕ} (hpos : 0 < n) : irreducible (cyclotomic n ℚ) := begin rw [← map_cyclotomic_int], - exact (is_primitive.int.irreducible_iff_irreducible_map_cast (cyclotomic.is_primitive n ℤ)).1 + exact (is_primitive.irreducible_iff_irreducible_map_fraction_map (cyclotomic.is_primitive n ℤ)).1 (cyclotomic.irreducible hpos), end diff --git a/src/ring_theory/polynomial/gauss_lemma.lean b/src/ring_theory/polynomial/gauss_lemma.lean index c0681583f97d5..50fbc6b2bc3fb 100644 --- a/src/ring_theory/polynomial/gauss_lemma.lean +++ b/src/ring_theory/polynomial/gauss_lemma.lean @@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Aaron Anderson -/ import ring_theory.int.basic +import field_theory.splitting_field import ring_theory.localization.integral +import ring_theory.integrally_closed + /-! # Gauss's Lemma @@ -12,12 +15,18 @@ import ring_theory.localization.integral Gauss's Lemma is one of a few results pertaining to irreducibility of primitive polynomials. ## Main Results + - `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 + - `is_integrally_closed_iff'`: + Integrally closed domains are precisely the domains for in which Gauss's lemma holds + for monic polynomials - `polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map`: - A primitive polynomial is irreducible iff it is irreducible in a fraction field. + A primitive polynomial over a GCD domain is irreducible iff it is irreducible in a fraction field - `polynomial.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 divide each other iff they do in a fraction field. + 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 `ℚ`. @@ -25,15 +34,13 @@ Gauss's Lemma is one of a few results pertaining to irreducibility of primitive open_locale non_zero_divisors polynomial -variables {R : Type*} [comm_ring R] [is_domain R] +variables {R : Type*} [comm_ring R] namespace polynomial -section normalized_gcd_monoid -variable [normalized_gcd_monoid R] section -variables {S : Type*} [comm_ring S] [is_domain S] {φ : R →+* S} (hinj : function.injective φ) -variables {f : R[X]} (hf : f.is_primitive) +variables {S : Type*} [comm_ring S] [is_domain S] +variables {φ : R →+* S} (hinj : function.injective φ) {f : R[X]} (hf : f.is_primitive) include hinj hf lemma is_primitive.is_unit_iff_is_unit_map_of_injective : @@ -43,34 +50,93 @@ begin rcases is_unit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩, have hdeg := degree_C u.ne_zero, rw [hu, degree_map_eq_of_injective hinj] at hdeg, - rw [eq_C_of_degree_eq_zero hdeg, is_primitive_iff_content_eq_one, - content_C, normalize_eq_one] at hf, - rwa [eq_C_of_degree_eq_zero hdeg, is_unit_C], + rw [eq_C_of_degree_eq_zero hdeg] at hf ⊢, + exact is_unit_C.mpr (is_primitive_iff_is_unit_of_C_dvd.mp hf (f.coeff 0) dvd_rfl), end lemma is_primitive.irreducible_of_irreducible_map_of_injective (h_irr : irreducible (map φ f)) : irreducible f := begin - refine ⟨λ h, h_irr.not_unit (is_unit.map (map_ring_hom φ) h), _⟩, - intros a b h, - rcases h_irr.is_unit_or_is_unit (by rw [h, polynomial.map_mul]) with hu | hu, - { left, - rwa (hf.is_primitive_of_dvd (dvd.intro _ h.symm)).is_unit_iff_is_unit_map_of_injective hinj }, - right, - rwa (hf.is_primitive_of_dvd (dvd.intro_left _ h.symm)).is_unit_iff_is_unit_map_of_injective hinj + refine ⟨λ h, h_irr.not_unit (is_unit.map (map_ring_hom φ) h), + λ a b h, (h_irr.is_unit_or_is_unit $ by rw [h, polynomial.map_mul]).imp _ _⟩, + all_goals { apply ((is_primitive_of_dvd hf _).is_unit_iff_is_unit_map_of_injective hinj).mpr }, + exacts [(dvd.intro _ h.symm), dvd.intro_left _ h.symm], end end section fraction_map + variables {K : Type*} [field K] [algebra R K] [is_fraction_ring R K] lemma is_primitive.is_unit_iff_is_unit_map {p : R[X]} (hp : p.is_primitive) : is_unit p ↔ is_unit (p.map (algebra_map R K)) := hp.is_unit_iff_is_unit_map_of_injective (is_fraction_ring.injective _ _) +variable [is_domain R] + +section is_integrally_closed + +open is_integrally_closed + +/-- **Gauss's Lemma** for integrally closed domains states that a monic polynomial is irreducible + iff it is irreducible in the fraction field. -/ +theorem monic.irreducible_iff_irreducible_map_fraction_map [is_integrally_closed R] {p : R[X]} + (h : p.monic) : irreducible p ↔ irreducible (p.map $ algebra_map R K) := +begin + /- The ← direction follows from `is_primitive.irreducible_of_irreducible_map_of_injective`. + For the → direction, it is enought to show that if `(p.map $ algebra_map R K) = a * b` and + `a` is not a unit then `b` is a unit -/ + refine ⟨λ hp, irreducible_iff.mpr ⟨hp.not_unit.imp h.is_primitive.is_unit_iff_is_unit_map.mpr, + λ a b H, or_iff_not_imp_left.mpr (λ hₐ, _)⟩, + λ hp, h.is_primitive.irreducible_of_irreducible_map_of_injective + (is_fraction_ring.injective R K) hp⟩, + + obtain ⟨a', ha⟩ := eq_map_mul_C_of_dvd K h (dvd_of_mul_right_eq b H.symm), + obtain ⟨b', hb⟩ := eq_map_mul_C_of_dvd K h (dvd_of_mul_left_eq a H.symm), + + have : a.leading_coeff * b.leading_coeff = 1, + { rw [← leading_coeff_mul, ← H, monic.leading_coeff (h.map $ algebra_map R K)] }, + + rw [← ha, ← hb, mul_comm _ (C b.leading_coeff), mul_assoc, ← mul_assoc (C a.leading_coeff), + ← C_mul, this, C_1, one_mul, ← polynomial.map_mul] at H, + rw [← hb, ← polynomial.coe_map_ring_hom], + refine is_unit.mul + (is_unit.map _ (or.resolve_left (hp.is_unit_or_is_unit _) (show ¬ is_unit a', from _))) + (is_unit_iff_exists_inv'.mpr (exists.intro (C a.leading_coeff) $ by rwa [← C_mul, this, C_1])), + { exact polynomial.map_injective _ (is_fraction_ring.injective R K) H }, + + { by_contra h_contra, + refine hₐ _, + rw [← ha, ← polynomial.coe_map_ring_hom], + exact is_unit.mul (is_unit.map _ h_contra) (is_unit_iff_exists_inv.mpr + (exists.intro (C b.leading_coeff) $ by rwa [← C_mul, this, C_1])) }, +end + +/-- Integrally closed domains are precisely the domains for in which Gauss's lemma holds + for monic polynomials -/ +theorem is_integrally_closed_iff' : is_integrally_closed R ↔ + ∀ p : R[X], p.monic → (irreducible p ↔ irreducible (p.map $ algebra_map R K)) := +begin + split, + { intros hR p hp, letI := hR, exact monic.irreducible_iff_irreducible_map_fraction_map hp }, + { intro H, + refine (is_integrally_closed_iff K).mpr (λ x hx, ring_hom.mem_range.mp $ + minpoly.mem_range_of_degree_eq_one R x _), + rw ← monic.degree_map (minpoly.monic hx) (algebra_map R K), + apply degree_eq_one_of_irreducible_of_root ((H _ $ minpoly.monic hx).mp + (minpoly.irreducible hx)), + rw [is_root, eval_map, ← aeval_def, minpoly.aeval R x] }, +end + +end is_integrally_closed + open is_localization +section normalized_gcd_monoid + +variable [normalized_gcd_monoid R] + lemma is_unit_or_eq_zero_of_is_unit_integer_normalization_prim_part {p : K[X]} (h0 : p ≠ 0) (h : is_unit (integer_normalization R⁰ p).prim_part) : is_unit p := @@ -91,8 +157,8 @@ begin { apply units.ne_zero _ con }, end -/-- **Gauss's Lemma** states that a primitive polynomial is irreducible iff it is irreducible in the - fraction field. -/ +/-- **Gauss's Lemma** for GCD domains states that a primitive polynomial is irreducible iff it is + irreducible in the fraction field. -/ theorem is_primitive.irreducible_iff_irreducible_map_fraction_map {p : R[X]} (hp : p.is_primitive) : irreducible p ↔ irreducible (p.map (algebra_map R K)) := @@ -167,6 +233,8 @@ lemma is_primitive.dvd_iff_fraction_map_dvd_fraction_map {p q : R[X]} ⟨λ ⟨a,b⟩, ⟨a.map (algebra_map R K), b.symm ▸ polynomial.map_mul (algebra_map R K)⟩, λ h, hp.dvd_of_fraction_map_dvd_fraction_map hq h⟩ +end normalized_gcd_monoid + end fraction_map /-- **Gauss's Lemma** for `ℤ` states that a primitive integer polynomial is irreducible iff it is @@ -181,5 +249,4 @@ lemma is_primitive.int.dvd_iff_map_cast_dvd_map_cast (p q : ℤ[X]) (p ∣ q) ↔ (p.map (int.cast_ring_hom ℚ) ∣ q.map (int.cast_ring_hom ℚ)) := hp.dvd_iff_fraction_map_dvd_fraction_map ℚ hq -end normalized_gcd_monoid end polynomial