From d788647f8de7374ffa3b529f59394a7b76685d79 Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Sun, 24 Oct 2021 00:37:37 +0000 Subject: [PATCH] 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 --- src/data/polynomial/div.lean | 22 +++++++++ src/ring_theory/adjoin_root.lean | 78 ++++++++++++++++++++++++++++++++ 2 files changed, 100 insertions(+) diff --git a/src/data/polynomial/div.lean b/src/data/polynomial/div.lean index 2f68b60bb390a..b426f79fcdc5c 100644 --- a/src/data/polynomial/div.lean +++ b/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`". ` diff --git a/src/ring_theory/adjoin_root.lean b/src/ring_theory/adjoin_root.lean index a3aebb694e750..17b0abe8a585d 100644 --- a/src/ring_theory/adjoin_root.lean +++ b/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) :=