feat(field_theory/minpoly): generalize statements about GCD domains (#…

…14979)

Currently, the statements about the minimal polynomial over a GCD domain `R` require the element to be in a `K`-algebra, where `K` is the fraction field of `R`. We remove this assumption.

From flt-regular.

src/field_theory/minpoly.lean

@@ -262,8 +262,9 @@ variables {x : B}
 
 variables (A x)
 
-/-- 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`. -/
+/-- 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 `gcd_domain_degree_le_of_ne_zero` which relaxes
+the assumptions on `A` in exchange for stronger assumptions on `B`. -/
 lemma degree_le_of_ne_zero
   {p : A[X]} (pnz : p ≠ 0) (hp : polynomial.aeval x p = 0) :
   degree (minpoly A x) ≤ degree p :=
@@ -275,8 +276,9 @@ lemma ne_zero_of_finite_field_extension (e : B) [finite_dimensional A B] : minpo
 minpoly.ne_zero $ is_integral_of_noetherian (is_noetherian.iff_fg.2 infer_instance) _
 
 /-- 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`. -/
+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.gcd_unique` which relaxes the
+assumptions on `A` in exchange for stronger assumptions on `B`. -/
 lemma unique {p : A[X]}
   (pmonic : p.monic) (hp : polynomial.aeval x p = 0)
   (pmin : ∀ q : A[X], q.monic → polynomial.aeval x q = 0 → degree p ≤ degree q) :
@@ -293,8 +295,9 @@ begin
       (pmin (minpoly A x) (monic hx) (aeval A x)) }
 end
 
-/-- If an element `x` is a root of a polynomial `p`,
-then the minimal polynomial of `x` divides `p`. -/
+/-- If an element `x` is a root of a polynomial `p`, then the minimal polynomial of `x` divides `p`.
+See also `minpoly.gcd_domain_dvd` which relaxes the assumptions on `A` in exchange for stronger
+assumptions on `B`. -/
 lemma dvd {p : A[X]} (hp : polynomial.aeval x p = 0) : minpoly A x ∣ p :=
 begin
   by_cases hp0 : p = 0,
@@ -386,38 +389,91 @@ by simpa [sub_eq_add_neg] using add_algebra_map hx (-a)
 
 section gcd_domain
 
+variables {R S : Type*} (K L : Type*) [comm_ring R] [is_domain R] [normalized_gcd_monoid R]
+  [field K] [comm_ring S] [is_domain S] [algebra R K] [is_fraction_ring R K] [algebra R S] [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)
+
+include hs
+
 /-- For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
-over the fraction field. -/
-lemma gcd_domain_eq_field_fractions {A R : Type*} (K : Type*) [comm_ring A] [is_domain A]
-  [normalized_gcd_monoid A] [field K]
-  [comm_ring R] [is_domain R] [algebra A K] [is_fraction_ring A K]
-  [algebra K R] [algebra A R] [is_scalar_tower A K R] {x : R} (hx : is_integral A x) :
-  minpoly K x = (minpoly A x).map (algebra_map A K) :=
+over the fraction field. See `minpoly.gcd_domain_eq_field_fractions'` if `S` is already a
+`K`-algebra. -/
+lemma gcd_domain_eq_field_fractions :
+  minpoly K (algebra_map S L s) = (minpoly R s).map (algebra_map R K) :=
 begin
-  symmetry,
-  refine eq_of_irreducible_of_monic _ _ _,
+  refine (eq_of_irreducible_of_monic _ _ _).symm,
   { exact (polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map
-      (polynomial.monic.is_primitive (monic hx))).1 (irreducible hx) },
-  { have htower := is_scalar_tower.aeval_apply A K R x (minpoly A x),
-    rwa [aeval, eq_comm] at htower },
-  { exact (monic hx).map _ }
+      (polynomial.monic.is_primitive (monic hs))).1 (irreducible hs) },
+   { rw [aeval_map, aeval_def, is_scalar_tower.algebra_map_eq R S L, ← eval₂_map, eval₂_at_apply,
+      eval_map, ← aeval_def, 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' [algebra K S] [is_scalar_tower R K 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]
+
 /-- For GCD domains, the minimal polynomial divides any primitive polynomial that has the integral
-element as root. -/
-lemma gcd_domain_dvd {A R : Type*} (K : Type*)
-  [comm_ring A] [is_domain A] [normalized_gcd_monoid A] [field K]
-  [comm_ring R] [is_domain R] [algebra A K]
-  [is_fraction_ring A K] [algebra K R] [algebra A R] [is_scalar_tower A K R]
-  {x : R} (hx : is_integral A x)
-  {P : A[X]} (hprim : is_primitive P) (hroot : polynomial.aeval x P = 0) :
-  minpoly A x ∣ P :=
+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 :=
 begin
-  apply (is_primitive.dvd_iff_fraction_map_dvd_fraction_map K
-    (monic.is_primitive (monic hx)) hprim).2,
-  rw ← gcd_domain_eq_field_fractions K hx,
+  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 _ _ _,
-  rwa ← is_scalar_tower.aeval_apply
+  rw [aeval_map, aeval_def, is_scalar_tower.algebra_map_eq R S L, ← eval₂_map, eval₂_at_apply,
+    eval_map, ← aeval_def, aeval_prim_part_eq_zero hP hroot, map_zero]
+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 :=
+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
+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)
+  (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]),
+  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

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.gcd_domain_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.gcd_domain_eq_field_fractions' _ _,
     exact is_integral_sub (hζ.is_integral n.pos) is_integral_one }
 end
 

src/number_theory/cyclotomic/rat.lean

@@ -104,7 +104,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.gcd_domain_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/ring_theory/polynomial/content.lean

@@ -275,6 +275,28 @@ end
 lemma prim_part_dvd (p : R[X]) : p.prim_part ∣ p :=
 dvd.intro_left (C p.content) p.eq_C_content_mul_prim_part.symm
 
+lemma aeval_prim_part_eq_zero {S : Type*} [ring S] [is_domain S] [algebra R S]
+  [no_zero_smul_divisors R S] {p : R[X]} {s : S} (hpzero : p ≠ 0) (hp : aeval s p = 0) :
+  aeval s p.prim_part = 0 :=
+begin
+  rw [eq_C_content_mul_prim_part p, map_mul, aeval_C] at hp,
+  have hcont : p.content ≠ 0 := λ h, hpzero (content_eq_zero_iff.1 h),
+  replace hcont := function.injective.ne (no_zero_smul_divisors.algebra_map_injective R S) hcont,
+  rw [map_zero] at hcont,
+  exact eq_zero_of_ne_zero_of_mul_left_eq_zero hcont hp
+end
+
+lemma eval₂_prim_part_eq_zero {S : Type*} [comm_ring S] [is_domain S] {f : R →+* S}
+  (hinj : function.injective f) {p : R[X]} {s : S} (hpzero : p ≠ 0)
+  (hp : eval₂ f s p = 0) : eval₂ f s p.prim_part = 0 :=
+begin
+  rw [eq_C_content_mul_prim_part p, eval₂_mul, eval₂_C] at hp,
+  have hcont : p.content ≠ 0 := λ h, hpzero (content_eq_zero_iff.1 h),
+  replace hcont := function.injective.ne hinj hcont,
+  rw [map_zero] at hcont,
+  exact eq_zero_of_ne_zero_of_mul_left_eq_zero hcont hp
+end
+
 end prim_part
 
 lemma gcd_content_eq_of_dvd_sub {a : R} {p q : R[X]} (h : C a ∣ p - q) :

src/ring_theory/polynomial/cyclotomic/basic.lean

@@ -828,7 +828,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.monic n ℤ).is_primitive,
+  apply minpoly.gcd_domain_dvd (is_integral h hpos) (cyclotomic_ne_zero n ℤ),
   simpa [aeval_def, eval₂_eq_eval_map, is_root.def] using is_root_cyclotomic hpos h
 end
 
@@ -857,7 +857,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.gcd_domain_eq_field_fractions' _ (is_integral h hpos)).symm
 end
 
 /-- `cyclotomic n ℤ` is irreducible. -/
@@ -950,9 +950,8 @@ 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 ℤ ℂ ℚ _ _ _ _ _ _ _ _ complex.algebra (algebra_int ℂ) _ _
-      (is_primitive_root.is_integral hprim hpos) _ ((cyclotomic.monic n ℤ).expand
-      hp.pos).is_primitive _,
+    refine minpoly.gcd_domain_dvd (hprim.is_integral hpos)
+      ((cyclotomic.monic n ℤ).expand hp.pos).ne_zero _,
     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),

src/ring_theory/polynomial/eisenstein.lean

@@ -317,7 +317,7 @@ begin
   have finrank_K_L : finite_dimensional.finrank K L = B.dim := B.finrank,
   have deg_K_P : (minpoly K B.gen).nat_degree = B.dim := B.nat_degree_minpoly,
   have deg_R_P : P.nat_degree = B.dim,
-  { rw [← deg_K_P, minpoly.gcd_domain_eq_field_fractions K hBint,
+  { rw [← deg_K_P, minpoly.gcd_domain_eq_field_fractions' K hBint,
         (minpoly.monic hBint).nat_degree_map (algebra_map R K)] },
   choose! f hf using hei.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree_le
     (minpoly.aeval R B.gen) (minpoly.monic hBint),
@@ -359,7 +359,7 @@ begin
   ... = _ : _,
   { simp only [algebra.smul_def, algebra_map_apply R K L, algebra.norm_algebra_map, _root_.map_mul,
       _root_.map_pow, finrank_K_L, power_basis.norm_gen_eq_coeff_zero_minpoly,
-      minpoly.gcd_domain_eq_field_fractions K hBint, coeff_map, ← hn],
+      minpoly.gcd_domain_eq_field_fractions' K hBint, coeff_map, ← hn],
     ring_exp },
   swap, { simp_rw [← smul_sum, ← smul_sub, algebra.smul_def p, algebra_map_apply R K L,
       _root_.map_mul, algebra.norm_algebra_map, finrank_K_L, hr, ← hn] },
@@ -493,7 +493,7 @@ begin
     rw [nat.succ_eq_add_one, add_assoc, ← nat.add_sub_assoc H, ← add_assoc, add_comm (j + 1),
       nat.add_sub_add_left, ← nat.add_sub_assoc, nat.add_sub_add_left, hP,
       ← (minpoly.monic hBint).nat_degree_map  (algebra_map R K),
-      ← minpoly.gcd_domain_eq_field_fractions K hBint, nat_degree_minpoly, hn, nat.sub_one,
+      ← minpoly.gcd_domain_eq_field_fractions' K hBint, nat_degree_minpoly, hn, nat.sub_one,
       nat.pred_succ],
     linarith },
 
@@ -531,7 +531,7 @@ begin
     rw [algebra.smul_def, mul_assoc, ← mul_sub, _root_.map_mul, algebra_map_apply R K L, map_pow,
       algebra.norm_algebra_map, _root_.map_mul, algebra_map_apply R K L, algebra.norm_algebra_map,
       finrank B, ← hr,
-      power_basis.norm_gen_eq_coeff_zero_minpoly, minpoly.gcd_domain_eq_field_fractions K hBint,
+      power_basis.norm_gen_eq_coeff_zero_minpoly, minpoly.gcd_domain_eq_field_fractions' K hBint,
       coeff_map, show (-1 : K) = algebra_map R K (-1), by simp, ← map_pow, ← map_pow,
       ← _root_.map_mul, ← map_pow, ← _root_.map_mul, ← map_pow, ← _root_.map_mul] at hQ,
 

src/ring_theory/roots_of_unity.lean

@@ -957,8 +957,8 @@ omit hpos
 lemma minpoly_dvd_X_pow_sub_one : minpoly ℤ μ ∣ X ^ n - 1 :=
 begin
   by_cases hpos : n = 0, { simp [hpos], },
-  apply minpoly.gcd_domain_dvd ℚ (is_integral h (nat.pos_of_ne_zero hpos))
-    (polynomial.monic.is_primitive (monic_X_pow_sub_C 1 (ne_of_lt (nat.pos_of_ne_zero hpos)).symm)),
+  apply minpoly.gcd_domain_dvd (is_integral h (nat.pos_of_ne_zero hpos))
+    (monic_X_pow_sub_C 1 (ne_of_lt (nat.pos_of_ne_zero hpos)).symm).ne_zero,
   simp only [((is_primitive_root.iff_def μ n).mp h).left, aeval_X_pow, ring_hom.eq_int_cast,
   int.cast_one, aeval_one, alg_hom.map_sub, sub_self]
 end
@@ -990,8 +990,8 @@ lemma minpoly_dvd_expand {p : ℕ} (hprime : nat.prime p) (hdiv : ¬ p ∣ n) :
 begin
   by_cases hn : n = 0, { simp * at *, },
   have hpos := nat.pos_of_ne_zero hn,
-  apply minpoly.gcd_domain_dvd ℚ (h.is_integral hpos),
-  { apply monic.is_primitive,
+  refine minpoly.gcd_domain_dvd (h.is_integral hpos) _ _,
+  { apply monic.ne_zero,
     rw [polynomial.monic, leading_coeff, nat_degree_expand, mul_comm, coeff_expand_mul'
         (nat.prime.pos hprime), ← leading_coeff, ← polynomial.monic],
     exact minpoly.monic (is_integral (pow_of_prime h hprime hdiv) hpos) },