From 964f0e53fd21a434c0ce50b3cd1111d6fb5146a0 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 29 Jun 2020 13:48:26 +0000 Subject: [PATCH] feat(data/polynomial): work over noncommutative rings where possible (#3193) After downgrading `C` from an algebra homomorphism to a ring homomorphism in [69931ac](https://github.com/leanprover-community/mathlib/commit/69931acfe7b6a29f988bcf7094e090767b34fb85), which requires a few tweaks, everything else is straightforward. Co-authored-by: Scott Morrison Co-authored-by: Alex J. Best --- src/data/finsupp.lean | 2 +- src/data/monoid_algebra.lean | 31 +- src/data/polynomial.lean | 719 +++++++++++++++++----------- src/ring_theory/free_comm_ring.lean | 2 +- src/ring_theory/localization.lean | 2 +- 5 files changed, 461 insertions(+), 295 deletions(-) diff --git a/src/data/finsupp.lean b/src/data/finsupp.lean index 00d31725f5c60..557190db191aa 100644 --- a/src/data/finsupp.lean +++ b/src/data/finsupp.lean @@ -1486,7 +1486,7 @@ end (b • v) a = b • (v a) := rfl -lemma sum_smul_index [ring β] [add_comm_monoid γ] {g : α →₀ β} {b : β} {h : α → β → γ} +lemma sum_smul_index [semiring β] [add_comm_monoid γ] {g : α →₀ β} {b : β} {h : α → β → γ} (h0 : ∀i, h i 0 = 0) : (b • g).sum h = g.sum (λi a, h i (b * a)) := finsupp.sum_map_range_index h0 diff --git a/src/data/monoid_algebra.lean b/src/data/monoid_algebra.lean index 90d61f8b62bce..451baaeda9cdb 100644 --- a/src/data/monoid_algebra.lean +++ b/src/data/monoid_algebra.lean @@ -236,14 +236,22 @@ lemma single_one_comm [comm_semiring k] [monoid G] (r : k) (f : monoid_algebra k single 1 r * f = f * single 1 r := by { ext, rw [single_one_mul_apply, mul_single_one_apply, mul_comm] } -instance [comm_semiring k] [monoid G] : algebra k (monoid_algebra k G) := +/-- +As a preliminary to defining the `k`-algebra structure on `add_monoid_algebra k G`, +we define the underlying ring homomorphism. +-/ +def algebra_map' [semiring k] [monoid G] : k →+* monoid_algebra k G := { to_fun := single 1, map_one' := rfl, map_mul' := λ x y, by rw [single_mul_single, one_mul], map_zero' := single_zero, - map_add' := λ x y, single_add, - smul_def' := λ r a, ext (λ _, smul_apply.trans (single_one_mul_apply _ _ _).symm), - commutes' := λ r f, ext $ λ _, by rw [single_one_mul_apply, mul_single_one_apply, mul_comm] } + map_add' := λ x y, single_add, } + +instance [comm_semiring k] [monoid G] : algebra k (monoid_algebra k G) := +{ smul_def' := λ r a, ext (λ _, smul_apply.trans (single_one_mul_apply _ _ _).symm), + commutes' := λ r f, ext $ λ _, + by simp [algebra_map', single_one_mul_apply, mul_single_one_apply, mul_comm], + ..algebra_map' } @[simp] lemma coe_algebra_map [comm_semiring k] [monoid G] : (algebra_map k (monoid_algebra k G) : k → monoid_algebra k G) = single 1 := @@ -579,15 +587,22 @@ finsupp.has_scalar instance [semiring k] : semimodule k (add_monoid_algebra k G) := finsupp.semimodule G k -instance [comm_semiring k] [add_monoid G] : algebra k (add_monoid_algebra k G) := +/-- +As a preliminary to defining the `k`-algebra structure on `add_monoid_algebra k G`, +we define the underlying ring homomorphism. +-/ +def algebra_map' [semiring k] [add_monoid G] : k →+* add_monoid_algebra k G := { to_fun := single 0, map_one' := rfl, map_mul' := λ x y, by rw [single_mul_single, zero_add], map_zero' := single_zero, - map_add' := λ x y, single_add, - smul_def' := λ r a, by { ext x, exact smul_apply.trans (single_zero_mul_apply _ _ _).symm }, + map_add' := λ x y, single_add, } + +instance [comm_semiring k] [add_monoid G] : algebra k (add_monoid_algebra k G) := +{ smul_def' := λ r a, by { ext x, exact smul_apply.trans (single_zero_mul_apply _ _ _).symm }, commutes' := λ r f, show single 0 r * f = f * single 0 r, - by ext; rw [single_zero_mul_apply, mul_single_zero_apply, mul_comm] } + by ext; rw [single_zero_mul_apply, mul_single_zero_apply, mul_comm], + ..algebra_map', } @[simp] lemma coe_algebra_map [comm_semiring k] [add_monoid G] : (algebra_map k (add_monoid_algebra k G) : k → add_monoid_algebra k G) = single 0 := diff --git a/src/data/polynomial.lean b/src/data/polynomial.lean index 9936fe60789ae..2a4f53ef057d8 100644 --- a/src/data/polynomial.lean +++ b/src/data/polynomial.lean @@ -59,6 +59,24 @@ def monomial (n : ℕ) (a : R) : polynomial R := finsupp.single n a /-- `X` is the polynomial variable (aka indeterminant). -/ def X : polynomial R := monomial 1 1 +/-- `X` commutes with everything, even when the coefficients are noncommutative. -/ +lemma X_mul : X * p = p * X := +begin + ext, + simp [X, monomial, add_monoid_algebra.mul_apply, sum_single_index, add_comm], +end + +lemma X_pow_mul {n : ℕ} : X^n * p = p * X^n := +begin + induction n with n ih, + { simp, }, + { conv_lhs { rw pow_succ', }, + rw [mul_assoc, X_mul, ←mul_assoc, ih, mul_assoc, ←pow_succ'], } +end + +lemma X_pow_mul_assoc {n : ℕ} : (p * X^n) * q = (p * q) * X^n := +by rw [mul_assoc, X_pow_mul, ←mul_assoc] + /-- coeff p n is the coefficient of X^n in p -/ def coeff (p : polynomial R) := p.to_fun @@ -187,24 +205,9 @@ ext $ λ k, (coeff_mul_X_pow p n k).symm.trans $ ext_iff.1 H (k+n) end coeff -end semiring - -section ring -variables [ring R] - -instance : ring (polynomial R) := add_monoid_algebra.ring -end ring - -section comm_semiring -variables [comm_semiring R] {p q r : polynomial R} - -local attribute [instance] coeff_coe_to_fun - -instance : comm_semiring (polynomial R) := add_monoid_algebra.comm_semiring -instance : algebra R (polynomial R) := add_monoid_algebra.algebra - +section C /-- `C a` is the constant polynomial `a`. -/ -def C : R →ₐ[R] polynomial R := algebra.of_id R (polynomial R) +def C : R →+* polynomial R := add_monoid_algebra.algebra_map' lemma C_def (a : R) : C a = single 0 a := rfl @@ -245,12 +248,15 @@ lemma C_mul : C (a * b) = C a * C b := C.map_mul a b lemma C_add : C (a + b) = C a + C b := C.map_add a b instance C.is_semiring_hom : is_semiring_hom (C : R → polynomial R) := -C.to_ring_hom.is_semiring_hom +C.is_semiring_hom lemma C_pow : C (a ^ n) = C a ^ n := C.map_pow a n -lemma nat_cast_eq_C (n : ℕ) : (n : polynomial R) = C (n : R) := -(C.to_ring_hom.map_nat_cast n).symm +@[simp] +lemma C_eq_nat_cast (n : ℕ) : C (n : R) = (n : polynomial R) := +C.map_nat_cast n + +end C section coeff @@ -273,14 +279,18 @@ begin { simp [finsupp.sum] } end +end coeff + +section C + lemma C_mul' (a : R) (f : polynomial R) : C a * f = a • f := ext $ λ n, coeff_C_mul f -end coeff - lemma C_inj : C a = C b ↔ a = b := ⟨λ h, coeff_C_zero.symm.trans (h.symm ▸ coeff_C_zero), congr_arg C⟩ +end C + section eval₂ variables [semiring S] variables (f : R → S) (x : S) @@ -310,45 +320,16 @@ finsupp.sum_add_index @[simp] lemma eval₂_one : (1 : polynomial R).eval₂ f x = 1 := by rw [← C_1, eval₂_C, map_one f] -instance eval₂.is_add_monoid_hom : is_add_monoid_hom (eval₂ f x) := -{ map_zero := eval₂_zero _ _, map_add := λ _ _, eval₂_add _ _ } - -end eval₂ - -section eval₂ -variables [comm_semiring S] -variables (f : R → S) [is_semiring_hom f] (x : S) -open is_semiring_hom - -@[simp] lemma eval₂_mul : (p * q).eval₂ f x = p.eval₂ f x * q.eval₂ f x := +@[simp] lemma eval₂_smul (g : R →+* S) (p : polynomial R) (x : S) {s : R} : + eval₂ g x (s • p) = g s • eval₂ g x p := begin - dunfold eval₂, - rw [mul_def, finsupp.sum_mul _ p], simp only [finsupp.mul_sum _ q], rw [sum_sum_index], - { apply sum_congr rfl, assume i hi, dsimp only, rw [sum_sum_index], - { apply sum_congr rfl, assume j hj, dsimp only, - rw [sum_single_index, map_mul f, pow_add], - { simp only [mul_assoc, mul_left_comm] }, - { rw [map_zero f, zero_mul] } }, - { intro, rw [map_zero f, zero_mul] }, - { intros, rw [map_add f, add_mul] } }, - { intro, rw [map_zero f, zero_mul] }, - { intros, rw [map_add f, add_mul] } + simp only [eval₂, sum_smul_index, forall_const, zero_mul, g.map_zero, g.map_mul, mul_assoc], + -- Why doesn't `rw [←finsupp.mul_sum]` work? + convert (@finsupp.mul_sum _ _ _ _ _ (g s) p (λ i a, (g a * x ^ i))).symm, end -lemma eval₂_smul (g : R →+* S) (p : polynomial R) (x : S) {s : R} : - eval₂ g x (s • p) = g s * eval₂ g x p := -by rw [← C_mul', eval₂_mul, eval₂_C] - -instance eval₂.is_semiring_hom : is_semiring_hom (eval₂ f x) := -⟨eval₂_zero _ _, eval₂_one _ _, λ _ _, eval₂_add _ _, λ _ _, eval₂_mul _ _⟩ - -/-- `eval₂` as a `ring_hom` -/ -def eval₂_ring_hom (f : R →+* S) (x) : polynomial R →+* S := -ring_hom.of (eval₂ f x) - -@[simp] lemma coe_eval₂_ring_hom (f : R →+* S) (x) : ⇑(eval₂_ring_hom f x) = eval₂ f x := rfl - -lemma eval₂_pow (n : ℕ) : (p ^ n).eval₂ f x = p.eval₂ f x ^ n := map_pow _ _ _ +instance eval₂.is_add_monoid_hom : is_add_monoid_hom (eval₂ f x) := +{ map_zero := eval₂_zero _ _, map_add := λ _ _, eval₂_add _ _ } lemma eval₂_sum (p : polynomial R) (g : ℕ → R → polynomial R) (x : S) : (p.sum g).eval₂ f x = p.sum (λ n a, (g n a).eval₂ f x) := @@ -365,6 +346,9 @@ def eval : R → polynomial R → R := eval₂ id @[simp] lemma eval_C : (C a).eval x = a := eval₂_C _ _ +@[simp] lemma eval_nat_cast {n : ℕ} : (n : polynomial R).eval x = n := +by simp only [←C_eq_nat_cast, eval_C] + @[simp] lemma eval_X : X.eval x = x := eval₂_X _ _ @[simp] lemma eval_zero : (0 : polynomial R).eval x = 0 := eval₂_zero _ _ @@ -373,24 +357,14 @@ def eval : R → polynomial R → R := eval₂ id @[simp] lemma eval_one : (1 : polynomial R).eval x = 1 := eval₂_one _ _ -@[simp] lemma eval_mul : (p * q).eval x = p.eval x * q.eval x := eval₂_mul _ _ - -instance eval.is_semiring_hom : is_semiring_hom (eval x) := eval₂.is_semiring_hom _ _ - -@[simp] lemma eval_pow (n : ℕ) : (p ^ n).eval x = p.eval x ^ n := eval₂_pow _ _ _ +@[simp] lemma eval_smul (p : polynomial R) (x : R) {s : R} : + (s • p).eval x = s • p.eval x := +eval₂_smul (ring_hom.id _) _ _ lemma eval_sum (p : polynomial R) (f : ℕ → R → polynomial R) (x : R) : (p.sum f).eval x = p.sum (λ n a, (f n a).eval x) := eval₂_sum _ _ _ _ -lemma eval₂_hom [comm_semiring S] (f : R → S) [is_semiring_hom f] (x : R) : - p.eval₂ f (f x) = f (p.eval x) := -polynomial.induction_on p - (by simp) - (by simp [is_semiring_hom.map_add f] {contextual := tt}) - (by simp [is_semiring_hom.map_mul f, eval_pow, - is_semiring_hom.map_pow f, pow_succ', (mul_assoc _ _ _).symm] {contextual := tt}) - /-- `is_root p x` implies `x` is a root of `p`. The evaluation of `p` at `x` is zero -/ def is_root (p : polynomial R) (a : R) : Prop := p.eval a = 0 @@ -398,14 +372,6 @@ instance [decidable_eq R] : decidable (is_root p a) := by unfold is_root; apply_ @[simp] lemma is_root.def : is_root p a ↔ p.eval a = 0 := iff.rfl -lemma root_mul_left_of_is_root (p : polynomial R) {q : polynomial R} : - is_root q a → is_root (p * q) a := -λ H, by rw [is_root, eval_mul, is_root.def.1 H, mul_zero] - -lemma root_mul_right_of_is_root {p : polynomial R} (q : polynomial R) : - is_root p a → is_root (p * q) a := -λ H, by rw [is_root, eval_mul, is_root.def.1 H, zero_mul] - lemma coeff_zero_eq_eval_zero (p : polynomial R) : coeff p 0 = p.eval 0 := calc coeff p 0 = coeff p 0 * 0 ^ 0 : by simp @@ -422,12 +388,6 @@ section comp def comp (p q : polynomial R) : polynomial R := p.eval₂ C q -lemma eval₂_comp [comm_semiring S] (f : R → S) [is_semiring_hom f] {x : S} : - (p.comp q).eval₂ f x = p.eval₂ f (q.eval₂ f x) := -show (p.sum (λ e a, C a * q ^ e)).eval₂ f x = p.eval₂ f (eval₂ f x q), -by simp only [eval₂_mul, eval₂_C, eval₂_pow, eval₂_sum]; refl - -lemma eval_comp : (p.comp q).eval a = p.eval (q.eval a) := eval₂_comp _ @[simp] lemma comp_X : p.comp X = p := begin @@ -460,10 +420,103 @@ by rw [← C_1, comp_C] @[simp] lemma one_comp : comp (1 : polynomial R) p = 1 := by rw [← C_1, C_comp] +@[simp] lemma add_comp : (p + q).comp r = p.comp r + q.comp r := eval₂_add _ _ + +end comp + +/-! +We next prove that eval₂ is multiplicative +as long as target ring is commutative +(even if the source ring is not). +-/ +section eval₂ +variables [comm_semiring S] +variables (f : R → S) [is_semiring_hom f] (x : S) +open is_semiring_hom + +@[simp] lemma eval₂_mul : (p * q).eval₂ f x = p.eval₂ f x * q.eval₂ f x := +begin + dunfold eval₂, + rw [mul_def, finsupp.sum_mul _ p], simp only [finsupp.mul_sum _ q], rw [sum_sum_index], + { apply sum_congr rfl, assume i hi, dsimp only, rw [sum_sum_index], + { apply sum_congr rfl, assume j hj, dsimp only, + rw [sum_single_index, map_mul f, pow_add], + { simp only [mul_assoc, mul_left_comm] }, + { rw [map_zero f, zero_mul] } }, + { intro, rw [map_zero f, zero_mul] }, + { intros, rw [map_add f, add_mul] } }, + { intro, rw [map_zero f, zero_mul] }, + { intros, rw [map_add f, add_mul] } +end + +instance eval₂.is_semiring_hom : is_semiring_hom (eval₂ f x) := +⟨eval₂_zero _ _, eval₂_one _ _, λ _ _, eval₂_add _ _, λ _ _, eval₂_mul _ _⟩ + +/-- `eval₂` as a `ring_hom` -/ +def eval₂_ring_hom (f : R →+* S) (x) : polynomial R →+* S := +ring_hom.of (eval₂ f x) + +@[simp] lemma coe_eval₂_ring_hom (f : R →+* S) (x) : ⇑(eval₂_ring_hom f x) = eval₂ f x := rfl + +lemma eval₂_pow (n : ℕ) : (p ^ n).eval₂ f x = p.eval₂ f x ^ n := map_pow _ _ _ + +end eval₂ + +end semiring + +section ring +variables [ring R] + +instance : ring (polynomial R) := add_monoid_algebra.ring +end ring + +section comm_semiring +variables [comm_semiring R] {p q r : polynomial R} + +local attribute [instance] coeff_coe_to_fun + +instance : comm_semiring (polynomial R) := add_monoid_algebra.comm_semiring +instance : algebra R (polynomial R) := add_monoid_algebra.algebra + +section eval +variable {x : R} + +@[simp] lemma eval_mul : (p * q).eval x = p.eval x * q.eval x := eval₂_mul _ _ + +instance eval.is_semiring_hom : is_semiring_hom (eval x) := eval₂.is_semiring_hom _ _ + +@[simp] lemma eval_pow (n : ℕ) : (p ^ n).eval x = p.eval x ^ n := eval₂_pow _ _ _ + +lemma eval₂_hom [comm_semiring S] (f : R → S) [is_semiring_hom f] (x : R) : + p.eval₂ f (f x) = f (p.eval x) := +polynomial.induction_on p + (by simp) + (by simp [is_semiring_hom.map_add f] {contextual := tt}) + (by simp [is_semiring_hom.map_mul f, eval_pow, + is_semiring_hom.map_pow f, pow_succ', (mul_assoc _ _ _).symm] {contextual := tt}) + +lemma root_mul_left_of_is_root (p : polynomial R) {q : polynomial R} : + is_root q a → is_root (p * q) a := +λ H, by rw [is_root, eval_mul, is_root.def.1 H, mul_zero] + +lemma root_mul_right_of_is_root {p : polynomial R} (q : polynomial R) : + is_root p a → is_root (p * q) a := +λ H, by rw [is_root, eval_mul, is_root.def.1 H, zero_mul] + +end eval + +section comp + +lemma eval₂_comp [comm_semiring S] (f : R → S) [is_semiring_hom f] {x : S} : + (p.comp q).eval₂ f x = p.eval₂ f (q.eval₂ f x) := +show (p.sum (λ e a, C a * q ^ e)).eval₂ f x = p.eval₂ f (eval₂ f x q), +by simp only [eval₂_mul, eval₂_C, eval₂_pow, eval₂_sum]; refl + +lemma eval_comp : (p.comp q).eval a = p.eval (q.eval a) := eval₂_comp _ + instance : is_semiring_hom (λ q : polynomial R, q.comp p) := by unfold comp; apply_instance -@[simp] lemma add_comp : (p + q).comp r = p.comp r + q.comp r := eval₂_add _ _ @[simp] lemma mul_comp : (p * q).comp r = p.comp r * q.comp r := eval₂_mul _ _ end comp @@ -558,12 +611,6 @@ lemma degree_ne_of_nat_degree_ne {n : ℕ} : (λ _ h, option.no_confusion h) (λ n' h, mt option.some_inj.mp h) -end semiring - -section comm_semiring - -variables [comm_semiring R] {p q : polynomial R} - @[simp] lemma degree_C (ha : a ≠ 0) : degree (C a) = (0 : with_bot ℕ) := show sup (ite (a = 0) ∅ {0}) some = 0, by rw if_neg ha; refl @@ -585,7 +632,7 @@ end @[simp] lemma nat_degree_one : nat_degree (1 : polynomial R) = 0 := nat_degree_C 1 @[simp] lemma nat_degree_nat_cast (n : ℕ) : nat_degree (n : polynomial R) = 0 := -by simp [nat_cast_eq_C] +by simp only [←C_eq_nat_cast, nat_degree_C] @[simp] lemma degree_monomial (n : ℕ) (ha : a ≠ 0) : degree (C a * X ^ n) = n := by rw [← single_eq_C_mul_X, degree, support_single_ne_zero ha]; refl @@ -640,8 +687,14 @@ lemma coeff_ne_zero_of_eq_degree {p : polynomial R} {n : ℕ} (hn : degree p = n coeff p n ≠ 0 := λ h, mem_support_iff.mp (mem_of_max hn) h +end semiring + +section semiring + +variables [semiring R] {p q : polynomial R} + section map -variables [comm_semiring S] +variables [semiring S] variables (f : R →+* S) /-- `map f p` maps a polynomial `p` across a ring hom `f` -/ @@ -660,12 +713,6 @@ is_semiring_hom.comp _ _ @[simp] lemma map_one : (1 : polynomial R).map f = 1 := eval₂_one _ _ -@[simp] lemma map_mul : (p * q).map f = p.map f * q.map f := eval₂_mul _ _ - -instance map.is_semiring_hom : is_semiring_hom (map f) := eval₂.is_semiring_hom _ _ - -@[simp] lemma map_pow (n : ℕ) : (p ^ n).map f = p.map f ^ n := eval₂_pow _ _ _ - lemma coeff_map (n : ℕ) : coeff (p.map f) n = f (coeff p n) := begin rw [map, eval₂, coeff_sum], @@ -676,53 +723,15 @@ begin split_ifs; simp [is_semiring_hom.map_zero f], end -lemma map_map [comm_semiring T] (g : S →+* T) +lemma map_map [semiring T] (g : S →+* T) (p : polynomial R) : (p.map f).map g = p.map (g.comp f) := ext (by simp [coeff_map]) -lemma eval₂_map [comm_semiring T] (g : S → T) [is_semiring_hom g] (x : T) : - (p.map f).eval₂ g x = p.eval₂ (λ y, g (f y)) x := -polynomial.induction_on p - (by simp) - (by simp [is_semiring_hom.map_add f] {contextual := tt}) - (by simp [is_semiring_hom.map_mul f, - is_semiring_hom.map_pow f, pow_succ', (mul_assoc _ _ _).symm] {contextual := tt}) - -lemma eval_map (x : S) : (p.map f).eval x = p.eval₂ f x := eval₂_map _ _ _ - @[simp] lemma map_id : p.map (ring_hom.id _) = p := by simp [polynomial.ext_iff, coeff_map] -lemma mem_map_range {p : polynomial S} : - p ∈ set.range (map f) ↔ ∀ n, p.coeff n ∈ (set.range f) := -begin - split, - { rintro ⟨p, rfl⟩ n, rw coeff_map, exact set.mem_range_self _ }, - { intro h, rw p.as_sum, - apply is_add_submonoid.finset_sum_mem, - intros i hi, - rcases h i with ⟨c, hc⟩, - use [C c * X^i], - rw [map_mul, map_C, hc, map_pow, map_X] } -end - end map -section -variables [comm_semiring S] [comm_semiring T] -variables (f : R →+* S) (g : S →+* T) (p) - -lemma hom_eval₂ (x : S) : g (p.eval₂ f x) = p.eval₂ (g ∘ f) (g x) := -begin - apply polynomial.induction_on p; clear p, - { intros a, rw [eval₂_C, eval₂_C] }, - { intros p q hp hq, simp only [hp, hq, eval₂_add, is_semiring_hom.map_add g] }, - { intros n a ih, - replace ih := congr_arg (λ y, y * g x) ih, - simpa [pow_succ', is_semiring_hom.map_mul g, (mul_assoc _ _ _).symm, - eval₂_C, eval₂_mul, eval₂_X] using ih } -end - -end +section degree lemma coeff_nat_degree_eq_zero_of_degree_lt (h : degree p < degree q) : coeff p (nat_degree q) = 0 := @@ -853,7 +862,7 @@ lemma monic.ne_zero_of_zero_ne_one (h : (0:R) ≠ 1) {p : polynomial R} (hp : p. p ≠ 0 := by { contrapose! h, rwa [h] at hp } -lemma monic.ne_zero {R : Type*} [comm_semiring R] [nonzero R] {p : polynomial R} (hp : p.monic) : +lemma monic.ne_zero {R : Type*} [semiring R] [nonzero R] {p : polynomial R} (hp : p.monic) : p ≠ 0 := hp.ne_zero_of_zero_ne_one zero_ne_one @@ -988,7 +997,7 @@ else with_bot.coe_le_coe.1 $ (le_nat_degree_of_ne_zero (finsupp.mem_support_iff.1 hn)) (nat.zero_le _)) -lemma degree_map_le [comm_semiring S] (f : R →+* S) : +lemma degree_map_le [semiring S] (f : R →+* S) : degree (p.map f) ≤ degree p := if h : p.map f = 0 then by simp [h] else begin @@ -1004,7 +1013,7 @@ by rw [monic.def, leading_coeff_zero] at h; exact ⟨λ p q, by rw [← mul_one p, ← mul_one q, ← C_1, ← h, C_0, mul_zero, mul_zero], λ a b, by rw [← mul_one a, ← mul_one b, ← h, mul_zero, mul_zero]⟩ -lemma degree_map_eq_of_leading_coeff_ne_zero [comm_semiring S] (f : R →+* S) +lemma degree_map_eq_of_leading_coeff_ne_zero [semiring S] (f : R →+* S) (hf : f (leading_coeff p) ≠ 0) : degree (p.map f) = degree p := le_antisymm (degree_map_le f) $ have hp0 : p ≠ 0, from λ hp0, by simpa [hp0, is_semiring_hom.map_zero f] using hf, @@ -1014,7 +1023,7 @@ le_antisymm (degree_map_le f) $ rw [coeff_map], exact hf end -lemma monic_map [comm_semiring S] (f : R →+* S) (hp : monic p) : monic (p.map f) := +lemma monic_map [semiring S] (f : R →+* S) (hp : monic p) : monic (p.map f) := if h : (0 : S) = 1 then by haveI := subsingleton_of_zero_eq_one S h; exact subsingleton.elim _ _ @@ -1025,13 +1034,119 @@ by erw [monic, leading_coeff, nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero f this), coeff_map, ← leading_coeff, show _ = _, from hp, is_semiring_hom.map_one f] -lemma zero_le_degree_iff {p : polynomial R} : 0 ≤ degree p ↔ p ≠ 0 := -by rw [ne.def, ← degree_eq_bot]; - cases degree p; exact dec_trivial +lemma zero_le_degree_iff {p : polynomial R} : 0 ≤ degree p ↔ p ≠ 0 := +by rw [ne.def, ← degree_eq_bot]; + cases degree p; exact dec_trivial + +@[simp] lemma coeff_mul_X_zero (p : polynomial R) : coeff (p * X) 0 = 0 := +by rw [coeff_mul, nat.antidiagonal_zero]; +simp only [polynomial.coeff_X_zero, finset.sum_singleton, mul_zero] + +lemma degree_nonneg_iff_ne_zero : 0 ≤ degree p ↔ p ≠ 0 := +⟨λ h0p hp0, absurd h0p (by rw [hp0, degree_zero]; exact dec_trivial), + λ hp0, le_of_not_gt (λ h, by simp [gt, degree_eq_bot, *] at *)⟩ + +lemma nat_degree_eq_zero_iff_degree_le_zero : p.nat_degree = 0 ↔ p.degree ≤ 0 := +if hp0 : p = 0 then by simp [hp0] +else by rw [degree_eq_nat_degree hp0, ← with_bot.coe_zero, with_bot.coe_le_coe, + nat.le_zero_iff] + +end degree + +section map +variables [semiring S] +variables (f : R →+* S) + +open is_semiring_hom + +-- If the rings were commutative, we could prove this just using `eval₂_mul`. +-- TODO this proof is just a hack job on the proof of `eval₂_mul`, +-- using that `X` is central. It should probably be golfed! +@[simp] lemma map_mul : (p * q).map f = p.map f * q.map f := +begin + dunfold map, + dunfold eval₂, + rw [mul_def, finsupp.sum_mul _ p], simp only [finsupp.mul_sum _ q], rw [sum_sum_index], + { apply sum_congr rfl, assume i hi, dsimp only, rw [sum_sum_index], + { apply sum_congr rfl, assume j hj, dsimp only, + rw [sum_single_index, map_mul (C ∘ f), pow_add], + { simp [←mul_assoc], conv_lhs { rw ←@X_pow_mul_assoc _ _ _ _ i }, }, + { simp, } }, + { intro, simp, }, + { intros, simp [add_mul], } }, + { intro, simp, }, + { intros, simp [add_mul], } +end + +instance map.is_semiring_hom : is_semiring_hom (map f) := +{ map_zero := eval₂_zero _ _, + map_one := eval₂_one _ _, + map_add := λ _ _, eval₂_add _ _, + map_mul := λ _ _, map_mul f, } + +@[simp] lemma map_pow (n : ℕ) : (p ^ n).map f = p.map f ^ n := is_semiring_hom.map_pow (map f) _ _ + +lemma mem_map_range {p : polynomial S} : + p ∈ set.range (map f) ↔ ∀ n, p.coeff n ∈ (set.range f) := +begin + split, + { rintro ⟨p, rfl⟩ n, rw coeff_map, exact set.mem_range_self _ }, + { intro h, rw p.as_sum, + apply is_add_submonoid.finset_sum_mem, + intros i hi, + rcases h i with ⟨c, hc⟩, + use [C c * X^i], + rw [map_mul, map_C, hc, map_pow, map_X] } +end + +-- This lemma requires commutativity just in `T`. +-- Really, it just requires that `x` is central. +lemma eval₂_map [comm_semiring T] (g : S → T) [is_semiring_hom g] (x : T) : + (p.map f).eval₂ g x = p.eval₂ (λ y, g (f y)) x := +polynomial.induction_on p + (by simp) + (by simp [is_semiring_hom.map_add f] {contextual := tt}) + (by simp [is_semiring_hom.map_mul f, + is_semiring_hom.map_pow f, pow_succ', (mul_assoc _ _ _).symm] {contextual := tt}) + +lemma eval_map (x : S) : (p.map f).eval x = p.eval₂ f x := +begin + convert finsupp.sum_map_range_index _, + work_on_goal 1 { exact ring_hom.map_zero f, }, + work_on_goal 1 { intro a, simp only [id.def, zero_mul], }, + { change map f p = map_range f _ p, + ext, + rw map_range_apply, + exact coeff_map f a, }, +end + +end map + +section hom_eval₂ +-- Here we need commutativity in both `S` and `T`. +variables [comm_semiring S] [comm_semiring T] +variables (f : R →+* S) (g : S →+* T) (p) + +lemma hom_eval₂ (x : S) : g (p.eval₂ f x) = p.eval₂ (g ∘ f) (g x) := +begin + apply polynomial.induction_on p; clear p, + { intros a, rw [eval₂_C, eval₂_C] }, + { intros p q hp hq, simp only [hp, hq, eval₂_add, is_semiring_hom.map_add g] }, + { intros n a ih, + replace ih := congr_arg (λ y, y * g x) ih, + simpa [pow_succ', is_semiring_hom.map_mul g, (mul_assoc _ _ _).symm, + eval₂_C, eval₂_mul, eval₂_X] using ih } +end + +end hom_eval₂ + +end semiring + +section comm_semiring -@[simp] lemma coeff_mul_X_zero (p : polynomial R) : coeff (p * X) 0 = 0 := -by rw [coeff_mul, nat.antidiagonal_zero]; -simp only [polynomial.coeff_X_zero, finset.sum_singleton, mul_zero] +variables [comm_semiring R] {p q : polynomial R} + +section is_unit lemma is_unit_C {x : R} : is_unit (C x) ↔ is_unit x := begin @@ -1045,15 +1160,6 @@ begin exact ⟨C y, by rw [← C_mul, ← hy, C_1]⟩ } end -lemma degree_nonneg_iff_ne_zero : 0 ≤ degree p ↔ p ≠ 0 := -⟨λ h0p hp0, absurd h0p (by rw [hp0, degree_zero]; exact dec_trivial), - λ hp0, le_of_not_gt (λ h, by simp [gt, degree_eq_bot, *] at *)⟩ - -lemma nat_degree_eq_zero_iff_degree_le_zero : p.nat_degree = 0 ↔ p.degree ≤ 0 := -if hp0 : p = 0 then by simp [hp0] -else by rw [degree_eq_nat_degree hp0, ← with_bot.coe_zero, with_bot.coe_le_coe, - nat.le_zero_iff] - lemma eq_one_of_is_unit_of_monic (hm : monic p) (hpu : is_unit p) : p = 1 := have degree p ≤ 0, from calc degree p ≤ degree (1 : polynomial R) : @@ -1073,14 +1179,16 @@ have degree p ≤ 0, by rw [eq_C_of_degree_le_zero this, ← nat_degree_eq_zero_iff_degree_le_zero.2 this, ← leading_coeff, hm.leading_coeff, C_1] +end is_unit + end comm_semiring -instance subsingleton [subsingleton R] [comm_semiring R] : subsingleton (polynomial R) := +instance subsingleton [subsingleton R] [semiring R] : subsingleton (polynomial R) := ⟨λ _ _, ext (λ _, subsingleton.elim _ _)⟩ -section comm_semiring +section semiring -variables [comm_semiring R] {p q r : polynomial R} +variables [semiring R] {p q r : polynomial R} lemma ne_zero_of_monic_of_zero_ne_one (hp : monic p) (h : (0 : R) ≠ 1) : p ≠ 0 := mt (congr_arg leading_coeff) $ by rw [monic.def.1 hp, leading_coeff_zero]; cc @@ -1114,7 +1222,7 @@ by simpa only [C_1, one_mul, pow_one] using degree_C_mul_X_pow_le (1:R) 1 section injective open function -variables [comm_semiring S] {f : R →+* S} (hf : function.injective f) +variables [semiring S] {f : R →+* S} (hf : function.injective f) include hf lemma degree_map_eq_of_injective (p : polynomial R) : degree (p.map f) = degree p := @@ -1206,6 +1314,12 @@ lemma monic_pow (hp : monic p) : ∀ (n : ℕ), monic (p ^ n) | 0 := monic_one | (n+1) := monic_mul hp (monic_pow n) +end semiring + +section comm_semiring + +variables [comm_semiring R] {p q : polynomial R} + lemma multiplicity_finite_of_degree_pos_of_monic (hp : (0 : with_bot ℕ) < degree p) (hmp : monic p) (hq : q ≠ 0) : multiplicity.finite p q := have zn0 : (0 : R) ≠ 1, from λ h, by haveI := subsingleton_of_zero_eq_one _ h; @@ -1235,8 +1349,8 @@ have zn0 : (0 : R) ≠ 1, from λ h, by haveI := subsingleton_of_zero_eq_one _ h end comm_semiring -section nonzero_comm_semiring -variables [comm_semiring R] [nonzero R] {p q : polynomial R} +section nonzero_semiring +variables [semiring R] [nonzero R] {p q : polynomial R} instance : nonzero (polynomial R) := { zero_ne_one := λ (h : (0 : polynomial R) = 1), zero_ne_one $ @@ -1271,10 +1385,10 @@ by simpa only [monic, leading_coeff_zero] using (zero_ne_one : (0 : R) ≠ 1) lemma ne_zero_of_monic (h : monic p) : p ≠ 0 := λ h₁, @not_monic_zero R _ _ (h₁ ▸ h) -end nonzero_comm_semiring +end nonzero_semiring -section comm_semiring -variables [comm_semiring R] {p q : polynomial R} +section semiring +variables [semiring R] {p q : polynomial R} /-- `dix_X p` return a polynomial `q` such that `q * X + C (p.coeff 0) = p`. It can be used in a semiring where the usual division algorithm is not possible -/ @@ -1392,11 +1506,10 @@ rec_on_horner p by simpa [h, nat.not_lt_zero] using h0')) h0 -end comm_semiring +end semiring -section comm_ring -variables [comm_ring R] {p q : polynomial R} -instance : comm_ring (polynomial R) := add_monoid_algebra.comm_ring +section semiring +variables [semiring R] variable (R) def lcoeff (n : ℕ) : polynomial R →ₗ[R] R := @@ -1407,23 +1520,65 @@ variable {R} @[simp] lemma lcoeff_apply (n : ℕ) (f : polynomial R) : lcoeff R n f = coeff f n := rfl -instance : is_ring_hom (C : R → polynomial R) := (C : R →ₐ[R] polynomial R).to_ring_hom.is_ring_hom +lemma degree_pos_of_root {p : polynomial R} (hp : p ≠ 0) (h : is_root p a) : 0 < degree p := +lt_of_not_ge $ λ hlt, begin + have := eq_C_of_degree_le_zero hlt, + rw [is_root, this, eval_C] at h, + exact hp (finsupp.ext (λ n, show coeff p n = 0, from + nat.cases_on n h (λ _, coeff_eq_zero_of_degree_lt (lt_of_le_of_lt hlt + (with_bot.coe_lt_coe.2 (nat.succ_pos _)))))), +end -lemma int_cast_eq_C (n : ℤ) : (n : polynomial R) = C ↑n := -((C : R →ₐ[R] _).to_ring_hom.map_int_cast n).symm +lemma eq_C_of_nat_degree_le_zero {p : polynomial R} (h : nat_degree p ≤ 0) : p = C (coeff p 0) := +begin + refine polynomial.ext (λ n, _), + cases n, + { simp }, + { have : nat_degree p < nat.succ n := lt_of_le_of_lt h (nat.succ_pos _), + rw [coeff_C, if_neg (nat.succ_ne_zero _), coeff_eq_zero_of_nat_degree_lt this] } +end -lemma C_neg : C (-a) = -C a := alg_hom.map_neg C a +lemma nat_degree_pos_iff_degree_pos {p : polynomial R} : + 0 < nat_degree p ↔ 0 < degree p := +⟨ λ h, ((degree_eq_iff_nat_degree_eq_of_pos h).mpr rfl).symm ▸ (with_bot.some_lt_some.mpr h), + by { unfold nat_degree, + cases degree p, + { rintros ⟨_, ⟨⟩, _⟩ }, + { exact with_bot.some_lt_some.mp } } ⟩ -lemma C_sub : C (a - b) = C a - C b := alg_hom.map_sub C a b +variables [semiring S] -instance eval₂.is_ring_hom {S} [comm_ring S] - (f : R → S) [is_ring_hom f] {x : S} : is_ring_hom (eval₂ f x) := -by apply is_ring_hom.of_semiring +lemma nat_degree_pos_of_eval₂_root {p : polynomial R} (hp : p ≠ 0) (f : R →+* S) + {z : S} (hz : eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) : + 0 < nat_degree p := +lt_of_not_ge $ λ hlt, begin + rw [eq_C_of_nat_degree_le_zero hlt, eval₂_C] at hz, + refine hp (finsupp.ext (λ n, _)), + cases n, + { exact inj _ hz }, + { exact coeff_eq_zero_of_nat_degree_lt (lt_of_le_of_lt hlt (nat.succ_pos _)) } +end -instance eval.is_ring_hom {x : R} : is_ring_hom (eval x) := eval₂.is_ring_hom _ +lemma degree_pos_of_eval₂_root {p : polynomial R} (hp : p ≠ 0) (f : R →+* S) + {z : S} (hz : eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) : + 0 < degree p := +nat_degree_pos_iff_degree_pos.mp (nat_degree_pos_of_eval₂_root hp f hz inj) + +end semiring + +section ring +variables [ring R] {p q : polynomial R} + +@[simp] +lemma C_eq_int_cast (n : ℤ) : C ↑n = (n : polynomial R) := +(C : R →+* _).map_int_cast n + +lemma C_neg : C (-a) = -C a := ring_hom.map_neg C a -instance map.is_ring_hom {S} [comm_ring S] (f : R →+* S) : is_ring_hom (map f) := -eval₂.is_ring_hom (C ∘ f) +lemma C_sub : C (a - b) = C a - C b := ring_hom.map_sub C a b + +instance map.is_ring_hom {S} [ring S] (f : R →+* S) : is_ring_hom (map f) := +by apply is_ring_hom.of_semiring @[simp] lemma map_sub {S} [comm_ring S] (f : R →+* S) : (p - q).map f = p.map f - q.map f := @@ -1443,26 +1598,46 @@ degree_neg q ▸ degree_add_le p (-q) by simp [nat_degree] @[simp] lemma nat_degree_int_cast (n : ℤ) : nat_degree (n : polynomial R) = 0 := -by simp [int_cast_eq_C] +by simp only [←C_eq_int_cast, nat_degree_C] @[simp] lemma coeff_neg (p : polynomial R) (n : ℕ) : coeff (-p) n = -coeff p n := rfl @[simp] lemma coeff_sub (p q : polynomial R) (n : ℕ) : coeff (p - q) n = coeff p n - coeff q n := rfl -@[simp] lemma eval₂_neg {S} [comm_ring S] (f : R → S) [is_ring_hom f] {x : S} : +@[simp] lemma eval_int_cast {n : ℤ} {x : R} : (n : polynomial R).eval x = n := +by simp only [←C_eq_int_cast, eval_C] + +@[simp] lemma eval₂_neg {S} [ring S] (f : R → S) [is_ring_hom f] {x : S} : (-p).eval₂ f x = -p.eval₂ f x := -is_ring_hom.map_neg _ +by rw [eq_neg_iff_add_eq_zero, ←eval₂_add, add_left_neg, eval₂_zero] -@[simp] lemma eval₂_sub {S} [comm_ring S] (f : R → S) [is_ring_hom f] {x : S} : +@[simp] lemma eval₂_sub {S} [ring S] (f : R → S) [is_ring_hom f] {x : S} : (p - q).eval₂ f x = p.eval₂ f x - q.eval₂ f x := -is_ring_hom.map_sub _ +by rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg] @[simp] lemma eval_neg (p : polynomial R) (x : R) : (-p).eval x = -p.eval x := -is_ring_hom.map_neg _ +eval₂_neg _ @[simp] lemma eval_sub (p q : polynomial R) (x : R) : (p - q).eval x = p.eval x - q.eval x := -is_ring_hom.map_sub _ +eval₂_sub _ + +end ring + +section comm_ring +variables [comm_ring R] {p q : polynomial R} +instance : comm_ring (polynomial R) := add_monoid_algebra.comm_ring + +instance eval₂.is_ring_hom {S} [comm_ring S] + (f : R → S) [is_ring_hom f] {x : S} : is_ring_hom (eval₂ f x) := +by apply is_ring_hom.of_semiring + +instance eval.is_ring_hom {x : R} : is_ring_hom (eval x) := eval₂.is_ring_hom _ + +end comm_ring + +section comm_semiring +variables [comm_semiring R] {p q : polynomial R} section aeval /-- `R[X]` is the generator of the category `R-Alg`. -/ @@ -1472,6 +1647,9 @@ instance polynomial (R : Type u) [comm_semiring R] : algebra R (polynomial R) := .. polynomial.semimodule, .. ring_hom.of polynomial.C } variables (R) (A) + +-- TODO this could be generalized: there's no need for `A` to be commutative, +-- we just need that `x` is central. variables [comm_ring A] [algebra R A] variables (x : A) @@ -1502,6 +1680,11 @@ end end aeval +end comm_semiring + +section ring +variables [ring R] {p q : polynomial R} + lemma degree_sub_lt (hd : degree p = degree q) (hp0 : p ≠ 0) (hlc : leading_coeff p = leading_coeff q) : degree (p - q) < degree p := @@ -1595,31 +1778,6 @@ else end using_well_founded {dec_tac := tactic.assumption} -lemma mod_by_monic_eq_sub_mul_div : ∀ (p : polynomial R) {q : polynomial R} (hq : monic q), - p %ₘ q = p - q * (p /ₘ q) -| p := λ q hq, - if h : degree q ≤ degree p ∧ p ≠ 0 then - have wf : _ := div_wf_lemma h hq, - have ih : _ := mod_by_monic_eq_sub_mul_div - (p - C (leading_coeff p) * X ^ (nat_degree p - nat_degree q) * q) hq, - begin - unfold mod_by_monic div_by_monic div_mod_by_monic_aux, - rw [dif_pos hq, if_pos h], - rw [mod_by_monic, dif_pos hq] at ih, - refine ih.trans _, - unfold div_by_monic, - rw [dif_pos hq, dif_pos hq, if_pos h, mul_add, sub_add_eq_sub_sub, mul_comm] - end - else - begin - unfold mod_by_monic div_by_monic div_mod_by_monic_aux, - rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero] - end -using_well_founded {dec_tac := tactic.assumption} - -lemma mod_by_monic_add_div (p : polynomial R) {q : polynomial R} (hq : monic q) : - p %ₘ q + q * (p /ₘ q) = p := eq_sub_iff_add_eq.1 (mod_by_monic_eq_sub_mul_div p hq) - @[simp] lemma zero_mod_by_monic (p : polynomial R) : 0 %ₘ p = 0 := begin unfold mod_by_monic div_mod_by_monic_aux, @@ -1653,6 +1811,50 @@ lemma mod_by_monic_eq_self_iff (hq : monic q) (hq0 : q ≠ 0) : p %ₘ q = p ↔ λ h, have ¬ degree q ≤ degree p := not_le_of_gt h, by unfold mod_by_monic div_mod_by_monic_aux; rw [dif_pos hq, if_neg (mt and.left this)]⟩ +theorem monic_X_sub_C (x : R) : monic (X - C x) := +by simpa only [C_neg] using monic_X_add_C (-x) + +theorem monic_X_pow_sub {n : ℕ} (H : degree p ≤ n) : monic (X ^ (n+1) - p) := +monic_X_pow_add ((degree_neg p).symm ▸ H) + +theorem degree_mod_by_monic_le (p : polynomial R) {q : polynomial R} + (hq : monic q) : degree (p %ₘ q) ≤ degree q := +decidable.by_cases + (assume H : q = 0, by rw [monic, H, leading_coeff_zero] at hq; + have : (0:polynomial R) = 1 := (by rw [← C_0, ← C_1, hq]); + rw [eq_zero_of_zero_eq_one _ this (p %ₘ q), eq_zero_of_zero_eq_one _ this q]; exact le_refl _) + (assume H : q ≠ 0, le_of_lt $ degree_mod_by_monic_lt _ hq H) + +end ring + +section comm_ring +variables [comm_ring R] {p q : polynomial R} + +lemma mod_by_monic_eq_sub_mul_div : ∀ (p : polynomial R) {q : polynomial R} (hq : monic q), + p %ₘ q = p - q * (p /ₘ q) +| p := λ q hq, + if h : degree q ≤ degree p ∧ p ≠ 0 then + have wf : _ := div_wf_lemma h hq, + have ih : _ := mod_by_monic_eq_sub_mul_div + (p - C (leading_coeff p) * X ^ (nat_degree p - nat_degree q) * q) hq, + begin + unfold mod_by_monic div_by_monic div_mod_by_monic_aux, + rw [dif_pos hq, if_pos h], + rw [mod_by_monic, dif_pos hq] at ih, + refine ih.trans _, + unfold div_by_monic, + rw [dif_pos hq, dif_pos hq, if_pos h, mul_add, sub_add_eq_sub_sub, mul_comm] + end + else + begin + unfold mod_by_monic div_by_monic div_mod_by_monic_aux, + rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero] + end +using_well_founded {dec_tac := tactic.assumption} + +lemma mod_by_monic_add_div (p : polynomial R) {q : polynomial R} (hq : monic q) : + p %ₘ q + q * (p /ₘ q) = p := eq_sub_iff_add_eq.1 (mod_by_monic_eq_sub_mul_div p hq) + lemma div_by_monic_eq_zero_iff (hq : monic q) (hq0 : q ≠ 0) : p /ₘ q = 0 ↔ degree p < degree q := ⟨λ h, by have := mod_by_monic_add_div p hq; rwa [h, mul_zero, add_zero, mod_by_monic_eq_self_iff hq hq0] at this, @@ -1785,50 +1987,8 @@ lemma dvd_iff_mod_by_monic_eq_zero (hq : monic q) : p %ₘ q = 0 ↔ q ∣ p := @[simp] lemma div_by_monic_one (p : polynomial R) : p /ₘ 1 = p := by conv_rhs { rw [← mod_by_monic_add_div p monic_one] }; simp -lemma degree_pos_of_root (hp : p ≠ 0) (h : is_root p a) : 0 < degree p := -lt_of_not_ge $ λ hlt, begin - have := eq_C_of_degree_le_zero hlt, - rw [is_root, this, eval_C] at h, - exact hp (finsupp.ext (λ n, show coeff p n = 0, from - nat.cases_on n h (λ _, coeff_eq_zero_of_degree_lt (lt_of_le_of_lt hlt - (with_bot.coe_lt_coe.2 (nat.succ_pos _)))))), -end - -lemma eq_C_of_nat_degree_le_zero {p : polynomial R} (h : nat_degree p ≤ 0) : p = C (coeff p 0) := -begin - refine polynomial.ext (λ n, _), - cases n, - { simp }, - { have : nat_degree p < nat.succ n := lt_of_le_of_lt h (nat.succ_pos _), - rw [coeff_C, if_neg (nat.succ_ne_zero _), coeff_eq_zero_of_nat_degree_lt this] } -end - variables [comm_ring S] -lemma nat_degree_pos_iff_degree_pos {p : polynomial R} : - 0 < nat_degree p ↔ 0 < degree p := -⟨ λ h, ((degree_eq_iff_nat_degree_eq_of_pos h).mpr rfl).symm ▸ (with_bot.some_lt_some.mpr h), - by { unfold nat_degree, - cases degree p, - { rintros ⟨_, ⟨⟩, _⟩ }, - { exact with_bot.some_lt_some.mp } } ⟩ - -lemma nat_degree_pos_of_eval₂_root {p : polynomial R} (hp : p ≠ 0) (f : R →+* S) - {z : S} (hz : eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) : - 0 < nat_degree p := -lt_of_not_ge $ λ hlt, begin - rw [eq_C_of_nat_degree_le_zero hlt, eval₂_C] at hz, - refine hp (finsupp.ext (λ n, _)), - cases n, - { exact inj _ hz }, - { exact coeff_eq_zero_of_nat_degree_lt (lt_of_le_of_lt hlt (nat.succ_pos _)) } -end - -lemma degree_pos_of_eval₂_root {p : polynomial R} (hp : p ≠ 0) (f : R →+* S) - {z : S} (hz : eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) : - 0 < degree p := -nat_degree_pos_iff_degree_pos.mp (nat_degree_pos_of_eval₂_root hp f hz inj) - lemma nat_degree_pos_of_aeval_root [algebra R S] {p : polynomial R} (hp : p ≠ 0) {z : S} (hz : aeval R S z p = 0) (inj : ∀ (x : R), algebra_map R S x = 0 → x = 0) : 0 < p.nat_degree := @@ -1839,27 +1999,13 @@ 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) -theorem monic_X_sub_C (x : R) : monic (X - C x) := -by simpa only [C_neg] using monic_X_add_C (-x) - -theorem monic_X_pow_sub {n : ℕ} (H : degree p ≤ n) : monic (X ^ (n+1) - p) := -monic_X_pow_add ((degree_neg p).symm ▸ H) - -theorem degree_mod_by_monic_le (p : polynomial R) {q : polynomial R} - (hq : monic q) : degree (p %ₘ q) ≤ degree q := -decidable.by_cases - (assume H : q = 0, by rw [monic, H, leading_coeff_zero] at hq; - have : (0:polynomial R) = 1 := (by rw [← C_0, ← C_1, hq]); - rw [eq_zero_of_zero_eq_one _ this (p %ₘ q), eq_zero_of_zero_eq_one _ this q]; exact le_refl _) - (assume H : q ≠ 0, le_of_lt $ degree_mod_by_monic_lt _ hq H) - lemma root_X_sub_C : is_root (X - C a) b ↔ a = b := by rw [is_root.def, eval_sub, eval_X, eval_C, sub_eq_zero_iff_eq, eq_comm] end comm_ring -section nonzero_comm_ring -variables [comm_ring R] [nonzero R] {p q : polynomial R} +section nonzero_ring +variables [ring R] [nonzero R] {p q : polynomial R} @[simp] lemma degree_X_sub_C (a : R) : degree (X - C a) = 1 := begin @@ -1882,7 +2028,7 @@ lemma X_pow_sub_C_ne_zero {n : ℕ} (hn : 0 < n) (a : R) : mt degree_eq_bot.2 (show degree ((X : polynomial R) ^ n - C a) ≠ ⊥, by rw degree_X_pow_sub_C hn a; exact dec_trivial) -end nonzero_comm_ring +end nonzero_ring section comm_ring @@ -2484,7 +2630,7 @@ by rw [neg_mul_eq_neg_mul_symm, ← sub_eq_add_neg, ← mul_sub, sub_sub_sub_can end field section derivative -variables [comm_semiring R] +variables [semiring R] /-- `derivative p` is the formal derivative of the polynomial `p` -/ def derivative (p : polynomial R) : polynomial R := p.sum (λn a, C (a * n) * X^(n - 1)) @@ -2527,16 +2673,16 @@ by refine finsupp.sum_add_index _ _; intros; simp only [add_mul, zero_mul, C_0, C_add, C_mul] /-- The formal derivative of polynomials, as additive homomorphism. -/ -def derivative_hom (R : Type*) [comm_semiring R] : polynomial R →+ polynomial R := +def derivative_hom (R : Type*) [semiring R] : polynomial R →+ polynomial R := { to_fun := derivative, map_zero' := derivative_zero, map_add' := λ p q, derivative_add } -@[simp] lemma derivative_neg {R : Type*} [comm_ring R] (f : polynomial R) : +@[simp] lemma derivative_neg {R : Type*} [ring R] (f : polynomial R) : derivative (-f) = -derivative f := (derivative_hom R).map_neg f -@[simp] lemma derivative_sub {R : Type*} [comm_ring R] (f g : polynomial R) : +@[simp] lemma derivative_sub {R : Type*} [ring R] (f g : polynomial R) : derivative (f - g) = derivative f - derivative g := (derivative_hom R).map_sub f g @@ -2547,6 +2693,14 @@ instance : is_add_monoid_hom (derivative : polynomial R → polynomial R) := derivative (∑ b in s, f b) = ∑ b in s, derivative (f b) := (derivative_hom R).map_sum f s +@[simp] lemma derivative_smul (r : R) (p : polynomial R) : derivative (r • p) = r • derivative p := +by { ext, simp only [coeff_derivative, mul_assoc, coeff_smul], } + +end derivative + +section derivative +variables [comm_semiring R] + @[simp] lemma derivative_mul {f g : polynomial R} : derivative (f * g) = derivative f * g + f * derivative g := calc derivative (f * g) = f.sum (λn a, g.sum (λm b, C ((a * b) * (n + m : ℕ)) * X^((n + m) - 1))) : @@ -2578,9 +2732,6 @@ lemma derivative_eval (p : polynomial R) (x : R) : p.derivative.eval x = p.sum (λ n a, (a * n)*x^(n-1)) := by simp [derivative, eval_sum, eval_pow] -@[simp] lemma derivative_smul (r : R) (p : polynomial R) : derivative (r • p) = r • derivative p := -by { ext, simp only [coeff_derivative, mul_assoc, coeff_smul], } - /-- The formal derivative of polynomials, as linear homomorphism. -/ def derivative_lhom (R : Type*) [comm_ring R] : polynomial R →ₗ[R] polynomial R := { to_fun := derivative, @@ -2726,8 +2877,8 @@ end identities section integral_normalization -section comm_semiring -variables [comm_semiring R] +section semiring +variables [semiring R] /-- If `f : polynomial R` is a nonzero polynomial with root `z`, `integral_normalization f` is a monic polynomial with root `leading_coeff f * z`. @@ -2775,7 +2926,7 @@ begin { exact integral_normalization_coeff_nat_degree hf } end -end comm_semiring +end semiring variables [integral_domain R] diff --git a/src/ring_theory/free_comm_ring.lean b/src/ring_theory/free_comm_ring.lean index 8931c058d23bd..8736453e9db0c 100644 --- a/src/ring_theory/free_comm_ring.lean +++ b/src/ring_theory/free_comm_ring.lean @@ -183,7 +183,7 @@ assume hps : is_supported (of p) s, begin { rintros x y ⟨q, hq⟩ ⟨r, hr⟩, refine ⟨q+r, _⟩, rw [lift_add, hq, hr], norm_cast } }, specialize this (of p) hps, rw [lift_of] at this, split_ifs at this, { exact h }, exfalso, apply ne.symm int.zero_ne_one, - rcases this with ⟨w, H⟩, rw polynomial.int_cast_eq_C at H, + rcases this with ⟨w, H⟩, rw ←polynomial.C_eq_int_cast at H, have : polynomial.X.coeff 1 = (polynomial.C ↑w).coeff 1, by rw H, rwa [polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), polynomial.coeff_X, if_pos rfl] at this end diff --git a/src/ring_theory/localization.lean b/src/ring_theory/localization.lean index 5cb7df20ea5a8..5480860956559 100644 --- a/src/ring_theory/localization.lean +++ b/src/ring_theory/localization.lean @@ -708,7 +708,7 @@ variables {R' : Type*} [comm_ring R'] lemma integer_normalization_eval₂_eq_zero (g : f.codomain →+* R') (p : polynomial f.codomain) {x : R'} (hx : eval₂ g x p = 0) : eval₂ (g ∘ f.to_map) x (integer_normalization p) = 0 := let ⟨b, hb⟩ := integer_normalization_map_to_map p in -trans (eval₂_map f.to_map g x).symm (by rw [hb, eval₂_smul, hx, _root_.mul_zero]) +trans (eval₂_map f.to_map g x).symm (by rw [hb, eval₂_smul, hx, smul_zero]) lemma integer_normalization_aeval_eq_zero [algebra f.codomain R'] (p : polynomial f.codomain) {x : R'} (hx : aeval _ _ x p = 0) :