feat: Polynomial.map f strictly decreases the degree if `f p.leadin…

…gCoeff = 0` (#19411)

Also make more arguments to `degree_map_le` implicit.

From GrowthInGroups

Co-authored-by: Andrew Yang

Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

@@ -271,7 +271,7 @@ theorem degree_map_eq_iff {f : R →+* S} {p : Polynomial R} :
 theorem natDegree_map_eq_iff {f : R →+* S} {p : Polynomial R} :
     natDegree (map f p) = natDegree p ↔ f (p.leadingCoeff) ≠ 0 ∨ natDegree p = 0 := by
   rcases eq_or_ne (natDegree p) 0 with h|h
-  · simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le f p]
+  · simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]
   have h2 : p ≠ 0 := by rintro rfl; simp at h
   have h3 : degree p ≠ (0 : ℕ)  := degree_ne_of_natDegree_ne h
   simp_rw [h, or_false, natDegree, WithBot.unbot'_eq_unbot'_iff, degree_map_eq_iff]

Mathlib/Algebra/Polynomial/Div.lean

@@ -349,7 +349,7 @@ theorem map_mod_divByMonic [Ring S] (f : R →+* S) (hq : Monic q) :
     div_modByMonic_unique ((p /ₘ q).map f) _ (hq.map f)
       ⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div _ hq],
         calc
-          _ ≤ degree (p %ₘ q) := degree_map_le _ _
+          _ ≤ degree (p %ₘ q) := degree_map_le
           _ < degree q := degree_modByMonic_lt _ hq
           _ = _ :=
             Eq.symm <|

Mathlib/Algebra/Polynomial/Eval/Degree.lean

@@ -111,25 +111,15 @@ end Comp
 
 section Map
 
-variable [Semiring S]
-variable (f : R →+* S)
+variable [Semiring S] {f : R →+* S} {p : R[X]}
 
+variable (f) in
 /-- If `R` and `S` are isomorphic, then so are their polynomial rings. -/
 @[simps!]
 def mapEquiv (e : R ≃+* S) : R[X] ≃+* S[X] :=
   RingEquiv.ofHomInv (mapRingHom (e : R →+* S)) (mapRingHom (e.symm : S →+* R)) (by ext; simp)
     (by ext; simp)
 
-theorem degree_map_le (p : R[X]) : degree (p.map f) ≤ degree p := by
-  refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
-  rw [degree_lt_iff_coeff_zero] at hm
-  simp [hm m le_rfl]
-
-theorem natDegree_map_le (p : R[X]) : natDegree (p.map f) ≤ natDegree p :=
-  natDegree_le_natDegree (degree_map_le f p)
-
-variable {f}
-
 theorem map_monic_eq_zero_iff (hp : p.Monic) : p.map f = 0 ↔ ∀ x, f x = 0 :=
   ⟨fun hfp x =>
     calc
@@ -142,15 +132,39 @@ theorem map_monic_eq_zero_iff (hp : p.Monic) : p.map f = 0 ↔ ∀ x, f x = 0 :=
 theorem map_monic_ne_zero (hp : p.Monic) [Nontrivial S] : p.map f ≠ 0 := fun h =>
   f.map_one_ne_zero ((map_monic_eq_zero_iff hp).mp h _)
 
+lemma degree_map_le : degree (p.map f) ≤ degree p := by
+  refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
+  rw [degree_lt_iff_coeff_zero] at hm
+  simp [hm m le_rfl]
+
+lemma natDegree_map_le : natDegree (p.map f) ≤ natDegree p := natDegree_le_natDegree degree_map_le
+
+lemma degree_map_lt (hp : f p.leadingCoeff = 0) (hp₀ : p ≠ 0) : (p.map f).degree < p.degree := by
+  refine degree_map_le.lt_of_ne fun hpq ↦ hp₀ ?_
+  rw [leadingCoeff, ← coeff_map, ← natDegree_eq_natDegree hpq, ← leadingCoeff, leadingCoeff_eq_zero]
+    at hp
+  rw [← degree_eq_bot, ← hpq, hp, degree_zero]
+
+lemma natDegree_map_lt (hp : f p.leadingCoeff = 0) (hp₀ : map f p ≠ 0) :
+    (p.map f).natDegree < p.natDegree :=
+  natDegree_lt_natDegree hp₀ <| degree_map_lt hp <| by rintro rfl; simp at hp₀
+
+/-- Variant of `natDegree_map_lt` that assumes `0 < natDegree p` instead of `map f p ≠ 0`. -/
+lemma natDegree_map_lt' (hp : f p.leadingCoeff = 0) (hp₀ : 0 < natDegree p) :
+    (p.map f).natDegree < p.natDegree := by
+  by_cases H : map f p = 0
+  · rwa [H, natDegree_zero]
+  · exact natDegree_map_lt hp H
+
 theorem degree_map_eq_of_leadingCoeff_ne_zero (f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) :
-    degree (p.map f) = degree p :=
-  le_antisymm (degree_map_le f _) <| by
-    have hp0 : p ≠ 0 :=
-      leadingCoeff_ne_zero.mp fun hp0 => hf (_root_.trans (congr_arg _ hp0) f.map_zero)
-    rw [degree_eq_natDegree hp0]
-    refine le_degree_of_ne_zero ?_
-    rw [coeff_map]
-    exact hf
+    degree (p.map f) = degree p := by
+  refine degree_map_le.antisymm ?_
+  have hp0 : p ≠ 0 :=
+    leadingCoeff_ne_zero.mp fun hp0 => hf (_root_.trans (congr_arg _ hp0) f.map_zero)
+  rw [degree_eq_natDegree hp0]
+  refine le_degree_of_ne_zero ?_
+  rw [coeff_map]
+  exact hf
 
 theorem natDegree_map_of_leadingCoeff_ne_zero (f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) :
     natDegree (p.map f) = natDegree p :=

Mathlib/Algebra/Polynomial/Monic.lean

@@ -357,7 +357,7 @@ variable [Semiring R]
 @[simp]
 theorem Monic.natDegree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic) (f : R →+* S) :
     (P.map f).natDegree = P.natDegree := by
-  refine le_antisymm (natDegree_map_le _ _) (le_natDegree_of_ne_zero ?_)
+  refine le_antisymm natDegree_map_le (le_natDegree_of_ne_zero ?_)
   rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]
   exact one_ne_zero
 
@@ -366,7 +366,7 @@ theorem Monic.degree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic)
     (P.map f).degree = P.degree := by
   by_cases hP : P = 0
   · simp [hP]
-  · refine le_antisymm (degree_map_le _ _) ?_
+  · refine le_antisymm degree_map_le ?_
     rw [degree_eq_natDegree hP]
     refine le_degree_of_ne_zero ?_
     rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]

Mathlib/Algebra/Polynomial/Roots.lean

@@ -749,13 +749,13 @@ theorem roots_map_of_injective_of_card_eq_natDegree [IsDomain A] [IsDomain B] {p
     {f : A →+* B} (hf : Function.Injective f) (hroots : Multiset.card p.roots = p.natDegree) :
     p.roots.map f = (p.map f).roots := by
   apply Multiset.eq_of_le_of_card_le (map_roots_le_of_injective p hf)
-  simpa only [Multiset.card_map, hroots] using (card_roots' _).trans (natDegree_map_le f p)
+  simpa only [Multiset.card_map, hroots] using (card_roots' _).trans natDegree_map_le
 
 theorem roots_map_of_map_ne_zero_of_card_eq_natDegree [IsDomain A] [IsDomain B] {p : A[X]}
     (f : A →+* B) (h : p.map f ≠ 0) (hroots : p.roots.card = p.natDegree) :
     p.roots.map f = (p.map f).roots :=
   eq_of_le_of_card_le (map_roots_le h) <| by
-    simpa only [Multiset.card_map, hroots] using (p.map f).card_roots'.trans (p.natDegree_map_le f)
+    simpa only [Multiset.card_map, hroots] using (p.map f).card_roots'.trans natDegree_map_le
 
 theorem Monic.roots_map_of_card_eq_natDegree [IsDomain A] [IsDomain B] {p : A[X]} (hm : p.Monic)
     (f : A →+* B) (hroots : p.roots.card = p.natDegree) : p.roots.map f  = (p.map f).roots :=

Mathlib/Algebra/Polynomial/Splits.lean

@@ -77,7 +77,7 @@ theorem splits_of_degree_le_one {f : K[X]} (hf : degree f ≤ 1) : Splits i f :=
   else by
     push_neg at hif
     rw [← Order.succ_le_iff, ← WithBot.coe_zero, WithBot.succ_coe, Nat.succ_eq_succ] at hif
-    exact splits_of_map_degree_eq_one i (le_antisymm ((degree_map_le i _).trans hf) hif)
+    exact splits_of_map_degree_eq_one i ((degree_map_le.trans hf).antisymm hif)
 
 theorem splits_of_degree_eq_one {f : K[X]} (hf : degree f = 1) : Splits i f :=
   splits_of_degree_le_one i hf.le
@@ -189,7 +189,7 @@ 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
+  Splits.comp_of_map_degree_le_one (degree_map_le.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 :=

Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean

@@ -217,14 +217,17 @@ theorem aeval_sumIDeriv_of_pos [Nontrivial A] [NoZeroDivisors A] (p : R[X]) {q :
   intro r p' hp
   have : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1) := by
     rw [range_eq_Ico, Ico_union_Ico_eq_Ico hq.le]
-    have h := natDegree_map_le (algebraMap R A) p
-    rw [congr_arg natDegree hp, natDegree_mul, natDegree_pow, natDegree_X_sub_C, mul_one,
-      ← Nat.sub_add_comm (Nat.one_le_of_lt hq), tsub_le_iff_right] at h
-    exact le_of_add_le_left h
-    · exact pow_ne_zero _ (X_sub_C_ne_zero r)
-    · rintro rfl
-      rw [mul_zero, Polynomial.map_eq_zero_iff inj_amap] at hp
-      exact p0 hp
+    rw [← tsub_le_iff_right]
+    calc
+      q - 1 ≤ q - 1 + p'.natDegree := le_self_add
+      _ = (p.map <| algebraMap R A).natDegree := by
+        rw [hp, natDegree_mul, natDegree_pow, natDegree_X_sub_C, mul_one,
+          ← Nat.sub_add_comm (Nat.one_le_of_lt hq)]
+        · exact pow_ne_zero _ (X_sub_C_ne_zero r)
+        · rintro rfl
+          rw [mul_zero, Polynomial.map_eq_zero_iff inj_amap] at hp
+          exact p0 hp
+      _ ≤ p.natDegree := natDegree_map_le
   rw [← zero_add ((q - 1)! • p'.eval r)]
   rw [sumIDeriv_apply, map_sum, map_sum, this]
   have : range q = range (q - 1 + 1) := by rw [tsub_add_cancel_of_le (Nat.one_le_of_lt hq)]

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -880,7 +880,7 @@ lemma isIntegral_of_isClosedMap_comap_mapRingHom (h : IsClosedMap (comap (mapRin
   · have : p.natDegree ≤ 1 := by simpa using natDegree_linear_le (a := r) (b := -1)
     rw [eval₂_eq_eval_map, reverse, Polynomial.map_mul, ← reflect_map, Polynomial.map_pow,
       map_X, ← revAt_zero (1 + _), ← reflect_monomial,
-      ← reflect_mul _ _ (natDegree_map_le _ _) (by simp), pow_zero, mul_one, hc,
+      ← reflect_mul _ _ natDegree_map_le (by simp), pow_zero, mul_one, hc,
       ← add_assoc, reflect_mul _ _ (this.trans (by simp)) le_rfl,
       eval_mul, reflect_sub, reflect_mul _ _ (by simp) (by simp)]
     simp [← pow_succ']

Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

@@ -214,7 +214,7 @@ lemma sum_smul_minpolyDiv_eq_X_pow (E) [Field E] [Algebra K E] [IsAlgClosed E]
         Finset.mem_univ, forall_true_left, true_and, Finset.fold_max_lt, AlgHom.card]
       refine ⟨finrank_pos, ?_⟩
       intro σ
-      exact ((Polynomial.natDegree_smul_le _ _).trans (natDegree_map_le _ _)).trans_lt
+      exact ((Polynomial.natDegree_smul_le _ _).trans natDegree_map_le).trans_lt
         ((natDegree_minpolyDiv_lt (Algebra.IsIntegral.isIntegral x)).trans_le
           (minpoly.natDegree_le _))
     · rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card]

Mathlib/RingTheory/EisensteinCriterion.lean

@@ -40,7 +40,7 @@ theorem map_eq_C_mul_X_pow_of_forall_coeff_mem {f : R[X]} {P : Ideal R}
     · rw [coeff_eq_zero_of_degree_lt, coeff_eq_zero_of_degree_lt]
       · refine lt_of_le_of_lt (degree_C_mul_X_pow_le _ _) ?_
         rwa [← degree_eq_natDegree hf0]
-      · exact lt_of_le_of_lt (degree_map_le _ _) h
+      · exact lt_of_le_of_lt degree_map_le h
 
 theorem le_natDegree_of_map_eq_mul_X_pow {n : ℕ} {P : Ideal R} (hP : P.IsPrime) {q : R[X]}
     {c : Polynomial (R ⧸ P)} (hq : map (mk P) q = c * X ^ n) (hc0 : c.degree = 0) :
@@ -49,7 +49,7 @@ theorem le_natDegree_of_map_eq_mul_X_pow {n : ℕ} {P : Ideal R} (hP : P.IsPrime
     (calc
       ↑n = degree (q.map (mk P)) := by
         rw [hq, degree_mul, hc0, zero_add, degree_pow, degree_X, nsmul_one]
-      _ ≤ degree q := degree_map_le _ _
+      _ ≤ degree q := degree_map_le
       _ ≤ natDegree q := degree_le_natDegree
       )
 

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

@@ -372,7 +372,7 @@ lemma exists_eval_ne_zero_of_totalDegree_le_card_aux {N : ℕ} {F : MvPolynomial
     have hφR : φ.natDegree < #R := by
       refine lt_of_lt_of_le ?_ hnR
       norm_cast
-      refine lt_of_le_of_lt (natDegree_map_le _ _) ?_
+      refine lt_of_le_of_lt natDegree_map_le ?_
       suffices (finSuccEquiv _ _ F).natDegree ≠ n by omega
       rintro rfl
       refine leadingCoeff_ne_zero.mpr ?_ hFn

Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean

@@ -62,7 +62,7 @@ theorem map (hf : f.IsWeaklyEisensteinAt 𝓟) {A : Type v} [CommRing A] (φ : R
     (f.map φ).IsWeaklyEisensteinAt (𝓟.map φ) := by
   refine (isWeaklyEisensteinAt_iff _ _).2 fun hn => ?_
   rw [coeff_map]
-  exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn (natDegree_map_le _ _)))
+  exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn natDegree_map_le))
 
 end CommSemiring
 
@@ -91,7 +91,7 @@ theorem exists_mem_adjoin_mul_eq_pow_natDegree {x : S} (hx : aeval x f = 0) (hmo
     congr
     · skip
     ext i
-    rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (natDegree_map_le _ _)),
+    rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 natDegree_map_le),
       RingHom.map_mul, mul_assoc]
   rw [hx, ← mul_sum, neg_eq_neg_one_mul, ← mul_assoc (-1 : S), mul_comm (-1 : S), mul_assoc]
   refine

Mathlib/RingTheory/RootsOfUnity/Minpoly.lean

@@ -217,7 +217,7 @@ theorem totient_le_degree_minpoly : Nat.totient n ≤ (minpoly ℤ μ).natDegree
     _ ≤ P_K.roots.toFinset.card := Finset.card_le_card (is_roots_of_minpoly h)
     _ ≤ Multiset.card P_K.roots := Multiset.toFinset_card_le _
     _ ≤ P_K.natDegree := card_roots' _
-    _ ≤ P.natDegree := natDegree_map_le _ _
+    _ ≤ P.natDegree := natDegree_map_le
 
 end IsDomain