chore(field_theory/minpoly/*): replace gcd_monoid.lean by `is_integ…

…rally_closed.lean` and remove results that have been generalized (#18206)

src/algebra/gcd_monoid/integrally_closed.lean

@@ -5,7 +5,7 @@ Authors: Andrew Yang
 -/
 import algebra.gcd_monoid.basic
 import ring_theory.integrally_closed
-import ring_theory.polynomial.eisenstein
+import ring_theory.polynomial.eisenstein.basic
 
 /-!
 

src/field_theory/minpoly/default.lean

@@ -1,3 +1,3 @@
 import field_theory.minpoly.basic
 import field_theory.minpoly.field
-import field_theory.minpoly.gcd_monoid
+import field_theory.minpoly.is_integrally_closed

src/field_theory/minpoly/gcd_monoid.lean → src/field_theory/minpoly/is_integrally_closed.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Riccardo Brasca. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Riccardo Brasca
+Authors: Riccardo Brasca, Paul Lezeau, Junyan Xu
 -/
 import data.polynomial.field_division
 import ring_theory.adjoin_root
@@ -15,23 +15,16 @@ This file specializes the theory of minpoly to the case of an algebra over a GCD
 
 ## Main results
 
- * `gcd_domain_eq_field_fractions`: For GCD domains, the minimal polynomial over the ring is the
-    same as the minimal polynomial over the fraction field.
-
- * `gcd_domain_dvd` : For GCD domains, the minimal polynomial divides any primitive polynomial
-    that has the integral element as root.
-
- * `gcd_domain_unique` : The minimal polynomial of an element `x` is uniquely characterized by
-    its defining property: if there is another monic polynomial of minimal degree that has `x` as a
-    root, then this polynomial is equal to the minimal polynomial of `x`.
-
  * `is_integrally_closed_eq_field_fractions`: For integrally closed domains, the minimal polynomial
     over the ring is the same as the minimal polynomial over the fraction field.
 
-## Todo
+ * `is_integrally_closed_dvd` : For integrally closed domains, the minimal polynomial divides any
+    primitive polynomial that has the integral element as root.
+
+ * `is_integrally_closed_unique` : The minimal polynomial of an element `x` is uniquely
+    characterized by its defining property: if there is another monic polynomial of minimal degree
+    that has `x` as a root, then this polynomial is equal to the minimal polynomial of `x`.
 
- * Remove all results that are now special cases (e.g. we no longer need `gcd_monoid_dvd` since we
-    have `is_integrally_closed_dvd`).
 -/
 
 open_locale classical polynomial
@@ -41,43 +34,11 @@ namespace minpoly
 
 variables {R S : Type*} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S]
 
-
 section
 
 variables (K L : Type*) [field K] [algebra R K] [is_fraction_ring R K] [field L] [algebra R L]
  [algebra S L] [algebra K L] [is_scalar_tower R K L] [is_scalar_tower R S L]
 
-section gcd_domain
-
-variable [normalized_gcd_monoid R]
-
-/-- For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
-over the fraction field. See `minpoly.gcd_domain_eq_field_fractions'` if `S` is already a
-`K`-algebra. -/
-lemma gcd_domain_eq_field_fractions [is_domain S] {s : S} (hs : is_integral R s) :
-  minpoly K (algebra_map S L s) = (minpoly R s).map (algebra_map R K) :=
-begin
-  refine (eq_of_irreducible_of_monic _ _ _).symm,
-  { exact (polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map
-      (polynomial.monic.is_primitive (monic hs))).1 (irreducible hs) },
-   { rw [aeval_map_algebra_map, aeval_algebra_map_apply, aeval, map_zero] },
-  { exact (monic hs).map _ }
-end
-
-/-- For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
-over the fraction field. Compared to `minpoly.gcd_domain_eq_field_fractions`, this version is useful
-if the element is in a ring that is already a `K`-algebra. -/
-lemma gcd_domain_eq_field_fractions' [is_domain S] [algebra K S] [is_scalar_tower R K S]
-  {s : S} (hs : is_integral R s) : minpoly K s = (minpoly R s).map (algebra_map R K) :=
-begin
-  let L := fraction_ring S,
-  rw [← gcd_domain_eq_field_fractions K L hs],
-  refine minpoly.eq_of_algebra_map_eq (is_fraction_ring.injective S L)
-    (is_integral_of_is_scalar_tower hs) rfl
-end
-
-end gcd_domain
-
 variables [is_integrally_closed R]
 
 /-- For integrally closed domains, the minimal polynomial over the ring is the same as the minimal
@@ -105,76 +66,19 @@ begin
     (is_integral_of_is_scalar_tower hs) rfl
 end
 
-/-- For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
-over the fraction field. Compared to `minpoly.is_integrally_closed_eq_field_fractions`, this
-version is useful if the element is in a ring that is not a domain -/
-theorem is_integrally_closed_eq_field_fractions'' [no_zero_smul_divisors S L] {s : S}
-  (hs : is_integral R s) : minpoly K (algebra_map S L s) = map (algebra_map R K) (minpoly R s) :=
-begin
-  --the idea of the proof is the following: since the minpoly of `a` over `Frac(R)` divides the
-  --minpoly of `a` over `R`, it is itself in `R`. Hence its degree is greater or equal to that of
-  --the minpoly of `a` over `R`. But the minpoly of `a` over `Frac(R)` divides the minpoly of a
-  --over `R` in `R[X]` so we are done.
-
-  --a few "trivial" preliminary results to set up the proof
-  have lem0 : minpoly K (algebra_map S L s) ∣ (map (algebra_map R K) (minpoly R s)),
-  { exact dvd_map_of_is_scalar_tower' R K L s },
-
-  have lem1 : is_integral K (algebra_map S L s),
-  { refine is_integral_map_of_comp_eq_of_is_integral (algebra_map R K) _ _ hs,
-    rw [← is_scalar_tower.algebra_map_eq, ← is_scalar_tower.algebra_map_eq] },
-
-  obtain ⟨g, hg⟩ := is_integrally_closed.eq_map_mul_C_of_dvd K (minpoly.monic hs) lem0,
-  rw [(minpoly.monic lem1).leading_coeff, C_1, mul_one] at hg,
-    have lem2 : polynomial.aeval s g = 0,
-  { have := minpoly.aeval K (algebra_map S L s),
-    rw [← hg, ← map_aeval_eq_aeval_map, ← map_zero (algebra_map S L)] at this,
-    { exact no_zero_smul_divisors.algebra_map_injective S L this },
-    { rw [← is_scalar_tower.algebra_map_eq, ← is_scalar_tower.algebra_map_eq] } },
-
-  have lem3 : g.monic,
-  { simpa only [function.injective.monic_map_iff (is_fraction_ring.injective R K), hg]
-      using minpoly.monic lem1 },
-
-  rw [← hg],
-  refine congr_arg _ (eq.symm (polynomial.eq_of_monic_of_dvd_of_nat_degree_le lem3
-    (minpoly.monic hs) _ _)),
-  { rwa [← map_dvd_map _ (is_fraction_ring.injective R K) lem3, hg] },
-  { exact nat_degree_le_nat_degree (minpoly.min R s lem3 lem2) },
-end
-
 end
 
 variables [is_domain S] [no_zero_smul_divisors R S]
 
-lemma gcd_domain_dvd [normalized_gcd_monoid R] {s : S} (hs : is_integral R s) {P : R[X]}
-  (hP : P ≠ 0) (hroot : polynomial.aeval s P = 0) : minpoly R s ∣ P :=
-begin
-  let K := fraction_ring R,
-  let L := fraction_ring S,
-  let P₁ := P.prim_part,
-  suffices : minpoly R s ∣ P₁,
-  { exact dvd_trans this (prim_part_dvd _) },
-  apply (is_primitive.dvd_iff_fraction_map_dvd_fraction_map K (monic hs).is_primitive
-    P.is_primitive_prim_part).2,
-  let y := algebra_map S L s,
-  have hy : is_integral R y := hs.algebra_map,
-  rw [← gcd_domain_eq_field_fractions K L hs],
-  refine dvd _ _ _,
-  rw [aeval_map_algebra_map, aeval_algebra_map_apply, aeval_prim_part_eq_zero hP hroot, map_zero]
-end
-
 variable [is_integrally_closed R]
 
 /-- For integrally closed rings, the minimal polynomial divides any polynomial that has the
   integral element as root. See also `minpoly.dvd` which relaxes the assumptions on `S`
   in exchange for stronger assumptions on `R`. -/
-theorem is_integrally_closed_dvd [nontrivial R] (p : R[X]) {s : S} (hs : is_integral R s) :
-  polynomial.aeval s p = 0 ↔ minpoly R s ∣ p :=
+theorem is_integrally_closed_dvd [nontrivial R] {s : S} (hs : is_integral R s) {p : R[X]}
+  (hp : polynomial.aeval s p = 0) : minpoly R s ∣ p :=
 begin
-  refine ⟨λ hp, _, λ hp, _⟩,
-
-  { let K := fraction_ring R,
+  let K := fraction_ring R,
     let L := fraction_ring S,
     have : minpoly K (algebra_map S L s) ∣ map (algebra_map R K) (p %ₘ (minpoly R s)),
     { rw [map_mod_by_monic _ (minpoly.monic hs), mod_by_monic_eq_sub_mul_div],
@@ -183,30 +87,27 @@ begin
       rw [← is_scalar_tower.algebra_map_eq, ← is_scalar_tower.algebra_map_eq],
 
       apply dvd_mul_of_dvd_left,
-      rw is_integrally_closed_eq_field_fractions'' K L hs,
+      rw is_integrally_closed_eq_field_fractions K L hs,
 
       exact monic.map _ (minpoly.monic hs) },
-    rw [is_integrally_closed_eq_field_fractions'' _ _ hs, map_dvd_map (algebra_map R K)
+    rw [is_integrally_closed_eq_field_fractions _ _ hs, map_dvd_map (algebra_map R K)
       (is_fraction_ring.injective R K) (minpoly.monic hs)] at this,
     rw [← dvd_iff_mod_by_monic_eq_zero (minpoly.monic hs)],
     refine polynomial.eq_zero_of_dvd_of_degree_lt this
       (degree_mod_by_monic_lt p $ minpoly.monic hs),
-      all_goals { apply_instance } },
-
-  { simpa only [ring_hom.mem_ker, ring_hom.coe_comp, coe_eval_ring_hom,
-      coe_map_ring_hom, function.comp_app, eval_map, ← aeval_def] using
-      aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s) }
+      all_goals { apply_instance }
 end
 
+theorem is_integrally_closed_dvd_iff [nontrivial R] {s : S} (hs : is_integral R s) (p : R[X]) :
+  polynomial.aeval s p = 0 ↔  minpoly R s ∣ p :=
+⟨λ hp, is_integrally_closed_dvd hs hp, λ hp, by simpa only [ring_hom.mem_ker, ring_hom.coe_comp,
+  coe_eval_ring_hom, coe_map_ring_hom, function.comp_app, eval_map, ← aeval_def] using
+    aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s)⟩
+
 lemma ker_eval {s : S} (hs : is_integral R s) :
   ((polynomial.aeval s).to_ring_hom : R[X] →+* S).ker = ideal.span ({minpoly R s} : set R[X] ):=
-begin
-  apply le_antisymm; intros p hp,
-  { rwa [ring_hom.mem_ker, alg_hom.to_ring_hom_eq_coe, alg_hom.coe_to_ring_hom,
-      is_integrally_closed_dvd p hs, ← ideal.mem_span_singleton] at hp },
-  { rwa [ring_hom.mem_ker, alg_hom.to_ring_hom_eq_coe, alg_hom.coe_to_ring_hom,
-      is_integrally_closed_dvd p hs, ← ideal.mem_span_singleton] }
-end
+by ext p ; simp_rw [ring_hom.mem_ker, alg_hom.to_ring_hom_eq_coe, alg_hom.coe_to_ring_hom,
+  is_integrally_closed_dvd_iff hs, ← ideal.mem_span_singleton]
 
 /-- If an element `x` is a root of a nonzero polynomial `p`, then the degree of `p` is at least the
 degree of the minimal polynomial of `x`. See also `minpoly.degree_le_of_ne_zero` which relaxes the
@@ -216,7 +117,7 @@ lemma is_integrally_closed.degree_le_of_ne_zero {s : S} (hs : is_integral R s) {
 begin
   rw [degree_eq_nat_degree (minpoly.ne_zero hs), degree_eq_nat_degree hp0],
   norm_cast,
-  exact nat_degree_le_of_dvd ((is_integrally_closed_dvd _ hs).mp hp) hp0
+  exact nat_degree_le_of_dvd ((is_integrally_closed_dvd_iff hs _).mp hp) hp0
 end
 
 /-- The minimal polynomial of an element `x` is uniquely characterized by its defining property:
@@ -255,7 +156,7 @@ begin
   by_cases hPzero : P = 0,
   { simpa [hPzero] using hP.symm },
   rw [← hP, minpoly.to_adjoin_apply', lift_hom_mk,  ← subalgebra.coe_eq_zero,
-    aeval_subalgebra_coe, set_like.coe_mk, is_integrally_closed_dvd _ hx] at hP₁,
+    aeval_subalgebra_coe, set_like.coe_mk, is_integrally_closed_dvd_iff hx] at hP₁,
   obtain ⟨Q, hQ⟩ := hP₁,
   rw [← hP, hQ, ring_hom.map_mul, mk_self, zero_mul],
 end

src/number_theory/cyclotomic/discriminant.lean

@@ -44,9 +44,9 @@ begin
     (λ i j, to_matrix_is_integral H₁ _ _ _ _)
     (λ i j, to_matrix_is_integral H₂ _ _ _ _),
   { exact hζ.is_integral n.pos },
-  { refine minpoly.gcd_domain_eq_field_fractions' _ (hζ.is_integral n.pos) },
+  { refine minpoly.is_integrally_closed_eq_field_fractions' _ (hζ.is_integral n.pos) },
   { exact is_integral_sub (hζ.is_integral n.pos) is_integral_one },
-  { refine minpoly.gcd_domain_eq_field_fractions' _ _,
+  { refine minpoly.is_integrally_closed_eq_field_fractions' _ _,
     exact is_integral_sub (hζ.is_integral n.pos) is_integral_one }
 end
 

src/number_theory/cyclotomic/rat.lean

@@ -5,7 +5,7 @@ Authors: Riccardo Brasca
 -/
 
 import number_theory.cyclotomic.discriminant
-import ring_theory.polynomial.eisenstein
+import ring_theory.polynomial.eisenstein.is_integral
 
 /-!
 # Ring of integers of `p ^ n`-th cyclotomic fields
@@ -105,7 +105,7 @@ begin
     rw [← hz, ← is_scalar_tower.algebra_map_apply],
     exact subalgebra.algebra_map_mem  _ _ },
   { have hmin : (minpoly ℤ B.gen).is_eisenstein_at (submodule.span ℤ {((p : ℕ) : ℤ)}),
-    { have h₁ := minpoly.gcd_domain_eq_field_fractions' ℚ hint,
+    { have h₁ := minpoly.is_integrally_closed_eq_field_fractions' ℚ hint,
       have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp
         (cyclotomic.irreducible_rat (p ^ _).pos),
       rw [is_primitive_root.sub_one_power_basis_gen] at h₁,

src/number_theory/number_field/embeddings.lean

@@ -6,7 +6,7 @@ Authors: Alex J. Best, Xavier Roblot
 
 import analysis.complex.polynomial
 import data.complex.basic
-import field_theory.minpoly.gcd_monoid
+import field_theory.minpoly.is_integrally_closed
 import number_theory.number_field.basic
 
 /-!
@@ -101,7 +101,7 @@ begin
   let C := nat.ceil ((max B 1) ^ (finrank ℚ K) * (finrank ℚ K).choose ((finrank ℚ K) / 2)),
   have := bUnion_roots_finite (algebra_map ℤ K) (finrank ℚ K) (finite_Icc (-C : ℤ) C),
   refine this.subset (λ x hx, _), simp_rw mem_Union,
-  have h_map_ℚ_minpoly := minpoly.gcd_domain_eq_field_fractions' ℚ hx.1,
+  have h_map_ℚ_minpoly := minpoly.is_integrally_closed_eq_field_fractions' ℚ hx.1,
   refine ⟨_, ⟨_, λ i, _⟩, mem_root_set.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩,
   { rw [← (minpoly.monic hx.1).nat_degree_map (algebra_map ℤ ℚ), ← h_map_ℚ_minpoly],
     exact minpoly.nat_degree_le (is_integral_of_is_scalar_tower hx.1) },

src/ring_theory/dedekind_domain/adic_valuation.lean

@@ -6,6 +6,7 @@ Authors: María Inés de Frutos-Fernández
 import ring_theory.dedekind_domain.ideal
 import ring_theory.valuation.extend_to_localization
 import ring_theory.valuation.valuation_subring
+import ring_theory.polynomial.cyclotomic.basic
 import topology.algebra.valued_field
 
 /-!

src/ring_theory/dedekind_domain/selmer_group.lean

@@ -6,6 +6,7 @@ Authors: David Kurniadi Angdinata
 import algebra.hom.equiv.type_tags
 import data.zmod.quotient
 import ring_theory.dedekind_domain.adic_valuation
+import ring_theory.norm
 
 /-!
 # Selmer groups of fraction fields of Dedekind domains

src/ring_theory/is_adjoin_root.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import data.polynomial.algebra_map
-import field_theory.minpoly.gcd_monoid
+import field_theory.minpoly.is_integrally_closed
 import ring_theory.power_basis
 
 /-!
@@ -627,10 +627,10 @@ end is_adjoin_root
 
 namespace is_adjoin_root_monic
 
-lemma minpoly_eq [is_domain R] [is_domain S] [no_zero_smul_divisors R S] [normalized_gcd_monoid R]
+lemma minpoly_eq [is_domain R] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R]
   (h : is_adjoin_root_monic S f) (hirr : irreducible f) :
   minpoly R h.root = f :=
-let ⟨q, hq⟩ := minpoly.gcd_domain_dvd h.is_integral_root h.monic.ne_zero h.aeval_root in
+let ⟨q, hq⟩ := minpoly.is_integrally_closed_dvd h.is_integral_root h.aeval_root in
 symm $ eq_of_monic_of_associated h.monic (minpoly.monic h.is_integral_root) $
 by convert (associated.mul_left (minpoly R h.root) $
     associated_one_iff_is_unit.2 $ (hirr.is_unit_or_is_unit hq).resolve_left $

src/ring_theory/polynomial/cyclotomic/basic.lean

@@ -787,7 +787,7 @@ lemma _root_.is_primitive_root.minpoly_dvd_cyclotomic {n : ℕ} {K : Type*} [fie
   (h : is_primitive_root μ n) (hpos : 0 < n) [char_zero K] :
   minpoly ℤ μ ∣ cyclotomic n ℤ :=
 begin
-  apply minpoly.gcd_domain_dvd (is_integral h hpos) (cyclotomic_ne_zero n ℤ),
+  apply minpoly.is_integrally_closed_dvd (is_integral h hpos),
   simpa [aeval_def, eval₂_eq_eval_map, is_root.def] using is_root_cyclotomic hpos h
 end
 
@@ -816,7 +816,7 @@ lemma cyclotomic_eq_minpoly_rat {n : ℕ} {K : Type*} [field K] {μ : K}
   cyclotomic n ℚ = minpoly ℚ μ :=
 begin
   rw [← map_cyclotomic_int, cyclotomic_eq_minpoly h hpos],
-  exact (minpoly.gcd_domain_eq_field_fractions' _ (is_integral h hpos)).symm
+  exact (minpoly.is_integrally_closed_eq_field_fractions' _ (is_integral h hpos)).symm
 end
 
 /-- `cyclotomic n ℤ` is irreducible. -/
@@ -909,8 +909,7 @@ begin
   { have hpos := nat.mul_pos hzero hp.pos,
     have hprim := complex.is_primitive_root_exp _ hpos.ne.symm,
     rw [cyclotomic_eq_minpoly hprim hpos],
-    refine minpoly.gcd_domain_dvd (hprim.is_integral hpos)
-      ((cyclotomic.monic n ℤ).expand hp.pos).ne_zero _,
+    refine minpoly.is_integrally_closed_dvd (hprim.is_integral hpos) _,
     rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval,
         ← is_root.def, is_root_cyclotomic_iff],
     { convert is_primitive_root.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n),