feat(ring_theory): generalize adjoin_root.power_basis (#9536)

Now we only need that `g` is monic to state that `adjoin_root g` has a power basis. Note that this does not quite imply the result of #9529: this is phrased in terms of `minpoly R (root g)` and the other PR in terms of `g` itself, so I don't have a direct use for the current PR. However, it seems useful enough to have this statement, so I PR'd it anyway.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/data/polynomial/div.lean

@@ -396,6 +396,28 @@ lemma eval₂_mod_by_monic_eq_self_of_root [comm_ring S] {f : R →+* S}
   (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]
 
+lemma sum_fin [add_comm_monoid S] (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0)
+  {n : ℕ} (hn : p.degree < n) :
+  ∑ (i : fin n), f i (p.coeff i) = p.sum f :=
+begin
+  by_cases hp : p = 0,
+  { rw [hp, sum_zero_index, finset.sum_eq_zero], intros i _, exact hf i },
+  rw [degree_eq_nat_degree hp, with_bot.coe_lt_coe] at hn,
+  calc  ∑ (i : fin n), f i (p.coeff i)
+      = ∑ i in finset.range n, f i (p.coeff i) : fin.sum_univ_eq_sum_range (λ i, f i (p.coeff i)) _
+  ... = ∑ i in p.support, f i (p.coeff i) : (finset.sum_subset
+    (supp_subset_range_nat_degree_succ.trans (finset.range_subset.mpr hn))
+    (λ i _ hi, show f i (p.coeff i) = 0, by rw [not_mem_support_iff.mp hi, hf])).symm
+  ... = p.sum f : p.sum_def _
+end
+
+lemma sum_mod_by_monic_coeff [nontrivial R] (hq : q.monic)
+  {n : ℕ} (hn : q.degree ≤ n) :
+  ∑ (i : fin n), monomial i ((p %ₘ q).coeff i) = p %ₘ q :=
+(sum_fin (λ i c, monomial i c) (by simp)
+  ((degree_mod_by_monic_lt _ hq).trans_le hn)).trans
+  (sum_monomial_eq _)
+
 section multiplicity
 /-- An algorithm for deciding polynomial divisibility.
 The algorithm is "compute `p %ₘ q` and compare to `0`". `

src/ring_theory/adjoin_root.lean

@@ -90,6 +90,9 @@ variables {f}
 
 instance adjoin_root.has_coe_t : has_coe_t R (adjoin_root f) := ⟨of f⟩
 
+@[simp] lemma mk_eq_mk {g h : polynomial R} : mk f g = mk f h ↔ f ∣ g - h :=
+ideal.quotient.eq.trans ideal.mem_span_singleton
+
 @[simp] lemma mk_self : mk f f = 0 :=
 quotient.sound' (mem_span_singleton.2 $ by simp)
 
@@ -205,6 +208,81 @@ end irreducible
 
 section power_basis
 
+variables [comm_ring R] {g : polynomial R}
+
+lemma is_integral_root' (hg : g.monic) : is_integral R (root g) :=
+⟨g, hg, eval₂_root g⟩
+
+/-- `adjoin_root.mod_by_monic_hom` sends the equivalence class of `f` mod `g` to `f %ₘ g`.
+
+This is a well-defined right inverse to `adjoin_root.mk`, see `adjoin_root.mk_left_inverse`. -/
+def mod_by_monic_hom [nontrivial R] (hg : g.monic) :
+  adjoin_root g →ₗ[R] polynomial R :=
+(submodule.liftq _ (polynomial.mod_by_monic_hom hg)
+  (λ f (hf : f ∈ (ideal.span {g}).restrict_scalars R),
+    (mem_ker_mod_by_monic hg).mpr (ideal.mem_span_singleton.mp hf))).comp $
+(submodule.quotient.restrict_scalars_equiv R (ideal.span {g} : ideal (polynomial R)))
+  .symm.to_linear_map
+
+@[simp] lemma mod_by_monic_hom_mk [nontrivial R] (hg : g.monic) (f : polynomial R) :
+  mod_by_monic_hom hg (mk g f) = f %ₘ g := rfl
+
+lemma mk_left_inverse [nontrivial R] (hg : g.monic) :
+  function.left_inverse (mk g) (mod_by_monic_hom hg) :=
+λ f, induction_on g f $ λ f, begin
+  rw [mod_by_monic_hom_mk hg, mk_eq_mk, mod_by_monic_eq_sub_mul_div _ hg,
+      sub_sub_cancel_left, dvd_neg],
+  apply dvd_mul_right
+end
+
+lemma mk_surjective [nontrivial R] (hg : g.monic) : function.surjective (mk g) :=
+(mk_left_inverse hg).surjective
+
+/-- The elements `1, root g, ..., root g ^ (d - 1)` form a basis for `adjoin_root g`,
+where `g` is a monic polynomial of degree `d`. -/
+@[simps] def power_basis_aux' [nontrivial R] (hg : g.monic) :
+  basis (fin g.nat_degree) R (adjoin_root g) :=
+basis.of_equiv_fun
+{ to_fun := λ f i, (mod_by_monic_hom hg f).coeff i,
+  inv_fun := λ c, mk g $ ∑ (i : fin g.nat_degree), monomial i (c i),
+  map_add' := λ f₁ f₂, funext $ λ i,
+    by simp only [(mod_by_monic_hom hg).map_add, coeff_add, pi.add_apply],
+  map_smul' := λ f₁ f₂, funext $ λ i,
+    by simp only [(mod_by_monic_hom hg).map_smul, coeff_smul, pi.smul_apply, ring_hom.id_apply],
+  left_inv := λ f, induction_on g f (λ f, eq.symm $ mk_eq_mk.mpr $
+    by { simp only [mod_by_monic_hom_mk, sum_mod_by_monic_coeff hg degree_le_nat_degree],
+         rw [mod_by_monic_eq_sub_mul_div _ hg, sub_sub_cancel],
+         exact dvd_mul_right _ _ }),
+  right_inv := λ x, funext $ λ i, begin
+    simp only [mod_by_monic_hom_mk],
+    rw [(mod_by_monic_eq_self_iff hg).mpr, finset_sum_coeff, finset.sum_eq_single i];
+      try { simp only [coeff_monomial, eq_self_iff_true, if_true] },
+    { intros j _ hj, exact if_neg (fin.coe_injective.ne hj) },
+    { intros, have := finset.mem_univ i, contradiction },
+    { refine (degree_sum_le _ _).trans_lt ((finset.sup_lt_iff _).mpr (λ j _, _)),
+      { exact bot_lt_iff_ne_bot.mpr (mt degree_eq_bot.mp hg.ne_zero) },
+      { refine (degree_monomial_le _ _).trans_lt _,
+        rw [degree_eq_nat_degree hg.ne_zero, with_bot.coe_lt_coe],
+        exact j.2 } },
+  end}
+
+/-- The power basis `1, root g, ..., root g ^ (d - 1)` for `adjoin_root g`,
+where `g` is a monic polynomial of degree `d`. -/
+@[simps] def power_basis' [nontrivial R] (hg : g.monic) :
+  power_basis R (adjoin_root g) :=
+{ gen := root g,
+  dim := g.nat_degree,
+  basis := power_basis_aux' hg,
+  basis_eq_pow := λ i, begin
+    simp only [power_basis_aux', basis.coe_of_equiv_fun, linear_equiv.coe_symm_mk],
+    rw finset.sum_eq_single i,
+    { rw [function.update_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X] },
+    { intros j _ hj,
+      rw ← monomial_zero_right _,
+      convert congr_arg _ (function.update_noteq hj _ _) }, -- Fix `decidable_eq` mismatch
+    { intros, have := finset.mem_univ i, contradiction },
+  end}
+
 variables [field K] {f : polynomial K}
 
 lemma is_integral_root (hf : f ≠ 0) : is_integral K (root f) :=