feat(ring_theory/polynomial/gauss_lemma): Prove Gauss's Lemma for int…

…egrally 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 <junyanxu.math@gmail.com>




Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>

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

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

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

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

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
 

src/ring_theory/polynomial/gauss_lemma.lean

@@ -4,36 +4,43 @@ 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
 
 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 `ℚ`.
 
 -/
 
 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