chore(ring_theory): remove splitting_field dependency from `is_inte…

…grally_closed` (#19137)

The only declarations involving splitting fields were `integral_closure.mem_lifts_of_monic_of_dvd_map` and `is_integrally_closed.eq_map_mul_C_of_dvd`. Both are similar to Gauss' lemma and their only use is to prove Gauss' lemma, so I moved them to that file.

src/ring_theory/integrally_closed.lean

@@ -3,7 +3,6 @@ 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
 
@@ -21,8 +20,6 @@ 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 polynomial
@@ -132,29 +129,6 @@ open is_integrally_closed
 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]
 
@@ -167,41 +141,3 @@ 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/gauss_lemma.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
+import field_theory.splitting_field
 import ring_theory.int.basic
 import ring_theory.localization.integral
 import ring_theory.integrally_closed
@@ -14,6 +15,9 @@ import ring_theory.integrally_closed
 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`: if `R` is integrally closed, `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`
  - `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
@@ -35,6 +39,70 @@ open_locale non_zero_divisors polynomial
 
 variables {R : Type*} [comm_ring R]
 
+section is_integrally_closed
+
+open polynomial
+open integral_closure
+open is_integrally_closed
+
+variables (K : Type*) [field K] [algebra R K]
+
+theorem integral_closure.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]
+
+/-- 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 is_integrally_closed.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 (integral_closure.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
+
 namespace polynomial
 
 section