feat(ring_theory/power_basis): equivs between algebras with the sam…

…e power basis (#4986)

`power_basis.lift` and `power_basis.equiv` use the power basis structure to define `alg_hom`s and `alg_equiv`s.
    
The main application in this PR is `power_basis.equiv_adjoin_simple`, which states that adjoining an element of a power basis of `L : K` gives `L` itself.

src/data/polynomial/algebra_map.lean

@@ -15,6 +15,7 @@ We promote `eval₂` to an algebra hom in `aeval`.
 
 noncomputable theory
 open finset
+open_locale big_operators
 
 namespace polynomial
 universes u v w z
@@ -207,6 +208,14 @@ lemma dvd_term_of_is_root_of_dvd_terms {r p : S} {f : polynomial S} (i : ℕ)
   (hr : f.is_root r) (h : ∀ (j ≠ i), p ∣ f.coeff j * r ^ j) : p ∣ f.coeff i * r ^ i :=
 dvd_term_of_dvd_eval_of_dvd_terms i (eq.symm hr ▸ dvd_zero p) h
 
+lemma aeval_eq_sum_range [algebra R S] {p : polynomial R} (x : S) :
+  aeval x p = ∑ i in finset.range (p.nat_degree + 1), p.coeff i • x ^ i :=
+by { simp_rw algebra.smul_def, exact eval₂_eq_sum_range (algebra_map R S) x }
+
+lemma aeval_eq_sum_range' [algebra R S] {p : polynomial R} {n : ℕ} (hn : p.nat_degree < n) (x : S) :
+  aeval x p = ∑ i in finset.range n, p.coeff i • x ^ i :=
+by { simp_rw algebra.smul_def, exact eval₂_eq_sum_range' (algebra_map R S) hn x }
+
 end aeval
 
 section ring

src/data/polynomial/degree/basic.lean

@@ -447,23 +447,25 @@ begin
     exact mul_X_pow_eq_zero ‹_›, },
 end
 
-lemma degree_add_eq_of_degree_lt (h : degree p < degree q) : degree (p + q) = degree q :=
-le_antisymm (max_eq_right_of_lt h ▸ degree_add_le _ _) $ degree_le_degree $
+lemma degree_add_eq_left_of_degree_lt (h : degree q < degree p) : degree (p + q) = degree p :=
+le_antisymm (max_eq_left_of_lt h ▸ degree_add_le _ _) $ degree_le_degree $
   begin
-    rw [coeff_add, coeff_nat_degree_eq_zero_of_degree_lt h, zero_add],
+    rw [coeff_add, coeff_nat_degree_eq_zero_of_degree_lt h, add_zero],
     exact mt leading_coeff_eq_zero.1 (ne_zero_of_degree_gt h)
   end
 
+lemma degree_add_eq_right_of_degree_lt (h : degree p < degree q) : degree (p + q) = degree q :=
+by rw [add_comm, degree_add_eq_left_of_degree_lt h]
 
 lemma degree_add_C (hp : 0 < degree p) : degree (p + C a) = degree p :=
-add_comm (C a) p ▸ degree_add_eq_of_degree_lt $ lt_of_le_of_lt degree_C_le hp
+add_comm (C a) p ▸ degree_add_eq_right_of_degree_lt $ lt_of_le_of_lt degree_C_le hp
 
 lemma degree_add_eq_of_leading_coeff_add_ne_zero (h : leading_coeff p + leading_coeff q ≠ 0) :
   degree (p + q) = max p.degree q.degree :=
 le_antisymm (degree_add_le _ _) $
   match lt_trichotomy (degree p) (degree q) with
   | or.inl hlt :=
-    by rw [degree_add_eq_of_degree_lt hlt, max_eq_right_of_lt hlt]; exact le_refl _
+    by rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]; exact le_refl _
   | or.inr (or.inl heq) :=
     le_of_not_gt $
       assume hlt : max (degree p) (degree q) > degree (p + q),
@@ -474,7 +476,7 @@ le_antisymm (degree_add_le _ _) $
         exact coeff_nat_degree_eq_zero_of_degree_lt hlt
       end
   | or.inr (or.inr hlt) :=
-    by rw [add_comm, degree_add_eq_of_degree_lt hlt, max_eq_left_of_lt hlt]; exact le_refl _
+    by rw [degree_add_eq_left_of_degree_lt hlt, max_eq_left_of_lt hlt]; exact le_refl _
   end
 
 lemma degree_erase_le (p : polynomial R) (n : ℕ) : degree (p.erase n) ≤ degree p :=
@@ -553,7 +555,7 @@ by { haveI := nontrivial.of_polynomial_ne hne, exact hp.ne_zero }
 lemma leading_coeff_add_of_degree_lt (h : degree p < degree q) :
   leading_coeff (p + q) = leading_coeff q :=
 have coeff p (nat_degree q) = 0, from coeff_nat_degree_eq_zero_of_degree_lt h,
-by simp only [leading_coeff, nat_degree_eq_of_degree_eq (degree_add_eq_of_degree_lt h),
+by simp only [leading_coeff, nat_degree_eq_of_degree_eq (degree_add_eq_right_of_degree_lt h),
   this, coeff_add, zero_add]
 
 lemma leading_coeff_add_of_degree_eq (h : degree p = degree q)
@@ -770,18 +772,42 @@ lemma nat_degree_X_sub_C_le {r : R} : (X - C r).nat_degree ≤ 1 :=
 nat_degree_le_iff_degree_le.2 $ le_trans (degree_sub_le _ _) $ max_le degree_X_le $
 le_trans degree_C_le $ with_bot.coe_le_coe.2 zero_le_one
 
+lemma degree_sum_fin_lt {n : ℕ} (f : fin n → R) :
+  degree (∑ i : fin n, C (f i) * X ^ (i : ℕ)) < n :=
+begin
+  haveI : is_commutative (with_bot ℕ) max := ⟨max_comm⟩,
+  haveI : is_associative (with_bot ℕ) max := ⟨max_assoc⟩,
+  calc  (∑ i, C (f i) * X ^ (i : ℕ)).degree
+      ≤ finset.univ.fold (⊔) ⊥ (λ i, (C (f i) * X ^ (i : ℕ)).degree) : degree_sum_le _ _
+  ... = finset.univ.fold max ⊥ (λ i, (C (f i) * X ^ (i : ℕ)).degree) :
+    (@finset.fold_hom _ _ _ (⊔) _ _ _ ⊥ finset.univ _ _ _ id (with_bot.sup_eq_max)).symm
+  ... < n : (finset.fold_max_lt (n : with_bot ℕ)).mpr ⟨with_bot.bot_lt_some _, _⟩,
+
+  rintros ⟨i, hi⟩ -,
+  calc (C (f ⟨i, hi⟩) * X ^ i).degree
+      ≤ (C _).degree + (X ^ i).degree : degree_mul_le _ _
+  ... ≤ 0 + i : add_le_add degree_C_le (degree_X_pow_le i)
+  ... = i : zero_add _
+  ... < n : with_bot.some_lt_some.mpr hi,
+end
+
+lemma degree_sub_eq_left_of_degree_lt (h : degree q < degree p) : degree (p - q) = degree p :=
+by { rw ← degree_neg q at h, rw [sub_eq_add_neg, degree_add_eq_left_of_degree_lt h] }
+
+lemma degree_sub_eq_right_of_degree_lt (h : degree p < degree q) : degree (p - q) = degree q :=
+by { rw ← degree_neg q at h, rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg] }
+
 end ring
 
 section nonzero_ring
 variables [nontrivial R] [ring R]
 
 @[simp] lemma degree_X_sub_C (a : R) : degree (X - C a) = 1 :=
-begin
-  rw [sub_eq_add_neg, add_comm, ← @degree_X R],
-  by_cases ha : a = 0,
-  { simp only [ha, C_0, neg_zero, zero_add] },
-  exact degree_add_eq_of_degree_lt (by rw [degree_X, degree_neg, degree_C ha]; exact dec_trivial)
-end
+have degree (C a) < degree (X : polynomial R),
+from calc degree (C a) ≤ 0 : degree_C_le
+                   ... < 1 : with_bot.some_lt_some.mpr zero_lt_one
+                   ... = degree X : degree_X.symm,
+by rw [degree_sub_eq_left_of_degree_lt this, degree_X]
 
 @[simp] lemma nat_degree_X_sub_C (x : R) : (X - C x).nat_degree = 1 :=
 nat_degree_eq_of_degree_eq_some $ degree_X_sub_C x
@@ -792,11 +818,11 @@ by simp [next_coeff_of_pos_nat_degree]
 
 lemma degree_X_pow_sub_C {n : ℕ} (hn : 0 < n) (a : R) :
   degree ((X : polynomial R) ^ n - C a) = n :=
-have degree (-C a) < degree ((X : polynomial R) ^ n),
-  from calc degree (-C a) ≤ 0 : by rw degree_neg; exact degree_C_le
+have degree (C a) < degree ((X : polynomial R) ^ n),
+  from calc degree (C a) ≤ 0 : degree_C_le
   ... < degree ((X : polynomial R) ^ n) : by rwa [degree_X_pow];
     exact with_bot.coe_lt_coe.2 hn,
-by rw [sub_eq_add_neg, add_comm, degree_add_eq_of_degree_lt this, degree_X_pow]
+by rw [degree_sub_eq_left_of_degree_lt this, degree_X_pow]
 
 lemma X_pow_sub_C_ne_zero {n : ℕ} (hn : 0 < n) (a : R) :
   (X : polynomial R) ^ n - C a ≠ 0 :=

src/data/polynomial/div.lean

@@ -100,7 +100,7 @@ calc (div_X p).degree < (div_X p * X + C (p.coeff 0)).degree :
               (by rw [zero_le_degree_iff, ne.def, div_X_eq_zero_iff];
                 exact λ h0, h (h0.symm ▸ degree_C_le))
               (le_refl _),
-    by rw [add_comm, degree_add_eq_of_degree_lt this];
+    by rw [degree_add_eq_left_of_degree_lt this];
       exact degree_lt_degree_mul_X hXp0
 ... = p.degree : by rw div_X_mul_X_add
 
@@ -364,7 +364,7 @@ have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
       degree_eq_nat_degree hdiv0, ← with_bot.coe_add, with_bot.coe_le_coe];
     exact nat.le_add_right _ _,
 calc degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) : eq.symm (degree_mul' hlc)
-... = degree (p %ₘ q + q * (p /ₘ q)) : (degree_add_eq_of_degree_lt hmod).symm
+... = degree (p %ₘ q + q * (p /ₘ q)) : (degree_add_eq_right_of_degree_lt hmod).symm
 ... = _ : congr_arg _ (mod_by_monic_add_div _ hq)
 
 lemma degree_div_by_monic_le (p q : polynomial R) : degree (p /ₘ q) ≤ degree p :=
@@ -538,6 +538,11 @@ lemma dvd_iff_is_root : (X - C a) ∣ p ↔ is_root p a :=
 lemma mod_by_monic_X (p : polynomial R) : p %ₘ X = C (p.eval 0) :=
 by rw [← mod_by_monic_X_sub_C_eq_C_eval, C_0, sub_zero]
 
+lemma eval₂_mod_by_monic_eq_self_of_root [comm_ring S] {f : R →+* S}
+  {p q : polynomial R} (hq : q.monic) {x : S} (hx : q.eval₂ f x = 0) :
+  (p %ₘ q).eval₂ f x = p.eval₂ f x :=
+by rw [mod_by_monic_eq_sub_mul_div p hq, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]
+
 section multiplicity
 /-- An algorithm for deciding polynomial divisibility.
 The algorithm is "compute `p %ₘ q` and compare to `0`". `

src/data/polynomial/eval.lean

@@ -188,6 +188,14 @@ lemma eval₂_eq_sum_range :
   p.eval₂ f x = ∑ i in finset.range (p.nat_degree + 1), f (p.coeff i) * x^i :=
 trans (congr_arg _ p.as_sum_range) (trans (eval₂_finset_sum f _ _ x) (congr_arg _ (by simp)))
 
+lemma eval₂_eq_sum_range' (f : R →+* S) {p : polynomial R} {n : ℕ} (hn : p.nat_degree < n) (x : S) :
+  eval₂ f x p = ∑ i in finset.range n, f (p.coeff i) * x ^ i :=
+begin
+  rw [eval₂_eq_sum, p.sum_over_range' _ _ hn],
+  intro i,
+  rw [f.map_zero, zero_mul]
+end
+
 end eval₂
 
 section eval

src/data/polynomial/field_division.lean

@@ -175,8 +175,8 @@ lemma degree_add_div (hq0 : q ≠ 0) (hpq : degree q ≤ degree p) :
 have degree (p % q) < degree (q * (p / q)) :=
   calc degree (p % q) < degree q : euclidean_domain.mod_lt _ hq0
   ... ≤ _ : degree_le_mul_left _ (mt (div_eq_zero_iff hq0).1 (not_lt_of_ge hpq)),
-by conv {to_rhs, rw [← euclidean_domain.div_add_mod p q, add_comm,
-    degree_add_eq_of_degree_lt this, degree_mul]}
+by conv_rhs { rw [← euclidean_domain.div_add_mod p q,
+    degree_add_eq_left_of_degree_lt this, degree_mul] }
 
 lemma degree_div_le (p q : polynomial R) : degree (p / q) ≤ degree p :=
 if hq : q = 0 then by simp [hq]

src/data/polynomial/lifts.lean

@@ -177,7 +177,7 @@ begin
   rw [←hdeg, erase_lead] at deg_erase,
   replace deg_erase := lt_of_le_of_lt degree_le_nat_degree (with_bot.coe_lt_coe.2 deg_erase),
   rw [← deg_lead, ← herase.2] at deg_erase,
-  rw [degree_add_eq_of_degree_lt deg_erase, deg_lead, degree_eq_nat_degree pzero]
+  rw [degree_add_eq_right_of_degree_lt deg_erase, deg_lead, degree_eq_nat_degree pzero]
 end
 
 end lift_deg
@@ -213,7 +213,7 @@ begin
   { simp only [hq, map_add, map_pow, map_X],
     nth_rewrite 3 [← erase_lead_add_C_mul_X_pow p],
     rw [erase_lead, monic.leading_coeff hmonic, C_1, one_mul] },
-  { rw [degree_add_eq_of_degree_lt deg_er, @degree_X_pow R _ Rtrivial p.nat_degree,
+  { rw [degree_add_eq_right_of_degree_lt deg_er, @degree_X_pow R _ Rtrivial p.nat_degree,
     degree_eq_nat_degree (monic.ne_zero hmonic)] },
   { rw [monic.def, leading_coeff_add_of_degree_lt deg_er],
     exact monic_pow monic_X p.nat_degree }

src/data/polynomial/monic.lean

@@ -92,6 +92,14 @@ lemma monic_pow (hp : monic p) : ∀ (n : ℕ), monic (p ^ n)
 | 0     := monic_one
 | (n+1) := monic_mul hp (monic_pow n)
 
+lemma monic_add_of_left {p q : polynomial R} (hp : monic p) (hpq : degree q < degree p) :
+  monic (p + q) :=
+by rwa [monic, add_comm, leading_coeff_add_of_degree_lt hpq]
+
+lemma monic_add_of_right {p q : polynomial R} (hq : monic q) (hpq : degree p < degree q) :
+  monic (p + q) :=
+by rwa [monic, leading_coeff_add_of_degree_lt hpq]
+
 end semiring
 
 section comm_semiring

src/data/polynomial/ring_division.lean

@@ -40,6 +40,11 @@ lemma degree_pos_of_aeval_root [algebra R S] {p : polynomial R} (hp : p ≠ 0)
   0 < p.degree :=
 nat_degree_pos_iff_degree_pos.mp (nat_degree_pos_of_aeval_root hp hz inj)
 
+lemma aeval_mod_by_monic_eq_self_of_root [algebra R S]
+  {p q : polynomial R} (hq : q.monic) {x : S} (hx : aeval x q = 0) :
+  aeval x (p %ₘ q) = aeval x p :=
+eval₂_mod_by_monic_eq_self_of_root hq hx
+
 end comm_ring
 
 section integral_domain

src/field_theory/minimal_polynomial.lean

@@ -59,6 +59,10 @@ lemma min {p : polynomial α} (pmonic : p.monic) (hp : polynomial.aeval x p = 0)
   degree (minimal_polynomial hx) ≤ degree p :=
 le_of_not_lt $ well_founded.not_lt_min degree_lt_wf _ hx ⟨pmonic, hp⟩
 
+/-- A minimal polynomial is nonzero. -/
+lemma ne_zero [nontrivial α] : (minimal_polynomial hx) ≠ 0 :=
+ne_zero_of_monic (monic hx)
+
 end ring
 
 section field
@@ -68,10 +72,6 @@ section ring
 variables [ring β] [algebra α β]
 variables {x : β} (hx : is_integral α x)
 
-/--A minimal polynomial is nonzero.-/
-lemma ne_zero : (minimal_polynomial hx) ≠ 0 :=
-ne_zero_of_monic (monic hx)
-
 /--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.-/
 lemma degree_le_of_ne_zero

src/linear_algebra/char_poly/coeff.lean

@@ -92,7 +92,7 @@ begin
   { rw degree_eq_iff_nat_degree_eq_of_pos, swap, apply nat.pos_of_ne_zero h,
     rw nat_degree_prod', simp_rw nat_degree_X_sub_C, unfold fintype.card, simp,
     simp_rw (monic_X_sub_C _).leading_coeff, simp, },
-  rw degree_add_eq_of_degree_lt, exact h1, rw h1,
+  rw degree_add_eq_right_of_degree_lt, exact h1, rw h1,
   apply lt_trans (char_poly_sub_diagonal_degree_lt M), rw with_bot.coe_lt_coe,
   rw ← nat.pred_eq_sub_one, apply nat.pred_lt, apply h,
 end