[Merged by Bors] - feat(ring_theory/*): generalise minpoly.dvd to integrally closed rings

src/data/polynomial/algebra_map.lean

@@ -251,6 +251,22 @@ lemma coeff_zero_eq_aeval_zero' (p : R[X]) :
   algebra_map R A (p.coeff 0) = aeval (0 : A) p :=
 by simp [aeval_def]
 
+lemma map_aeval_eq_aeval_map {S T U : Type*} [comm_semiring S] [comm_semiring T] [semiring U]
+  [algebra R S] [algebra T U] {φ : R →+* T} {ψ : S →+* U}
+  (h : (algebra_map T U).comp φ = ψ.comp (algebra_map R S)) (p : R[X]) (a : S) :
+  ψ (aeval a p) = aeval (ψ a) (p.map φ) :=
+begin
+  conv_rhs {rw [aeval_def, ← eval_map]},
+  rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map],
+end
+
+lemma aeval_eq_zero_of_dvd_aeval_eq_zero [comm_semiring S] [comm_semiring T] [algebra S T]
+  {p q : S[X]} (h₁ : p ∣ q) {a : T} (h₂ : aeval a p = 0) : aeval a q = 0 :=
+begin
+  rw [aeval_def, ← eval_map] at h₂ ⊢,
+  exact eval_eq_zero_of_dvd_of_eval_eq_zero (polynomial.map_dvd (algebra_map S T) h₁) h₂,
+end
+
 variable (R)
 
 theorem _root_.algebra.adjoin_singleton_eq_range_aeval (x : A) :

src/data/polynomial/monic.lean

@@ -346,6 +346,9 @@ begin
   rw [← leading_coeff_of_injective hf, hp.leading_coeff, f.map_one]
 end
 
+theorem _root_.function.injective.monic_map_iff {p : R[X]} : p.monic ↔ (p.map f).monic :=
+⟨monic.map _, polynomial.monic_of_injective hf⟩
+
 end injective
 
 end semiring

src/data/polynomial/ring_division.lean

@@ -163,6 +163,34 @@ begin
   exact degree_le_mul_left p h2.2,
 end
 
+lemma eq_zero_of_dvd_of_degree_lt {p q : R[X]} (h₁ : p ∣ q) (h₂ : degree q < degree p) :
+  q = 0 :=
+begin
+  by_contradiction hc,
+  exact (lt_iff_not_ge _ _ ).mp h₂ (degree_le_of_dvd h₁ hc),
+end
+
+lemma eq_zero_of_dvd_of_nat_degree_lt {p q : R[X]} (h₁ : p ∣ q) (h₂ : nat_degree q < nat_degree p) :
+  q = 0 :=
+begin
+  by_contradiction hc,
+  exact (lt_iff_not_ge _ _ ).mp h₂ (nat_degree_le_of_dvd h₁ hc),
+end
+
+theorem not_dvd_of_degree_lt {p q : R[X]} (h0 : q ≠ 0)
+  (hl : q.degree < p.degree) : ¬ p ∣ q :=
+begin
+  by_contra hcontra,
+  exact h0 (eq_zero_of_dvd_of_degree_lt hcontra hl),
+end
+
+theorem not_dvd_of_nat_degree_lt {p q : R[X]} (h0 : q ≠ 0)
+  (hl : q.nat_degree < p.nat_degree) : ¬ p ∣ q :=
+begin
+  by_contra hcontra,
+  exact h0 (eq_zero_of_dvd_of_nat_degree_lt hcontra hl),
+end
+
 /-- This lemma is useful for working with the `int_degree` of a rational function. -/
 lemma nat_degree_sub_eq_of_prod_eq {p₁ p₂ q₁ q₂ : R[X]} (hp₁ : p₁ ≠ 0) (hq₁ : q₁ ≠ 0)
   (hp₂ : p₂ ≠ 0) (hq₂ : q₂ ≠ 0) (h_eq : p₁ * q₂ = p₂ * q₁) :

src/field_theory/minpoly/field.lean

@@ -84,6 +84,16 @@ lemma dvd_map_of_is_scalar_tower (A K : Type*) {R : Type*} [comm_ring A] [field
   minpoly K x ∣ (minpoly A x).map (algebra_map A K) :=
 by { refine minpoly.dvd K x _, rw [aeval_map_algebra_map, minpoly.aeval] }
 
+lemma dvd_map_of_is_scalar_tower' (R : Type*) {S : Type*} (K L : Type*) [comm_ring R]
+  [comm_ring S] [field K] [comm_ring L] [algebra R S] [algebra R K] [algebra S L] [algebra K L]
+  [algebra R L] [is_scalar_tower R K L] [is_scalar_tower R S L] (s : S):
+  minpoly K (algebra_map S L s) ∣ (map (algebra_map R K) (minpoly R s)) :=
+begin
+  apply minpoly.dvd K (algebra_map S L s),
+  rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero],
+  rw [← is_scalar_tower.algebra_map_eq, ← is_scalar_tower.algebra_map_eq]
+end
+
 /-- If `y` is a conjugate of `x` over a field `K`, then it is a conjugate over a subring `R`. -/
 lemma aeval_of_is_scalar_tower (R : Type*) {K T U : Type*} [comm_ring R] [field K] [comm_ring T]
   [algebra R K] [algebra K T] [algebra R T] [is_scalar_tower R K T]

src/field_theory/minpoly/gcd_monoid.lean

@@ -24,27 +24,37 @@ This file specializes the theory of minpoly to the case of an algebra over a GCD
  * `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
+
+ * 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
 open polynomial set function minpoly
 
 namespace minpoly
 
-variables {R S : Type*} [comm_ring R] [comm_ring S] [is_domain R] [is_domain S] [algebra R S]
+variables {R S : Type*} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S]
 
-section gcd_domain
 
-variables (K L : Type*) [normalized_gcd_monoid R] [field K] [algebra R K] [is_fraction_ring R K]
-  [field L] [algebra S L] [algebra K L] [algebra R L] [is_scalar_tower R K L]
-  [is_scalar_tower R S L] {s : S} (hs : is_integral 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
 
-include hs
+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 :
+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,
@@ -57,21 +67,88 @@ 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' [algebra K S] [is_scalar_tower R K S] :
-  minpoly K s = (minpoly R s).map (algebra_map R K) :=
+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
 
-variable [no_zero_smul_divisors R S]
+end gcd_domain
+
+variables [is_integrally_closed R]
+
+/-- For integrally closed domains, the minimal polynomial over the ring is the same as the minimal
+polynomial over the fraction field. See `minpoly.is_integrally_closed_eq_field_fractions'` if
+`S` is already a `K`-algebra. -/
+theorem is_integrally_closed_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.monic.irreducible_iff_irreducible_map_fraction_map
+      (monic hs)).1 (irreducible hs) },
+   { rw [aeval_map_algebra_map, aeval_algebra_map_apply, aeval, map_zero] },
+  { exact (monic hs).map _ }
+end
+
+/-- For integrally closed 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 already a `K`-algebra. -/
+theorem is_integrally_closed_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 [← is_integrally_closed_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
+
+/-- 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]
 
-/-- For GCD domains, the minimal polynomial divides any primitive 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`. -/
-lemma gcd_domain_dvd {P : R[X]} (hP : P ≠ 0) (hroot : polynomial.aeval s P = 0) : minpoly R s ∣ P :=
+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,
@@ -87,47 +164,88 @@ begin
   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 :=
+begin
+  refine ⟨λ hp, _, λ hp, _⟩,
+
+  { 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],
+      refine dvd_sub (minpoly.dvd K (algebra_map S L s) _) _,
+      rw [← map_aeval_eq_aeval_map, hp, map_zero],
+      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,
+
+      exact monic.map _ (minpoly.monic hs) },
+    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) }
+end
+
+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
+
 /-- 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
 assumptions on `S` in exchange for stronger assumptions on `R`. -/
-lemma gcd_domain_degree_le_of_ne_zero {p : R[X]} (hp0 : p ≠ 0) (hp : polynomial.aeval s p = 0) :
-  degree (minpoly R s) ≤ degree p :=
+lemma is_integrally_closed.degree_le_of_ne_zero {s : S} (hs : is_integral R s) {p : R[X]}
+  (hp0 : p ≠ 0) (hp : polynomial.aeval s p = 0) : degree (minpoly R s) ≤ degree p :=
 begin
   rw [degree_eq_nat_degree (minpoly.ne_zero hs), degree_eq_nat_degree hp0],
   norm_cast,
-  exact nat_degree_le_of_dvd (gcd_domain_dvd hs hp0 hp) hp0
+  exact nat_degree_le_of_dvd ((is_integrally_closed_dvd _ hs).mp hp) hp0
 end
 
-omit hs
-
 /-- 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`. See also `minpoly.unique` which relaxes the
 assumptions on `S` in exchange for stronger assumptions on `R`. -/
-lemma gcd_domain_unique {P : R[X]} (hmo : P.monic) (hP : polynomial.aeval s P = 0)
+lemma is_integrally_closed.minpoly.unique {s : S} {P : R[X]} (hmo : P.monic)
+  (hP : polynomial.aeval s P = 0)
   (Pmin : ∀ Q : R[X], Q.monic → polynomial.aeval s Q = 0 → degree P ≤ degree Q) :
   P = minpoly R s :=
 begin
   have hs : is_integral R s := ⟨P, hmo, hP⟩,
   symmetry, apply eq_of_sub_eq_zero,
   by_contra hnz,
-  have := gcd_domain_degree_le_of_ne_zero hs hnz (by simp [hP]),
+  have := is_integrally_closed.degree_le_of_ne_zero hs hnz (by simp [hP]),
   contrapose! this,
   refine degree_sub_lt _ (ne_zero hs) _,
   { exact le_antisymm (min R s hmo hP)
       (Pmin (minpoly R s) (monic hs) (aeval R s)) },
   { rw [(monic hs).leading_coeff, hmo.leading_coeff] }
 end
 
-end gcd_domain
-
 section adjoin_root
 
 noncomputable theory
 
 open algebra polynomial adjoin_root
 
-variables {R} {x : S} [normalized_gcd_monoid R] [no_zero_smul_divisors R S]
+variables {R} {x : S}
 
 lemma to_adjoin.injective (hx : is_integral R x) :
   function.injective (minpoly.to_adjoin R x) :=
@@ -136,14 +254,10 @@ begin
   obtain ⟨P, hP⟩ := mk_surjective (minpoly.monic hx) P₁,
   by_cases hPzero : P = 0,
   { simpa [hPzero] using hP.symm },
-  have hPcont : P.content ≠ 0 := λ h, hPzero (content_eq_zero_iff.1 h),
-  rw [← hP, minpoly.to_adjoin_apply', lift_hom_mk, ← subalgebra.coe_eq_zero,
-    aeval_subalgebra_coe, set_like.coe_mk, P.eq_C_content_mul_prim_part, aeval_mul, aeval_C] at hP₁,
-  replace hP₁ := eq_zero_of_ne_zero_of_mul_left_eq_zero
-    ((map_ne_zero_iff _ (no_zero_smul_divisors.algebra_map_injective R S)).2 hPcont) hP₁,
-  obtain ⟨Q, hQ⟩ := minpoly.gcd_domain_dvd hx P.is_primitive_prim_part.ne_zero hP₁,
-  rw [P.eq_C_content_mul_prim_part] at hP,
-  simpa [hQ] 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₁,
+  obtain ⟨Q, hQ⟩ := hP₁,
+  rw [← hP, hQ, ring_hom.map_mul, mk_self, zero_mul],
 end
 
 /-- The algebra isomorphism `adjoin_root (minpoly R x) ≃ₐ[R] adjoin R x` -/

src/ring_theory/integral_closure.lean

@@ -125,6 +125,18 @@ begin
     aeval_alg_hom_apply, aeval_map_algebra_map, aeval_def, hP.2, _root_.map_zero]
 end
 
+lemma is_integral_map_of_comp_eq_of_is_integral {R S T U : Type*} [comm_ring R] [comm_ring S]
+  [comm_ring T] [comm_ring U] [algebra R S] [algebra T U] (φ : R →+* T) (ψ : S →+* U)
+  (h : (algebra_map T U).comp φ = ψ.comp (algebra_map R S)) {a : S} (ha : is_integral R a) :
+  is_integral T (ψ a) :=
+begin
+  rw [is_integral, ring_hom.is_integral_elem] at ⊢ ha,
+  obtain ⟨p, hp⟩ := ha,
+  refine ⟨p.map φ, hp.left.map _, _⟩,
+  rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply,
+    eval_map, hp.right, ring_hom.map_zero],
+end
+
 theorem is_integral_alg_hom_iff {A B : Type*} [ring A] [ring B] [algebra R A] [algebra R B]
   (f : A →ₐ[R] B) (hf : function.injective f) {x : A} : is_integral R (f x) ↔ is_integral R x :=
 begin

src/ring_theory/polynomial/gauss_lemma.lean

@@ -129,6 +129,22 @@ begin
     rw [is_root, eval_map, ← aeval_def, minpoly.aeval R x] },
 end
 
+theorem monic.dvd_of_fraction_map_dvd_fraction_map [is_integrally_closed R] {p q : R[X]}
+  (hp : p.monic ) (hq : q.monic) (h : q.map (algebra_map R K) ∣ p.map (algebra_map R K)) : q ∣ p :=
+begin
+  obtain ⟨r, hr⟩ := h,
+  obtain ⟨d', hr'⟩ := is_integrally_closed.eq_map_mul_C_of_dvd K hp (dvd_of_mul_left_eq _ hr.symm),
+  rw [monic.leading_coeff, C_1, mul_one] at hr',
+  rw [← hr', ← polynomial.map_mul] at hr,
+  exact dvd_of_mul_right_eq _ (polynomial.map_injective _ (is_fraction_ring.injective R K) hr.symm),
+   { exact monic.of_mul_monic_left (hq.map (algebra_map R K)) (by simpa [←hr] using hp.map _) },
+end
+
+theorem monic.dvd_iff_fraction_map_dvd_fraction_map [is_integrally_closed R] {p q : R[X]}
+  (hp : p.monic ) (hq : q.monic) : q.map (algebra_map R K) ∣ p.map (algebra_map R K) ↔ q ∣ p :=
+⟨λ h, hp.dvd_of_fraction_map_dvd_fraction_map hq h,
+  λ ⟨a,b⟩, ⟨a.map (algebra_map R K), b.symm ▸ polynomial.map_mul (algebra_map R K)⟩⟩
+
 end is_integrally_closed
 
 open is_localization