-
Notifications
You must be signed in to change notification settings - Fork 297
/
rational_root.lean
138 lines (114 loc) · 5.03 KB
/
rational_root.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
/-
Copyright (c) 2020 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen
-/
import ring_theory.integrally_closed
import ring_theory.localization.num_denom
import ring_theory.polynomial.scale_roots
/-!
# Rational root theorem and integral root theorem
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
This file contains the rational root theorem and integral root theorem.
The rational root theorem for a unique factorization domain `A`
with localization `S`, states that the roots of `p : A[X]` in `A`'s
field of fractions are of the form `x / y` with `x y : A`, `x ∣ p.coeff 0` and
`y ∣ p.leading_coeff`.
The corollary is the integral root theorem `is_integer_of_is_root_of_monic`:
if `p` is monic, its roots must be integers.
Finally, we use this to show unique factorization domains are integrally closed.
## References
* https://en.wikipedia.org/wiki/Rational_root_theorem
-/
open_locale polynomial
section scale_roots
variables {A K R S : Type*} [comm_ring A] [field K] [comm_ring R] [comm_ring S]
variables {M : submonoid A} [algebra A S] [is_localization M S] [algebra A K] [is_fraction_ring A K]
open finsupp is_fraction_ring is_localization polynomial
lemma scale_roots_aeval_eq_zero_of_aeval_mk'_eq_zero {p : A[X]} {r : A} {s : M}
(hr : aeval (mk' S r s) p = 0) :
aeval (algebra_map A S r) (scale_roots p s) = 0 :=
begin
convert scale_roots_eval₂_eq_zero (algebra_map A S) hr,
rw [aeval_def, mk'_spec' _ r s]
end
variables [is_domain A]
lemma num_is_root_scale_roots_of_aeval_eq_zero
[unique_factorization_monoid A] {p : A[X]} {x : K} (hr : aeval x p = 0) :
is_root (scale_roots p (denom A x)) (num A x) :=
begin
apply is_root_of_eval₂_map_eq_zero (is_fraction_ring.injective A K),
refine scale_roots_aeval_eq_zero_of_aeval_mk'_eq_zero _,
rw mk'_num_denom,
exact hr
end
end scale_roots
section rational_root_theorem
variables {A K : Type*} [comm_ring A] [is_domain A] [unique_factorization_monoid A] [field K]
variables [algebra A K] [is_fraction_ring A K]
open is_fraction_ring is_localization polynomial unique_factorization_monoid
/-- Rational root theorem part 1:
if `r : f.codomain` is a root of a polynomial over the ufd `A`,
then the numerator of `r` divides the constant coefficient -/
theorem num_dvd_of_is_root {p : A[X]} {r : K} (hr : aeval r p = 0) :
num A r ∣ p.coeff 0 :=
begin
suffices : num A r ∣ (scale_roots p (denom A r)).coeff 0,
{ simp only [coeff_scale_roots, tsub_zero] at this,
haveI := classical.prop_decidable,
by_cases hr : num A r = 0,
{ obtain ⟨u, hu⟩ := (is_unit_denom_of_num_eq_zero hr).pow p.nat_degree,
rw ←hu at this,
exact units.dvd_mul_right.mp this },
{ refine dvd_of_dvd_mul_left_of_no_prime_factors hr _ this,
intros q dvd_num dvd_denom_pow hq,
apply hq.not_unit,
exact num_denom_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow) } },
convert dvd_term_of_is_root_of_dvd_terms 0 (num_is_root_scale_roots_of_aeval_eq_zero hr) _,
{ rw [pow_zero, mul_one] },
intros j hj,
apply dvd_mul_of_dvd_right,
convert pow_dvd_pow (num A r) (nat.succ_le_of_lt (bot_lt_iff_ne_bot.mpr hj)),
exact (pow_one _).symm
end
/-- Rational root theorem part 2:
if `r : f.codomain` is a root of a polynomial over the ufd `A`,
then the denominator of `r` divides the leading coefficient -/
theorem denom_dvd_of_is_root {p : A[X]} {r : K} (hr : aeval r p = 0) :
(denom A r : A) ∣ p.leading_coeff :=
begin
suffices : (denom A r : A) ∣ p.leading_coeff * num A r ^ p.nat_degree,
{ refine dvd_of_dvd_mul_left_of_no_prime_factors
(mem_non_zero_divisors_iff_ne_zero.mp (denom A r).2) _ this,
intros q dvd_denom dvd_num_pow hq,
apply hq.not_unit,
exact num_denom_reduced A r (hq.dvd_of_dvd_pow dvd_num_pow) dvd_denom },
rw ←coeff_scale_roots_nat_degree,
apply dvd_term_of_is_root_of_dvd_terms _ (num_is_root_scale_roots_of_aeval_eq_zero hr),
intros j hj,
by_cases h : j < p.nat_degree,
{ rw coeff_scale_roots,
refine (dvd_mul_of_dvd_right _ _).mul_right _,
convert pow_dvd_pow _ (nat.succ_le_iff.mpr (lt_tsub_iff_left.mpr _)),
{ exact (pow_one _).symm },
simpa using h },
rw [←nat_degree_scale_roots p (denom A r)] at *,
rw [coeff_eq_zero_of_nat_degree_lt (lt_of_le_of_ne (le_of_not_gt h) hj.symm), zero_mul],
exact dvd_zero _
end
/-- Integral root theorem:
if `r : f.codomain` is a root of a monic polynomial over the ufd `A`,
then `r` is an integer -/
theorem is_integer_of_is_root_of_monic {p : A[X]} (hp : monic p) {r : K}
(hr : aeval r p = 0) : is_integer A r :=
is_integer_of_is_unit_denom (is_unit_of_dvd_one _ (hp ▸ denom_dvd_of_is_root hr))
namespace unique_factorization_monoid
lemma integer_of_integral {x : K} :
is_integral A x → is_integer A x :=
λ ⟨p, hp, hx⟩, is_integer_of_is_root_of_monic hp hx
@[priority 100] -- See library note [lower instance priority]
instance : is_integrally_closed A :=
⟨λ x, integer_of_integral⟩
end unique_factorization_monoid
end rational_root_theorem