Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 5bfbcca

Browse files
riccardobrascariccardobrasca
committed
chore(ring_theory.polynomial.cyclotomic): split file (#19077)
`ring_theory.polynomial.cyclotomic` is almost 1000 lines long and it can be nicely split. We also fix some docstring.
1 parent bc91ed7 commit 5bfbcca

8 files changed

Lines changed: 442 additions & 372 deletions

File tree

‎archive/100-theorems-list/37_solution_of_cubic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Jeoff Lee
55
-/
66
import tactic.linear_combination
77
import ring_theory.roots_of_unity
8-
import ring_theory.polynomial.cyclotomic.basic
8+
import ring_theory.polynomial.cyclotomic.roots
99

1010
/-!
1111
# The Solution of a Cubic

‎src/number_theory/cyclotomic/basic.lean‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Riccardo Brasca. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Riccardo Brasca
55
-/
6-
import ring_theory.polynomial.cyclotomic.basic
6+
import ring_theory.polynomial.cyclotomic.roots
77
import number_theory.number_field.basic
88
import field_theory.galois
99

@@ -374,7 +374,8 @@ begin
374374
map_cyclotomic, mem_roots (cyclotomic_ne_zero n B)] at hx,
375375
simp only [mem_singleton_iff, exists_eq_left, mem_set_of_eq],
376376
rw is_root_of_unity_iff n.pos,
377-
exact ⟨n, nat.mem_divisors_self n n.ne_zero, hx⟩ },
377+
exact ⟨n, nat.mem_divisors_self n n.ne_zero, hx⟩,
378+
all_goals { apply_instance } },
378379
{ simp only [mem_singleton_iff, exists_eq_left, mem_set_of_eq] at hx,
379380
obtain ⟨i, hin, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx n.pos,
380381
refine set_like.mem_coe.2 (subalgebra.pow_mem _ (subset_adjoin _) _),
@@ -393,7 +394,8 @@ begin
393394
rw is_root_of_unity_iff n.pos,
394395
refine ⟨n, nat.mem_divisors_self n n.ne_zero, _⟩,
395396
rwa [finset.mem_coe, multiset.mem_to_finset,
396-
map_cyclotomic, mem_roots $ cyclotomic_ne_zero n B] at hx },
397+
map_cyclotomic, mem_roots $ cyclotomic_ne_zero n B] at hx,
398+
all_goals { apply_instance } },
397399
{ simp only [mem_singleton_iff, exists_eq_left, mem_set_of_eq] at hx,
398400
simpa only [hx, multiset.mem_to_finset, finset.mem_coe, map_cyclotomic,
399401
mem_roots (cyclotomic_ne_zero n B)] using hζ.is_root_cyclotomic n.pos }

‎src/number_theory/cyclotomic/primitive_roots.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ import number_theory.cyclotomic.basic
1010
import ring_theory.adjoin.power_basis
1111
import ring_theory.polynomial.cyclotomic.eval
1212
import ring_theory.norm
13+
import ring_theory.polynomial.cyclotomic.expand
1314

1415
/-!
1516
# Primitive roots in cyclotomic fields

‎src/ring_theory/polynomial/cyclotomic/basic.lean‎

Lines changed: 4 additions & 366 deletions
Large diffs are not rendered by default.

‎src/ring_theory/polynomial/cyclotomic/eval.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Eric Rodriguez
55
-/
66

7-
import ring_theory.polynomial.cyclotomic.basic
7+
import ring_theory.polynomial.cyclotomic.roots
88
import tactic.by_contra
99
import topology.algebra.polynomial
1010
import number_theory.padics.padic_val

‎src/ring_theory/polynomial/cyclotomic/expand.lean‎

Lines changed: 186 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,186 @@
1+
/-
2+
Copyright (c) 2020 Riccardo Brasca. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Riccardo Brasca
5+
-/
6+
7+
import ring_theory.polynomial.cyclotomic.roots
8+
9+
/-!
10+
# Cyclotomic polynomials and `expand`.
11+
12+
We gather results relating cyclotomic polynomials and `expand`.
13+
14+
## Main results
15+
16+
* `polynomial.cyclotomic_expand_eq_cyclotomic_mul` : If `p` is a prime such that `¬ p ∣ n`, then
17+
`expand R p (cyclotomic n R) = (cyclotomic (n * p) R) * (cyclotomic n R)`.
18+
* `polynomial.cyclotomic_expand_eq_cyclotomic` : If `p` is a prime such that `p ∣ n`, then
19+
`expand R p (cyclotomic n R) = cyclotomic (p * n) R`.
20+
* `polynomial.cyclotomic_mul_prime_eq_pow_of_not_dvd` : If `R` is of characteristic `p` and
21+
`¬p ∣ n`, then `cyclotomic (n * p) R = (cyclotomic n R) ^ (p - 1)`.
22+
* `polynomial.cyclotomic_mul_prime_dvd_eq_pow` : If `R` is of characteristic `p` and `p ∣ n`, then
23+
`cyclotomic (n * p) R = (cyclotomic n R) ^ p`.
24+
* `polynomial.cyclotomic_mul_prime_pow_eq` : If `R` is of characteristic `p` and `¬p ∣ m`, then
25+
`cyclotomic (p ^ k * m) R = (cyclotomic m R) ^ (p ^ k - p ^ (k - 1))`.
26+
* `polynomial.cyclotomic_mul_prime_pow_eq` : If `R` is of characteristic `p` and `¬p ∣ m`, then
27+
`cyclotomic (p ^ k * m) R = (cyclotomic m R) ^ (p ^ k - p ^ (k - 1))`.
28+
-/
29+
30+
namespace polynomial
31+
32+
/-- If `p` is a prime such that `¬ p ∣ n`, then
33+
`expand R p (cyclotomic n R) = (cyclotomic (n * p) R) * (cyclotomic n R)`. -/
34+
@[simp] lemma cyclotomic_expand_eq_cyclotomic_mul {p n : ℕ} (hp : nat.prime p) (hdiv : ¬p ∣ n)
35+
(R : Type*) [comm_ring R] :
36+
expand R p (cyclotomic n R) = (cyclotomic (n * p) R) * (cyclotomic n R) :=
37+
begin
38+
rcases nat.eq_zero_or_pos n with rfl | hnpos,
39+
{ simp },
40+
haveI := ne_zero.of_pos hnpos,
41+
suffices : expand ℤ p (cyclotomic n ℤ) = (cyclotomic (n * p) ℤ) * (cyclotomic n ℤ),
42+
{ rw [← map_cyclotomic_int, ← map_expand, this, polynomial.map_mul, map_cyclotomic_int] },
43+
refine eq_of_monic_of_dvd_of_nat_degree_le ((cyclotomic.monic _ _).mul
44+
(cyclotomic.monic _ _)) ((cyclotomic.monic n ℤ).expand hp.pos) _ _,
45+
{ refine (is_primitive.int.dvd_iff_map_cast_dvd_map_cast _ _ (is_primitive.mul
46+
(cyclotomic.is_primitive (n * p) ℤ) (cyclotomic.is_primitive n ℤ))
47+
((cyclotomic.monic n ℤ).expand hp.pos).is_primitive).2 _,
48+
rw [polynomial.map_mul, map_cyclotomic_int, map_cyclotomic_int, map_expand, map_cyclotomic_int],
49+
refine is_coprime.mul_dvd (cyclotomic.is_coprime_rat (λ h, _)) _ _,
50+
{ replace h : n * p = n * 1 := by simp [h],
51+
exact nat.prime.ne_one hp (mul_left_cancel₀ hnpos.ne' h) },
52+
{ have hpos : 0 < n * p := mul_pos hnpos hp.pos,
53+
have hprim := complex.is_primitive_root_exp _ hpos.ne',
54+
rw [cyclotomic_eq_minpoly_rat hprim hpos],
55+
refine @minpoly.dvd ℚ ℂ _ _ algebra_rat _ _ _,
56+
rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← is_root.def,
57+
is_root_cyclotomic_iff],
58+
convert is_primitive_root.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n),
59+
rw [nat.mul_div_cancel _ (nat.prime.pos hp)] },
60+
{ have hprim := complex.is_primitive_root_exp _ hnpos.ne.symm,
61+
rw [cyclotomic_eq_minpoly_rat hprim hnpos],
62+
refine @minpoly.dvd ℚ ℂ _ _ algebra_rat _ _ _,
63+
rw [aeval_def, ← eval_map, map_expand, expand_eval, ← is_root.def,
64+
← cyclotomic_eq_minpoly_rat hprim hnpos, map_cyclotomic, is_root_cyclotomic_iff],
65+
exact is_primitive_root.pow_of_prime hprim hp hdiv,} },
66+
{ rw [nat_degree_expand, nat_degree_cyclotomic, nat_degree_mul (cyclotomic_ne_zero _ ℤ)
67+
(cyclotomic_ne_zero _ ℤ), nat_degree_cyclotomic, nat_degree_cyclotomic, mul_comm n,
68+
nat.totient_mul ((nat.prime.coprime_iff_not_dvd hp).2 hdiv),
69+
nat.totient_prime hp, mul_comm (p - 1), ← nat.mul_succ, nat.sub_one,
70+
nat.succ_pred_eq_of_pos hp.pos] }
71+
end
72+
73+
/-- If `p` is a prime such that `p ∣ n`, then
74+
`expand R p (cyclotomic n R) = cyclotomic (p * n) R`. -/
75+
@[simp] lemma cyclotomic_expand_eq_cyclotomic {p n : ℕ} (hp : nat.prime p) (hdiv : p ∣ n)
76+
(R : Type*) [comm_ring R] : expand R p (cyclotomic n R) = cyclotomic (n * p) R :=
77+
begin
78+
rcases n.eq_zero_or_pos with rfl | hzero,
79+
{ simp },
80+
haveI := ne_zero.of_pos hzero,
81+
suffices : expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ,
82+
{ rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int] },
83+
refine eq_of_monic_of_dvd_of_nat_degree_le (cyclotomic.monic _ _)
84+
((cyclotomic.monic n ℤ).expand hp.pos) _ _,
85+
{ have hpos := nat.mul_pos hzero hp.pos,
86+
have hprim := complex.is_primitive_root_exp _ hpos.ne.symm,
87+
rw [cyclotomic_eq_minpoly hprim hpos],
88+
refine minpoly.is_integrally_closed_dvd (hprim.is_integral hpos) _,
89+
rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval,
90+
← is_root.def, is_root_cyclotomic_iff],
91+
{ convert is_primitive_root.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n),
92+
rw [nat.mul_div_cancel _ hp.pos] } },
93+
{ rw [nat_degree_expand, nat_degree_cyclotomic, nat_degree_cyclotomic, mul_comm n,
94+
nat.totient_mul_of_prime_of_dvd hp hdiv, mul_comm] }
95+
end
96+
97+
/-- If the `p ^ n`th cyclotomic polynomial is irreducible, so is the `p ^ m`th, for `m ≤ n`. -/
98+
lemma cyclotomic_irreducible_pow_of_irreducible_pow {p : ℕ} (hp : nat.prime p)
99+
{R} [comm_ring R] [is_domain R] {n m : ℕ} (hmn : m ≤ n)
100+
(h : irreducible (cyclotomic (p ^ n) R)) : irreducible (cyclotomic (p ^ m) R) :=
101+
begin
102+
unfreezingI
103+
{ rcases m.eq_zero_or_pos with rfl | hm,
104+
{ simpa using irreducible_X_sub_C (1 : R) },
105+
obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le hmn,
106+
induction k with k hk },
107+
{ simpa using h },
108+
have : m + k ≠ 0 := (add_pos_of_pos_of_nonneg hm k.zero_le).ne',
109+
rw [nat.add_succ, pow_succ', ←cyclotomic_expand_eq_cyclotomic hp $ dvd_pow_self p this] at h,
110+
exact hk (by linarith) (of_irreducible_expand hp.ne_zero h)
111+
end
112+
113+
/-- If `irreducible (cyclotomic (p ^ n) R)` then `irreducible (cyclotomic p R).` -/
114+
lemma cyclotomic_irreducible_of_irreducible_pow {p : ℕ} (hp : nat.prime p) {R} [comm_ring R]
115+
[is_domain R] {n : ℕ} (hn : n ≠ 0) (h : irreducible (cyclotomic (p ^ n) R)) :
116+
irreducible (cyclotomic p R) :=
117+
pow_one p ▸ cyclotomic_irreducible_pow_of_irreducible_pow hp hn.bot_lt h
118+
119+
section char_p
120+
121+
/-- If `R` is of characteristic `p` and `¬p ∣ n`, then
122+
`cyclotomic (n * p) R = (cyclotomic n R) ^ (p - 1)`. -/
123+
lemma cyclotomic_mul_prime_eq_pow_of_not_dvd (R : Type*) {p n : ℕ} [hp : fact (nat.prime p)]
124+
[ring R] [char_p R p] (hn : ¬p ∣ n) : cyclotomic (n * p) R = (cyclotomic n R) ^ (p - 1) :=
125+
begin
126+
suffices : cyclotomic (n * p) (zmod p) = (cyclotomic n (zmod p)) ^ (p - 1),
127+
{ rw [← map_cyclotomic _ (algebra_map (zmod p) R), ← map_cyclotomic _ (algebra_map (zmod p) R),
128+
this, polynomial.map_pow] },
129+
apply mul_right_injective₀ (cyclotomic_ne_zero n $ zmod p),
130+
rw [←pow_succ, tsub_add_cancel_of_le hp.out.one_lt.le, mul_comm, ← zmod.expand_card],
131+
nth_rewrite 2 [← map_cyclotomic_int],
132+
rw [← map_expand, cyclotomic_expand_eq_cyclotomic_mul hp.out hn, polynomial.map_mul,
133+
map_cyclotomic, map_cyclotomic]
134+
end
135+
136+
/-- If `R` is of characteristic `p` and `p ∣ n`, then
137+
`cyclotomic (n * p) R = (cyclotomic n R) ^ p`. -/
138+
lemma cyclotomic_mul_prime_dvd_eq_pow (R : Type*) {p n : ℕ} [hp : fact (nat.prime p)] [ring R]
139+
[char_p R p] (hn : p ∣ n) : cyclotomic (n * p) R = (cyclotomic n R) ^ p :=
140+
begin
141+
suffices : cyclotomic (n * p) (zmod p) = (cyclotomic n (zmod p)) ^ p,
142+
{ rw [← map_cyclotomic _ (algebra_map (zmod p) R), ← map_cyclotomic _ (algebra_map (zmod p) R),
143+
this, polynomial.map_pow] },
144+
rw [← zmod.expand_card, ← map_cyclotomic_int n, ← map_expand, cyclotomic_expand_eq_cyclotomic
145+
hp.out hn, map_cyclotomic, mul_comm]
146+
end
147+
148+
/-- If `R` is of characteristic `p` and `¬p ∣ m`, then
149+
`cyclotomic (p ^ k * m) R = (cyclotomic m R) ^ (p ^ k - p ^ (k - 1))`. -/
150+
lemma cyclotomic_mul_prime_pow_eq (R : Type*) {p m : ℕ} [fact (nat.prime p)]
151+
[ring R] [char_p R p] (hm : ¬p ∣ m) :
152+
∀ {k}, 0 < k → cyclotomic (p ^ k * m) R = (cyclotomic m R) ^ (p ^ k - p ^ (k - 1))
153+
| 1 _ := by rw [pow_one, nat.sub_self, pow_zero, mul_comm,
154+
cyclotomic_mul_prime_eq_pow_of_not_dvd R hm]
155+
| (a + 2) _ :=
156+
begin
157+
have hdiv : p ∣ p ^ a.succ * m := ⟨p ^ a * m, by rw [← mul_assoc, pow_succ]⟩,
158+
rw [pow_succ, mul_assoc, mul_comm, cyclotomic_mul_prime_dvd_eq_pow R hdiv,
159+
cyclotomic_mul_prime_pow_eq a.succ_pos, ← pow_mul],
160+
congr' 1,
161+
simp only [tsub_zero, nat.succ_sub_succ_eq_sub],
162+
rw [nat.mul_sub_right_distrib, mul_comm, pow_succ']
163+
end
164+
165+
/-- If `R` is of characteristic `p` and `¬p ∣ m`, then `ζ` is a root of `cyclotomic (p ^ k * m) R`
166+
if and only if it is a primitive `m`-th root of unity. -/
167+
lemma is_root_cyclotomic_prime_pow_mul_iff_of_char_p {m k p : ℕ} {R : Type*} [comm_ring R]
168+
[is_domain R] [hp : fact (nat.prime p)] [hchar : char_p R p] {μ : R} [ne_zero (m : R)] :
169+
(polynomial.cyclotomic (p ^ k * m) R).is_root μ ↔ is_primitive_root μ m :=
170+
begin
171+
rcases k.eq_zero_or_pos with rfl | hk,
172+
{ rw [pow_zero, one_mul, is_root_cyclotomic_iff] },
173+
refine ⟨λ h, _, λ h, _⟩,
174+
{ rw [is_root.def, cyclotomic_mul_prime_pow_eq R (ne_zero.not_char_dvd R p m) hk, eval_pow] at h,
175+
replace h := pow_eq_zero h,
176+
rwa [← is_root.def, is_root_cyclotomic_iff] at h },
177+
{ rw [← is_root_cyclotomic_iff, is_root.def] at h,
178+
rw [cyclotomic_mul_prime_pow_eq R (ne_zero.not_char_dvd R p m) hk,
179+
is_root.def, eval_pow, h, zero_pow],
180+
simp only [tsub_pos_iff_lt],
181+
apply pow_strict_mono_right hp.out.one_lt (nat.pred_lt hk.ne') }
182+
end
183+
184+
end char_p
185+
186+
end polynomial

0 commit comments

Comments
 (0)