feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (algebraMap K L a - x) splits (#17369)

Add `minpoly K x` splits implies `minpoly K (- x)` splits and `minpoly K (algebraMap K L a - x)` splits. This is after #17093 . 



Co-authored-by: Jiang Jiedong <107380768+jjdishere@users.noreply.github.com>

Author: jjdishere

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -306,22 +306,46 @@ theorem algEquivOfCompEqX_eq_iff (p q p' q' : R[X])
 theorem algEquivOfCompEqX_symm (p q : R[X]) (hpq : p.comp q = X) (hqp : q.comp p = X) :
     (algEquivOfCompEqX p q hpq hqp).symm = algEquivOfCompEqX q p hqp hpq := rfl
 
+/-- The automorphism of the polynomial algebra given by `p(X) ↦ p(a * X + b)`,
+  with inverse `p(X) ↦ p(a⁻¹ * (X - b))`. -/
+@[simps!]
+def algEquivCMulXAddC {R : Type*} [CommRing R] (a b : R) [Invertible a] : R[X] ≃ₐ[R] R[X] :=
+  algEquivOfCompEqX (C a * X + C b) (C ⅟ a * (X - C b))
+    (by simp [← C_mul, ← mul_assoc]) (by simp [← C_mul, ← mul_assoc])
+
+theorem algEquivCMulXAddC_symm_eq {R : Type*} [CommRing R] (a b : R) [Invertible a] :
+    (algEquivCMulXAddC a b).symm =  algEquivCMulXAddC (⅟ a) (- ⅟ a * b) := by
+  ext p : 1
+  simp only [algEquivCMulXAddC_symm_apply, neg_mul, algEquivCMulXAddC_apply, map_neg, map_mul]
+  congr
+  simp [mul_add, sub_eq_add_neg]
+
 /-- The automorphism of the polynomial algebra given by `p(X) ↦ p(X+t)`,
   with inverse `p(X) ↦ p(X-t)`. -/
 @[simps!]
-def algEquivAevalXAddC {R} [CommRing R] (t : R) : R[X] ≃ₐ[R] R[X] :=
+def algEquivAevalXAddC {R : Type*} [CommRing R] (t : R) : R[X] ≃ₐ[R] R[X] :=
   algEquivOfCompEqX (X + C t) (X - C t) (by simp) (by simp)
 
 @[simp]
-theorem algEquivAevalXAddC_eq_iff {R} [CommRing R] (t t' : R) :
+theorem algEquivAevalXAddC_eq_iff {R : Type*} [CommRing R] (t t' : R) :
     algEquivAevalXAddC t = algEquivAevalXAddC t' ↔ t = t' := by
   simp [algEquivAevalXAddC]
 
 @[simp]
-theorem algEquivAevalXAddC_symm {R} [CommRing R] (t : R) :
+theorem algEquivAevalXAddC_symm {R : Type*} [CommRing R] (t : R) :
     (algEquivAevalXAddC t).symm = algEquivAevalXAddC (-t) := by
   simp [algEquivAevalXAddC, sub_eq_add_neg]
 
+/-- The involutive automorphism of the polynomial algebra given by `p(X) ↦ p(-X)`. -/
+@[simps!]
+def algEquivAevalNegX {R : Type*} [CommRing R] : R[X] ≃ₐ[R] R[X] :=
+  algEquivOfCompEqX (-X) (-X) (by simp) (by simp)
+
+theorem comp_neg_X_comp_neg_X {R : Type*} [CommRing R] (p : R[X]) :
+    (p.comp (-X)).comp (-X) = p := by
+  rw [comp_assoc]
+  simp only [neg_comp, X_comp, neg_neg, comp_X]
+
 theorem aeval_algHom (f : A →ₐ[R] B) (x : A) : aeval (f x) = f.comp (aeval x) :=
   algHom_ext <| by simp only [aeval_X, AlgHom.comp_apply]
 
@@ -570,16 +594,25 @@ lemma comp_X_add_C_eq_zero_iff : p.comp (X + C t) = 0 ↔ p = 0 :=
 
 lemma comp_X_add_C_ne_zero_iff : p.comp (X + C t) ≠ 0 ↔ p ≠ 0 := comp_X_add_C_eq_zero_iff.not
 
+lemma dvd_comp_C_mul_X_add_C_iff (p q : R[X]) (a b : R) [Invertible a] :
+    p ∣ q.comp (C a * X + C b) ↔ p.comp (C ⅟ a * (X - C b)) ∣ q := by
+  convert map_dvd_iff <| algEquivCMulXAddC a b using 2
+  simp [← comp_eq_aeval, comp_assoc, ← mul_assoc, ← C_mul]
+
 lemma dvd_comp_X_sub_C_iff (p q : R[X]) (a : R) :
     p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q := by
-  convert (map_dvd_iff <| algEquivAevalXAddC a).symm using 2
-  rw [C_eq_algebraMap, algEquivAevalXAddC_apply, ← comp_eq_aeval]
-  simp [comp_assoc]
+  let _ := invertibleOne (α := R)
+  simpa using dvd_comp_C_mul_X_add_C_iff p q 1 (-a)
 
 lemma dvd_comp_X_add_C_iff (p q : R[X]) (a : R) :
     p ∣ q.comp (X + C a) ↔ p.comp (X - C a) ∣ q := by
   simpa using dvd_comp_X_sub_C_iff p q (-a)
 
+lemma dvd_comp_neg_X_iff (p q : R[X]) : p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q := by
+  let _ := invertibleOne (α := R)
+  let _ := invertibleNeg (α := R) 1
+  simpa using dvd_comp_C_mul_X_add_C_iff p q (-1) 0
+
 variable [IsDomain R]
 
 lemma units_coeff_zero_smul (c : R[X]ˣ) (p : R[X]) : (c : R[X]).coeff 0 • p = c * p := by

Mathlib/Algebra/Polynomial/Splits.lean

@@ -139,26 +139,72 @@ theorem splits_X_pow (n : ℕ) : (X ^ n).Splits i :=
 theorem splits_id_iff_splits {f : K[X]} : (f.map i).Splits (RingHom.id L) ↔ f.Splits i := by
   rw [splits_map_iff, RingHom.id_comp]
 
-theorem Splits.comp_X_sub_C {i : L →+* F} (a : L) {f : L[X]}
-    (h : f.Splits i) : (f.comp (X - C a)).Splits i := by
+variable {i}
+
+theorem Splits.comp_of_map_degree_le_one {f : K[X]} {p : K[X]} (hd : (p.map i).degree ≤ 1)
+    (h : f.Splits i) : (f.comp p).Splits i := by
+  by_cases hzero : map i (f.comp p) = 0
+  · exact Or.inl hzero
   cases h with
   | inl h0 =>
-    left
-    simp only [map_eq_zero] at h0 ⊢
-    exact h0.symm ▸ zero_comp
+    exact Or.inl <| map_comp i _ _ ▸ h0.symm ▸ zero_comp
   | inr h =>
     right
     intro g irr dvd
-    rw [map_comp, Polynomial.map_sub, map_X, map_C, dvd_comp_X_sub_C_iff] at dvd
-    have := h (irr.map (algEquivAevalXAddC _)) dvd
-    rw [degree_eq_natDegree irr.ne_zero]
-    rwa [algEquivAevalXAddC_apply, ← comp_eq_aeval,
-      degree_eq_natDegree (fun h => WithBot.bot_ne_one (h ▸ this)),
-      natDegree_comp, natDegree_X_add_C, mul_one] at this
-
-theorem Splits.comp_X_add_C {i : L →+* F} (a : L) {f : L[X]}
-    (h : f.Splits i) : (f.comp (X + C a)).Splits i := by
-  simpa only [map_neg, sub_neg_eq_add] using h.comp_X_sub_C (-a)
+    rw [map_comp] at dvd hzero
+    cases lt_or_eq_of_le hd with
+    | inl hd =>
+      rw [eq_C_of_degree_le_zero (Nat.WithBot.lt_one_iff_le_zero.mp hd), comp_C] at dvd hzero
+      refine False.elim (irr.1 (isUnit_of_dvd_unit dvd ?_))
+      simpa using hzero
+    | inr hd =>
+      let _ := invertibleOfNonzero (leadingCoeff_ne_zero.mpr
+          (ne_zero_of_degree_gt (n := ⊥) (by rw [hd]; decide)))
+      rw [eq_X_add_C_of_degree_eq_one hd, dvd_comp_C_mul_X_add_C_iff _ _] at dvd
+      have := h (irr.map (algEquivCMulXAddC _ _).symm) dvd
+      rw [degree_eq_natDegree irr.ne_zero]
+      rwa [algEquivCMulXAddC_symm_apply, ← comp_eq_aeval,
+        degree_eq_natDegree (fun h => WithBot.bot_ne_one (h ▸ this)),
+        natDegree_comp, natDegree_C_mul (invertibleInvOf.ne_zero),
+        natDegree_X_sub_C, mul_one] at this
+
+theorem splits_iff_comp_splits_of_degree_eq_one {f : K[X]} {p : K[X]} (hd : (p.map i).degree = 1) :
+    f.Splits i ↔ (f.comp p).Splits i := by
+  rw [← splits_id_iff_splits, ← splits_id_iff_splits (f := f.comp p), map_comp]
+  refine ⟨fun h => Splits.comp_of_map_degree_le_one
+    (le_of_eq (map_id (R := L) ▸ hd)) h, fun h => ?_⟩
+  let _ := invertibleOfNonzero (leadingCoeff_ne_zero.mpr
+      (ne_zero_of_degree_gt (n := ⊥) (by rw [hd]; decide)))
+  have : (map i f) = ((map i f).comp (map i p)).comp ((C ⅟ (map i p).leadingCoeff *
+      (X - C ((map i p).coeff 0)))) := by
+    rw [comp_assoc]
+    nth_rw 1 [eq_X_add_C_of_degree_eq_one hd]
+    simp only [coeff_map, invOf_eq_inv, mul_sub, ← C_mul, add_comp, mul_comp, C_comp, X_comp,
+      ← mul_assoc]
+    simp
+  refine this ▸ Splits.comp_of_map_degree_le_one ?_ h
+  simp [degree_C (inv_ne_zero (Invertible.ne_zero (a := (map i p).leadingCoeff)))]
+
+/--
+This is a weaker variant of `Splits.comp_of_map_degree_le_one`,
+but its conditions are easier to check.
+-/
+theorem Splits.comp_of_degree_le_one {f : K[X]} {p : K[X]} (hd : p.degree ≤ 1)
+    (h : f.Splits i) : (f.comp p).Splits i :=
+  Splits.comp_of_map_degree_le_one ((degree_map_le i _).trans hd) h
+
+theorem Splits.comp_X_sub_C (a : K) {f : K[X]}
+    (h : f.Splits i) : (f.comp (X - C a)).Splits i :=
+  Splits.comp_of_degree_le_one (degree_X_sub_C_le _) h
+
+theorem Splits.comp_X_add_C (a : K) {f : K[X]}
+    (h : f.Splits i) : (f.comp (X + C a)).Splits i :=
+  Splits.comp_of_degree_le_one (by simpa using degree_X_sub_C_le (-a)) h
+
+theorem Splits.comp_neg_X {f : K[X]} (h : f.Splits i) : (f.comp (-X)).Splits i :=
+  Splits.comp_of_degree_le_one (by simpa using degree_X_sub_C_le (0 : K)) h
+
+variable (i)
 
 theorem exists_root_of_splits' {f : K[X]} (hs : Splits i f) (hf0 : degree (f.map i) ≠ 0) :
     ∃ x, eval₂ i x f = 0 :=

Mathlib/RingTheory/Adjoin/Field.lean

@@ -97,6 +97,13 @@ theorem IsIntegral.mem_range_algebraMap_of_minpoly_splits [Algebra K L] [IsScala
     x ∈ (algebraMap K L).range :=
   int.mem_range_algHom_of_minpoly_splits h (IsScalarTower.toAlgHom R K L)
 
+theorem minpoly_neg_splits [Algebra K L] {x : L} (g : (minpoly K x).Splits (algebraMap K L)) :
+    (minpoly K (-x)).Splits (algebraMap K L) := by
+  rw [minpoly.neg]
+  apply splits_mul _ _ g.comp_neg_X
+  simpa only [map_pow, map_neg, map_one] using
+    splits_C (algebraMap K L) ((-1) ^ (minpoly K x).natDegree)
+
 theorem minpoly_add_algebraMap_splits [Algebra K L] {x : L} (r : K)
     (g : (minpoly K x).Splits (algebraMap K L)) :
     (minpoly K (x + algebraMap K L r)).Splits (algebraMap K L) := by
@@ -112,6 +119,11 @@ theorem minpoly_algebraMap_add_splits [Algebra K L] {x : L} (r : K)
     (minpoly K (algebraMap K L r + x)).Splits (algebraMap K L) := by
   simpa only [add_comm] using minpoly_add_algebraMap_splits r g
 
+theorem minpoly_algebraMap_sub_splits [Algebra K L] {x : L} (r : K)
+    (g : (minpoly K x).Splits (algebraMap K L)) :
+    (minpoly K (algebraMap K L r - x)).Splits (algebraMap K L) := by
+  simpa only [neg_sub] using minpoly_neg_splits (minpoly_sub_algebraMap_splits r g)
+
 end
 
 variable [Algebra K M] [IsScalarTower R K M] {x : M}