feat(data/polynomial/reverse.lean): show trailing_coeff is a multiplicative homomorphism

src/data/finset/lattice.lean

@@ -77,7 +77,7 @@ lemma comp_sup_eq_sup_comp_of_is_total [is_total α (≤)] {γ : Type} [semilatt
   (g : α → γ) (mono_g : monotone g) (bot : g ⊥ = ⊥) : g (s.sup f) = s.sup (g ∘ f) :=
 comp_sup_eq_sup_comp g mono_g.map_sup bot
 
-/-- Computating `sup` in a subtype (closed under `sup`) is the same as computing it in `α`. -/
+/-- Computing `sup` in a subtype (closed under `sup`) is the same as computing it in `α`. -/
 lemma sup_coe {P : α → Prop}
   {Pbot : P ⊥} {Psup : ∀{{x y}}, P x → P y → P (x ⊔ y)}
   (t : finset β) (f : β → {x : α // P x}) :

src/data/polynomial/degree/trailing_degree.lean

@@ -274,7 +274,7 @@ by simp only [←C_eq_int_cast, nat_trailing_degree_C]
 end ring
 
 section semiring
-variables [semiring R]
+variables [semiring R] {p q : polynomial R} {ι : Type*}
 
 /-- The second-lowest coefficient, or 0 for constants -/
 def next_coeff_up (p : polynomial R) : R :=
@@ -288,12 +288,6 @@ lemma next_coeff_up_of_pos_nat_trailing_degree (p : polynomial R) (hp : 0 < p.na
   next_coeff_up p = p.coeff (p.nat_trailing_degree + 1) :=
 by { rw [next_coeff_up, if_neg], contrapose! hp, simpa }
 
-end semiring
-
-section semiring
-variables [semiring R] {p q : polynomial R} {ι : Type*}
-
-
 lemma coeff_nat_trailing_degree_eq_zero_of_trailing_degree_lt (h : trailing_degree p < trailing_degree q) :
   coeff q (nat_trailing_degree p) = 0 :=
 begin
@@ -314,5 +308,25 @@ begin
   exact dec_trivial,
 end
 
+@[simp] lemma trailing_coeff_one : (1 : polynomial R).trailing_coeff = 1 :=
+by rw [trailing_coeff, nat_trailing_degree_one, coeff_one_zero]
+
+lemma nat_trailing_degree_le_nat_degree : p.nat_trailing_degree ≤ p.nat_degree :=
+begin
+  by_cases p0 : p = 0,
+  { rw [p0, nat_degree_zero, nat_trailing_degree_zero], },
+  rw [nat_degree_eq_support_max' p0, nat_trailing_degree_eq_support_min' p0],
+  exact p.support.min'_le (p.support.max' _) (p.support.max'_mem _),
+end
+
+@[simp] lemma nat_trailing_degree_eq_zero (h : p.coeff 0 ≠ 0) : p.nat_trailing_degree = 0 :=
+begin
+  rw nat_trailing_degree_eq_support_min',
+  { exact nat.eq_zero_of_le_zero (min'_le _ _ (mem_support_iff_coeff_ne_zero.mpr h)),
+    intro p0,
+    apply h,
+    rw [p0, coeff_zero], },
+end
+
 end semiring
 end polynomial

src/data/polynomial/erase_lead.lean

@@ -3,9 +3,7 @@ Copyright (c) 2020 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import data.polynomial.degree.basic
 import data.polynomial.degree
-import data.polynomial.degree.trailing_degree
 
 /-!
 # Erase the leading term of a univariate polynomial

src/data/polynomial/reverse.lean

@@ -4,23 +4,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import data.polynomial.erase_lead
-import data.polynomial.degree
+import data.polynomial.degree.trailing_degree
+import data.polynomial.to_finset_lattice_max_min
 
 /-!
 # Reverse of a univariate polynomial
 
 The main definition is `reverse`.  Applying `reverse` to a polynomial `f : polynomial R` produces
 the polynomial with a reversed list of coefficients, equivalent to `X^f.nat_degree * f(1/X)`.
 
-The main result is that `reverse (f * g) = reverse (f) * reverse (g)`, provided the leading
-coefficients of `f` and `g` do not multiply to zero.
+The main results are:
+
+1. `reverse (f * g) = reverse (f) * reverse (g)`, provided the leading
+coefficients of `f` and `g` do not multiply to zero;
+
+2. if the coefficient ring R is an integral domain, then the function
+`trailing_coeff_hom : polynomial R →* R` is a multiplicative monoid homomorphism.
 -/
 
 namespace polynomial
 
 open polynomial finsupp finset
 open_locale classical
 
+section semiring
+
 variables {R : Type*} [semiring R] {f : polynomial R}
 
 /-- If `i ≤ N`, then `rev_at_fun N i` returns `N - i`, otherwise it returns `i`.
@@ -31,19 +39,13 @@ def rev_at_fun (N i : ℕ) : ℕ := ite (i ≤ N) (N-i) i
 lemma rev_at_fun_invol {N i : ℕ} : rev_at_fun N (rev_at_fun N i) = i :=
 begin
   unfold rev_at_fun,
-  split_ifs with h j,
-  { exact nat.sub_sub_self h, },
-  { exfalso,
-    apply j,
-    exact nat.sub_le N i, },
-  { refl, },
+  by_cases Ni : i ≤ N,
+  { rwa [if_pos Ni, if_pos (nat.sub_le_self N i), nat.sub_sub_self], },
+  { repeat { rw if_neg Ni, }, },
 end
 
 lemma rev_at_fun_inj {N : ℕ} : function.injective (rev_at_fun N) :=
-begin
-  intros a b hab,
-  rw [← @rev_at_fun_invol N a, hab, rev_at_fun_invol],
-end
+λ a b hab, by rw [← @rev_at_fun_invol N a, hab, rev_at_fun_invol]
 
 /-- If `i ≤ N`, then `rev_at N i` returns `N - i`, otherwise it returns `i`.
 Essentially, this embedding is only used for `i ≤ N`.
@@ -67,9 +69,9 @@ lemma rev_at_add {N O n o : ℕ} (hn : n ≤ N) (ho : o ≤ O) :
 begin
   rcases nat.le.dest hn with ⟨n', rfl⟩,
   rcases nat.le.dest ho with ⟨o', rfl⟩,
-  repeat { rw rev_at_le (le_add_right rfl.le) },
+  repeat { rw rev_at_le (le_add_right rfl.le), },
   rw [add_assoc, add_left_comm n' o, ← add_assoc, rev_at_le (le_add_right rfl.le)],
-  repeat {rw nat.add_sub_cancel_left},
+  repeat { rw nat.add_sub_cancel_left },
 end
 
 /-- `reflect N f` is the polynomial such that `(reflect N f).coeff i = f.coeff (rev_at N i)`.
@@ -83,10 +85,7 @@ finsupp.emb_domain (rev_at N) f
 
 lemma reflect_support (N : ℕ) (f : polynomial R) :
   (reflect N f).support = image (rev_at N) f.support :=
-begin
-  ext1,
-  rw [reflect, mem_image, support_emb_domain, mem_map],
-end
+by refine finset.ext (λ (a : ℕ), (by rw [reflect, mem_image, support_emb_domain, mem_map]))
 
 @[simp] lemma coeff_reflect (N : ℕ) (f : polynomial R) (i : ℕ) :
   coeff (reflect N f) i = f.coeff (rev_at N i) :=
@@ -98,35 +97,28 @@ calc finsupp.emb_domain (rev_at N) f i
 
 @[simp] lemma reflect_eq_zero_iff {N : ℕ} {f : polynomial R} :
   reflect N (f : polynomial R) = 0 ↔ f = 0 :=
-begin
-  split,
-  { intros a,
-    injection a with f0 f1,
-    rwa [map_eq_empty, support_eq_empty] at f0, },
-  { rintro rfl,
-    refl, },
-end
+by refine ⟨(λ a, by rwa [reflect, emb_domain_eq_zero] at a), by { rintro rfl, refl }⟩
 
 @[simp] lemma reflect_add (f g : polynomial R) (N : ℕ) :
   reflect N (f + g) = reflect N f + reflect N g :=
-by { ext, simp only [coeff_add, coeff_reflect], }
+by { ext1, rw [coeff_add, coeff_reflect, coeff_reflect, coeff_reflect, coeff_add], }
 
 @[simp] lemma reflect_C_mul (f : polynomial R) (r : R) (N : ℕ) :
   reflect N (C r * f) = C r * (reflect N f) :=
-by { ext, simp only [coeff_reflect, coeff_C_mul], }
+by refine ext (λ (n : ℕ), by rw [coeff_reflect, coeff_C_mul, coeff_C_mul, coeff_reflect])
 
 @[simp] lemma reflect_C_mul_X_pow (N n : ℕ) {c : R} :
   reflect N (C c * X ^ n) = C c * X ^ (rev_at N n) :=
 begin
-  ext,
+  ext a,
   rw [reflect_C_mul, coeff_C_mul, coeff_C_mul, coeff_X_pow, coeff_reflect],
-  split_ifs with h j,
+  split_ifs,
   { rw [h, rev_at_invol, coeff_X_pow_self], },
-  { rw [not_mem_support_iff_coeff_zero.mp],
-    intro a,
-    rw [← one_mul (X ^ n), ← C_1] at a,
+  { rw not_mem_support_iff_coeff_zero.mp,
+    intro rs,
+    rw [← one_mul (X ^ n), ← C_1] at rs,
     apply h,
-    rw [← (mem_support_C_mul_X_pow a), rev_at_invol], },
+    rw [← (mem_support_C_mul_X_pow rs), rev_at_invol], },
 end
 
 @[simp] lemma reflect_monomial (N n : ℕ) : reflect N ((X : polynomial R) ^ n) = X ^ (rev_at N n) :=
@@ -181,22 +173,184 @@ noncomputable def reverse (f : polynomial R) : polynomial R := reflect f.nat_deg
 @[simp] lemma reverse_zero : reverse (0 : polynomial R) = 0 := rfl
 
 theorem reverse_mul {f g : polynomial R} (fg : f.leading_coeff * g.leading_coeff ≠ 0) :
- reverse (f * g) = reverse f * reverse g :=
-begin
-  unfold reverse,
-  rw [nat_degree_mul' fg, reflect_mul  f g rfl.le rfl.le],
-end
+  reverse (f * g) = reverse f * reverse g :=
+by simp only [reverse, nat_degree_mul' fg, reflect_mul]
 
 @[simp] lemma reverse_mul_of_domain {R : Type*} [domain R] (f g : polynomial R) :
   reverse (f * g) = reverse f * reverse g :=
 begin
   by_cases f0 : f=0,
-  { simp only [f0, zero_mul, reverse_zero], },
+  { rw [f0, zero_mul, reverse_zero, zero_mul], },
   by_cases g0 : g=0,
   { rw [g0, mul_zero, reverse_zero, mul_zero], },
   apply reverse_mul,
   apply mul_ne_zero;
-    rwa [← leading_coeff_eq_zero] at *
+  { rwa [← leading_coeff_eq_zero] at *, },
+end
+
+lemma reflect_ne_zero_iff {N : ℕ} {f : polynomial R} :
+  reflect N (f : polynomial R) ≠ 0 ↔ f ≠ 0 :=
+not_congr reflect_eq_zero_iff
+
+@[simp] lemma rev_at_gt {N n : ℕ} (H : N < n) : rev_at N n = n :=
+if_neg (not_le.mpr H)
+
+@[simp] lemma reflect_invol (N : ℕ) : reflect N (reflect N f) = f :=
+by refine ext (λ (n : ℕ), by rw [coeff_reflect, coeff_reflect, rev_at_invol])
+
+/-- `monotone_rev_at N _` coincides with `rev_at N _` in the range [0,..,N].  I use
+`monotone_rev_at` just to show that `rev_at` exchanges `min`s and `max`s.  With an alternative
+proof of the exchange property that does not use this definition, it can be removed! -/
+def monotone_rev_at (N : ℕ) : ℕ → ℕ := λ i : ℕ , (N-i)
+
+lemma monotone_rev_at_monotone (N : ℕ) : mon (monotone_rev_at N) :=
+begin
+  intros x y hxy,
+  rw [monotone_rev_at, nat.sub_le_iff],
+  by_cases xle : x ≤ N,
+  { rwa nat.sub_sub_self xle, },
+  rw not_le at xle,
+  apply le_of_lt,
+  convert gt_of_ge_of_gt hxy xle,
+  convert nat.sub_zero N,
+  exact nat.sub_eq_zero_iff_le.mpr (le_of_lt xle),
+end
+
+lemma monotone_rev_at_max'_min' {N : ℕ} {s : finset ℕ} {hs : s.nonempty} :
+  max' (image (monotone_rev_at N) s) (nonempty.image hs (monotone_rev_at N)) =
+  monotone_rev_at N (min' s hs) :=
+monotone_max'_min' hs (monotone_rev_at_monotone N)
+
+@[simp] lemma monotone_rev_at_eq_rev_at_small {N n : ℕ} :
+  (n ≤ N) → rev_at N n = monotone_rev_at N n :=
+λ H, by convert (@rev_at_le N n H)
+
+lemma rev_at_small_min_max {N : ℕ} {s : finset ℕ} {hs : s.nonempty} (sm : s.max' hs ≤ N) :
+  max' (image (rev_at N) s) (nonempty.image hs (rev_at N)) = rev_at N (min' s hs) :=
+begin
+  rwa [monotone_rev_at_eq_rev_at_small (le_trans (le_max' _ _ (min'_mem s hs)) sm),
+    ← monotone_rev_at_max'_min'],
+  have im : (image (rev_at N) s) = (image (monotone_rev_at N) s) →
+    (image (rev_at N) s).max' (nonempty.image hs (rev_at N)) = (image (monotone_rev_at N) s).max'
+    (nonempty.image hs (monotone_rev_at N)) := λ a, (by {congr, exact a}),
+  apply im,
+  ext1 a,
+  repeat { rw mem_image },
+  refine ⟨_ , _⟩;
+  { rintro ⟨a, ha, rfl⟩ ,
+    refine ⟨a, ha, by rw (monotone_rev_at_eq_rev_at_small (le_trans (le_max' _ _ ha) sm)) ⟩, },
 end
 
+lemma nat_degree_reflect_eq_nat_trailing_degree {N : ℕ} (f0 : f ≠ 0) (H : f.nat_degree ≤ N) :
+  (reflect N f).nat_degree = rev_at N f.nat_trailing_degree :=
+begin
+  rw nat_degree_eq_support_max' (reflect_ne_zero_iff.mpr f0),
+  rw [nat_trailing_degree_eq_support_min' f0],
+  simp_rw [reflect, finsupp.support_emb_domain, map_eq_image],
+  refine rev_at_small_min_max (by rwa ← nat_degree_eq_support_max' f0),
+end
+
+lemma nat_degree_reflect_le {N : ℕ} : (reflect N f).nat_degree ≤ max N f.nat_degree :=
+begin
+  by_cases f0 : f=0,
+  { rw [f0, reflect_zero, nat_degree_zero], exact zero_le (max N 0), },
+  by_cases dsm : f.nat_degree ≤ N,
+  { rw [nat_degree_reflect_eq_nat_trailing_degree f0 dsm, max_eq_left dsm],
+    rw rev_at_le (le_trans nat_trailing_degree_le_nat_degree dsm),
+    exact (nat.sub_le N f.nat_trailing_degree), },
+  { rw [not_le, lt_iff_le_and_ne] at dsm,
+    rw [max_eq_right (dsm.1), nat_degree_eq_support_max', nat_degree_eq_support_max' f0],
+    { apply max'_le,
+      intros y hy,
+      rw [reflect_support, mem_image] at hy,
+      rcases hy with ⟨ y , hy , rfl ⟩,
+      rw ← nat_degree_eq_support_max',
+      by_cases ys : y ≤ N,
+      { rw rev_at_le ys, exact (le_trans (nat.sub_le N y) dsm.1), },
+      { rw rev_at_gt (not_le.mp ys), exact le_nat_degree_of_mem_supp _ hy, }, },
+    { rwa [ne.def, (@reflect_eq_zero_iff R _ N f)], }, },
+end
+
+@[simp] lemma reverse_invol (h : f.coeff 0 ≠ 0) : reverse (reverse f) = f :=
+begin
+  rw [reverse, reverse, nat_degree_reflect_eq_nat_trailing_degree _ rfl.le],
+  { rw [rev_at_le nat_trailing_degree_le_nat_degree, nat_trailing_degree_eq_zero h, nat.sub_zero,
+      reflect_invol], },
+  { intro f0, apply h, rw [f0, coeff_zero], },
+end
+
+lemma lead_reflect_eq_trailing (N : ℕ) (H : f.nat_degree ≤ N) :
+  leading_coeff (reflect N f) = trailing_coeff f :=
+begin
+  by_cases f0 : f = 0,
+  { rw [f0, reflect_zero, leading_coeff, trailing_coeff, coeff_zero, coeff_zero], },
+  rw [leading_coeff, trailing_coeff, nat_trailing_degree_eq_support_min' f0],
+  rw nat_degree_eq_support_max' (reflect_ne_zero_iff.mpr f0),
+  simp_rw [coeff_reflect, reflect_support],
+  rw [rev_at_small_min_max, rev_at_invol],
+  convert H,
+  rw nat_degree_eq_support_max',
+end
+
+lemma trailing_reflect_eq_lead (N : ℕ) (H : f.nat_degree ≤ N) :
+  trailing_coeff (reflect N f) = leading_coeff f :=
+begin
+  rw [← @reflect_invol R _ f N] {occs := occurrences.pos [2]},
+  rw lead_reflect_eq_trailing,
+  convert @nat_degree_reflect_le R _ f N,
+  rwa max_eq_left,
+end
+
+lemma nat_trailing_degree_reflect_eq_nat_degree {N : ℕ} (f0 : f ≠ 0) (H : f.nat_degree ≤ N) :
+  (reflect N f).nat_trailing_degree = rev_at N f.nat_degree :=
+begin
+  rw [← @reflect_invol R _ f N] {occs := occurrences.pos [2]},
+  rw [nat_degree_reflect_eq_nat_trailing_degree (reflect_ne_zero_iff.mpr f0), rev_at_invol],
+  apply le_trans nat_degree_reflect_le _,
+  rw max_eq_left H,
+end
+
+lemma lead_reverse_eq_trailing (f : polynomial R) : leading_coeff (reverse f) = trailing_coeff f :=
+lead_reflect_eq_trailing _ rfl.le
+
+lemma trailing_reverse_eq_lead (f : polynomial R) : trailing_coeff (reverse f) = leading_coeff f :=
+trailing_reflect_eq_lead _ rfl.le
+
+end semiring
+
+section integral_domain
+
+variables {R : Type*} [integral_domain R] {p q : polynomial R}
+
+@[simp] lemma trailing_coeff_mul (p q : polynomial R)  : trailing_coeff (p * q) =
+  trailing_coeff p * trailing_coeff q :=
+begin
+  rw [← @reflect_invol R _ (p * q) (p.nat_degree + q.nat_degree), trailing_reflect_eq_lead],
+  { rw [reflect_mul p q rfl.le rfl.le, leading_coeff_mul],
+    rw [← trailing_reflect_eq_lead p.nat_degree, reflect_invol],
+    { rw [← trailing_reflect_eq_lead q.nat_degree, reflect_invol],
+      convert @nat_degree_reflect_le R _ q q.nat_degree,
+      rw max_eq_left rfl.le, },
+    { convert @nat_degree_reflect_le R _ p p.nat_degree,
+      exact (max_eq_left rfl.le).symm, }, },
+  { convert nat_degree_reflect_le,
+    exact (max_eq_left nat_degree_mul_le).symm, },
+end
+
+/-- `polynomial.trailing_coeff` bundled as a `monoid_hom` when `R` is an `integral_domain`, and thus
+  `trailing_coeff` is multiplicative -/
+noncomputable def trailing_coeff_hom : polynomial R →* R :=
+{ to_fun := trailing_coeff,
+  map_one' := trailing_coeff_one,
+  map_mul' := trailing_coeff_mul }
+
+@[simp] lemma trailing_coeff_hom_apply (p : polynomial R) :
+  trailing_coeff_hom p = trailing_coeff p := rfl
+
+@[simp] lemma trailing_coeff_pow (p : polynomial R) (n : ℕ) :
+  trailing_coeff (p ^ n) = trailing_coeff p ^ n :=
+trailing_coeff_hom.map_pow p n
+
+end integral_domain
+
 end polynomial