mathlib3 documentation

ring_theory.polynomial.cyclotomic.basic

Cyclotomic polynomials. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For n : ℕ and an integral domain R, we define a modified version of the n-th cyclotomic polynomial with coefficients in R, denoted cyclotomic' n R, as ∏ (X - μ), where μ varies over the primitive nth roots of unity. If there is a primitive nth root of unity in R then this the standard definition. We then define the standard cyclotomic polynomial cyclotomic n R with coefficients in any ring R.

Main definition #

cyclotomic n R : the n-th cyclotomic polynomial with coefficients in R.

Main results #

polynomial.degree_cyclotomic : The degree of cyclotomic n is totient n.
polynomial.prod_cyclotomic_eq_X_pow_sub_one : X ^ n - 1 = ∏ (cyclotomic i), where i divides n.
polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius : The Möbius inversion formula for cyclotomic n R over an abstract fraction field for R[X].

Implementation details #

Our definition of cyclotomic' n R makes sense in any integral domain R, but the interesting results hold if there is a primitive n-th root of unity in R. In particular, our definition is not the standard one unless there is a primitive nth root of unity in R. For example, cyclotomic' 3 ℤ = 1, since there are no primitive cube roots of unity in ℤ. The main example is R = ℂ, we decided to work in general since the difficulties are essentially the same. To get the standard cyclotomic polynomials, we use int_coeff_of_cycl, with R = ℂ, to get a polynomial with integer coefficients and then we map it to R[X], for any ring R. To prove cyclotomic.irreducible, the irreducibility of cyclotomic n ℤ, we show in cyclotomic_eq_minpoly that cyclotomic n ℤ is the minimal polynomial of any n-th primitive root of unity μ : K, where K is a field of characteristic 0.

noncomputable def polynomial.cyclotomic' (n : ℕ) (R : Type u_1) [comm_ring R] [is_domain R] :

The modified n-th cyclotomic polynomial with coefficients in R, it is the usual cyclotomic polynomial if there is a primitive n-th root of unity in R.

Equations

polynomial.cyclotomic' n R = (primitive_roots n R).prod (λ (μ : R), polynomial.X - ⇑polynomial.C μ)

@[simp]

theorem polynomial.cyclotomic'_zero (R : Type u_1) [comm_ring R] [is_domain R] :

polynomial.cyclotomic' 0 R = 1

The zeroth modified cyclotomic polyomial is 1.

@[simp]

theorem polynomial.cyclotomic'_one (R : Type u_1) [comm_ring R] [is_domain R] :

polynomial.cyclotomic' 1 R = polynomial.X - 1

The first modified cyclotomic polyomial is X - 1.

@[simp]

theorem polynomial.cyclotomic'_two (R : Type u_1) [comm_ring R] [is_domain R] (p : ℕ) [char_p R p] (hp : p ≠ 2) :

polynomial.cyclotomic' 2 R = polynomial.X + 1

The second modified cyclotomic polyomial is X + 1 if the characteristic of R is not 2.

theorem polynomial.cyclotomic'.monic (n : ℕ) (R : Type u_1) [comm_ring R] [is_domain R] :

(polynomial.cyclotomic' n R).monic

cyclotomic' n R is monic.

theorem polynomial.cyclotomic'_ne_zero (n : ℕ) (R : Type u_1) [comm_ring R] [is_domain R] :

polynomial.cyclotomic' n R ≠ 0

cyclotomic' n R is different from 0.

theorem polynomial.nat_degree_cyclotomic' {R : Type u_1} [comm_ring R] [is_domain R] {ζ : R} {n : ℕ} (h : is_primitive_root ζ n) :

(polynomial.cyclotomic' n R).nat_degree = n.totient

The natural degree of cyclotomic' n R is totient n if there is a primitive root of unity in R.

theorem polynomial.degree_cyclotomic' {R : Type u_1} [comm_ring R] [is_domain R] {ζ : R} {n : ℕ} (h : is_primitive_root ζ n) :

(polynomial.cyclotomic' n R).degree = ↑(n.totient)

The degree of cyclotomic' n R is totient n if there is a primitive root of unity in R.

theorem polynomial.roots_of_cyclotomic (n : ℕ) (R : Type u_1) [comm_ring R] [is_domain R] :

(polynomial.cyclotomic' n R).roots = (primitive_roots n R).val

The roots of cyclotomic' n R are the primitive n-th roots of unity.

theorem polynomial.X_pow_sub_one_eq_prod {R : Type u_1} [comm_ring R] [is_domain R] {ζ : R} {n : ℕ} (hpos : 0 < n) (h : is_primitive_root ζ n) :

polynomial.X ^ n - 1 = (polynomial.nth_roots_finset n R).prod (λ (ζ : R), polynomial.X - ⇑polynomial.C ζ)

If there is a primitive nth root of unity in K, then X ^ n - 1 = ∏ (X - μ), where μ varies over the n-th roots of unity.

theorem polynomial.cyclotomic'_splits {K : Type u_1} [field K] (n : ℕ) :

polynomial.splits (ring_hom.id K) (polynomial.cyclotomic' n K)

cyclotomic' n K splits.

theorem polynomial.X_pow_sub_one_splits {K : Type u_1} [field K] {ζ : K} {n : ℕ} (h : is_primitive_root ζ n) :

polynomial.splits (ring_hom.id K) (polynomial.X ^ n - ⇑polynomial.C 1)

If there is a primitive n-th root of unity in K, then X ^ n - 1splits.

theorem polynomial.prod_cyclotomic'_eq_X_pow_sub_one {K : Type u_1} [comm_ring K] [is_domain K] {ζ : K} {n : ℕ} (hpos : 0 < n) (h : is_primitive_root ζ n) :

n.divisors.prod (λ (i : ℕ), polynomial.cyclotomic' i K) = polynomial.X ^ n - 1

If there is a primitive n-th root of unity in K, then ∏ i in nat.divisors n, cyclotomic' i K = X ^ n - 1.

theorem polynomial.cyclotomic'_eq_X_pow_sub_one_div {K : Type u_1} [comm_ring K] [is_domain K] {ζ : K} {n : ℕ} (hpos : 0 < n) (h : is_primitive_root ζ n) :

polynomial.cyclotomic' n K = (polynomial.X ^ n - 1) /ₘ n.proper_divisors.prod (λ (i : ℕ), polynomial.cyclotomic' i K)

If there is a primitive n-th root of unity in K, then cyclotomic' n K = (X ^ k - 1) /ₘ (∏ i in nat.proper_divisors k, cyclotomic' i K).

theorem polynomial.int_coeff_of_cyclotomic' {K : Type u_1} [comm_ring K] [is_domain K] {ζ : K} {n : ℕ} (h : is_primitive_root ζ n) :

∃ (P : polynomial ℤ), polynomial.map (int.cast_ring_hom K) P = polynomial.cyclotomic' n K ∧ P.degree = (polynomial.cyclotomic' n K).degree ∧ P.monic

If there is a primitive n-th root of unity in K, then cyclotomic' n K comes from a monic polynomial with integer coefficients.

theorem polynomial.unique_int_coeff_of_cycl {K : Type u_1} [comm_ring K] [is_domain K] [char_zero K] {ζ : K} {n : ℕ+} (h : is_primitive_root ζ ↑n) :

∃! (P : polynomial ℤ), polynomial.map (int.cast_ring_hom K) P = polynomial.cyclotomic' ↑n K

If K is of characteristic 0 and there is a primitive n-th root of unity in K, then cyclotomic n K comes from a unique polynomial with integer coefficients.

noncomputable def polynomial.cyclotomic (n : ℕ) (R : Type u_1) [ring R] :

The n-th cyclotomic polynomial with coefficients in R.

Equations

polynomial.cyclotomic n R = dite (n = 0) (λ (h : n = 0), 1) (λ (h : ¬n = 0), polynomial.map (int.cast_ring_hom R) _.some)

theorem polynomial.int_cyclotomic_rw {n : ℕ} (h : n ≠ 0) :

polynomial.cyclotomic n ℤ = _.some

theorem polynomial.map_cyclotomic_int (n : ℕ) (R : Type u_1) [ring R] :

polynomial.map (int.cast_ring_hom R) (polynomial.cyclotomic n ℤ) = polynomial.cyclotomic n R

cyclotomic n R comes from cyclotomic n ℤ.

theorem polynomial.int_cyclotomic_spec (n : ℕ) :

theorem polynomial.int_cyclotomic_unique {n : ℕ} {P : polynomial ℤ} (h : polynomial.map (int.cast_ring_hom ℂ) P = polynomial.cyclotomic' n ℂ) :

P = polynomial.cyclotomic n ℤ

@[simp]

theorem polynomial.map_cyclotomic (n : ℕ) {R : Type u_1} {S : Type u_2} [ring R] [ring S] (f : R →+* S) :

polynomial.map f (polynomial.cyclotomic n R) = polynomial.cyclotomic n S

The definition of cyclotomic n R commutes with any ring homomorphism.

theorem polynomial.cyclotomic.eval_apply {R : Type u_1} {S : Type u_2} (q : R) (n : ℕ) [ring R] [ring S] (f : R →+* S) :

polynomial.eval (⇑f q) (polynomial.cyclotomic n S) = ⇑f (polynomial.eval q (polynomial.cyclotomic n R))

@[simp]

theorem polynomial.cyclotomic_zero (R : Type u_1) [ring R] :

polynomial.cyclotomic 0 R = 1

The zeroth cyclotomic polyomial is 1.

@[simp]

theorem polynomial.cyclotomic_one (R : Type u_1) [ring R] :

polynomial.cyclotomic 1 R = polynomial.X - 1

The first cyclotomic polyomial is X - 1.

theorem polynomial.cyclotomic.monic (n : ℕ) (R : Type u_1) [ring R] :

(polynomial.cyclotomic n R).monic

cyclotomic n is monic.

theorem polynomial.cyclotomic.is_primitive (n : ℕ) (R : Type u_1) [comm_ring R] :

(polynomial.cyclotomic n R).is_primitive

cyclotomic n is primitive.

theorem polynomial.cyclotomic_ne_zero (n : ℕ) (R : Type u_1) [ring R] [nontrivial R] :

polynomial.cyclotomic n R ≠ 0

cyclotomic n R is different from 0.

theorem polynomial.degree_cyclotomic (n : ℕ) (R : Type u_1) [ring R] [nontrivial R] :

(polynomial.cyclotomic n R).degree = ↑(n.totient)

The degree of cyclotomic n is totient n.

theorem polynomial.nat_degree_cyclotomic (n : ℕ) (R : Type u_1) [ring R] [nontrivial R] :

(polynomial.cyclotomic n R).nat_degree = n.totient

The natural degree of cyclotomic n is totient n.

theorem polynomial.degree_cyclotomic_pos (n : ℕ) (R : Type u_1) (hpos : 0 < n) [ring R] [nontrivial R] :

0 < (polynomial.cyclotomic n R).degree

The degree of cyclotomic n R is positive.

theorem polynomial.prod_cyclotomic_eq_X_pow_sub_one {n : ℕ} (hpos : 0 < n) (R : Type u_1) [comm_ring R] :

n.divisors.prod (λ (i : ℕ), polynomial.cyclotomic i R) = polynomial.X ^ n - 1

∏ i in nat.divisors n, cyclotomic i R = X ^ n - 1.

theorem polynomial.cyclotomic.dvd_X_pow_sub_one (n : ℕ) (R : Type u_1) [ring R] :

polynomial.cyclotomic n R ∣ polynomial.X ^ n - 1

theorem polynomial.prod_cyclotomic_eq_geom_sum {n : ℕ} (h : 0 < n) (R : Type u_1) [comm_ring R] :

(n.divisors.erase 1).prod (λ (i : ℕ), polynomial.cyclotomic i R) = (finset.range n).sum (λ (i : ℕ), polynomial.X ^ i)

theorem polynomial.cyclotomic_prime (R : Type u_1) [ring R] (p : ℕ) [hp : fact (nat.prime p)] :

polynomial.cyclotomic p R = (finset.range p).sum (λ (i : ℕ), polynomial.X ^ i)

If p is prime, then cyclotomic p R = ∑ i in range p, X ^ i.

theorem polynomial.cyclotomic_prime_mul_X_sub_one (R : Type u_1) [ring R] (p : ℕ) [hn : fact (nat.prime p)] :

polynomial.cyclotomic p R * (polynomial.X - 1) = polynomial.X ^ p - 1

@[simp]

theorem polynomial.cyclotomic_two (R : Type u_1) [ring R] :

polynomial.cyclotomic 2 R = polynomial.X + 1

@[simp]

theorem polynomial.cyclotomic_three (R : Type u_1) [ring R] :

polynomial.cyclotomic 3 R = polynomial.X ^ 2 + polynomial.X + 1

theorem polynomial.cyclotomic_dvd_geom_sum_of_dvd (R : Type u_1) [ring R] {d n : ℕ} (hdn : d ∣ n) (hd : d ≠ 1) :

polynomial.cyclotomic d R ∣ (finset.range n).sum (λ (i : ℕ), polynomial.X ^ i)

theorem polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd (R : Type u_1) [comm_ring R] {d n : ℕ} (h : d ∈ n.proper_divisors) :

(polynomial.X ^ d - 1) * (n.divisors \ d.divisors).prod (λ (x : ℕ), polynomial.cyclotomic x R) = polynomial.X ^ n - 1

theorem polynomial.X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd (R : Type u_1) [comm_ring R] {d n : ℕ} (h : d ∈ n.proper_divisors) :

(polynomial.X ^ d - 1) * polynomial.cyclotomic n R ∣ polynomial.X ^ n - 1

theorem polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius {n : ℕ} (R : Type u_1) [comm_ring R] [is_domain R] :

⇑(algebra_map (polynomial R) (ratfunc R)) (polynomial.cyclotomic n R) = n.divisors_antidiagonal.prod (λ (i : ℕ × ℕ), ⇑(algebra_map (polynomial R) (ratfunc R)) (polynomial.X ^ i.snd - 1) ^ ⇑nat.arithmetic_function.moebius i.fst)

cyclotomic n R can be expressed as a product in a fraction field of R[X] using Möbius inversion.

theorem polynomial.cyclotomic_eq_X_pow_sub_one_div {R : Type u_1} [comm_ring R] {n : ℕ} (hpos : 0 < n) :

polynomial.cyclotomic n R = (polynomial.X ^ n - 1) /ₘ n.proper_divisors.prod (λ (i : ℕ), polynomial.cyclotomic i R)

We have cyclotomic n R = (X ^ k - 1) /ₘ (∏ i in nat.proper_divisors k, cyclotomic i K).

theorem polynomial.X_pow_sub_one_dvd_prod_cyclotomic (R : Type u_1) [comm_ring R] {n m : ℕ} (hpos : 0 < n) (hm : m ∣ n) (hdiff : m ≠ n) :

polynomial.X ^ m - 1 ∣ n.proper_divisors.prod (λ (i : ℕ), polynomial.cyclotomic i R)

If m is a proper divisor of n, then X ^ m - 1 divides ∏ i in nat.proper_divisors n, cyclotomic i R.

theorem polynomial.cyclotomic_eq_prod_X_sub_primitive_roots {K : Type u_1} [comm_ring K] [is_domain K] {ζ : K} {n : ℕ} (hz : is_primitive_root ζ n) :

polynomial.cyclotomic n K = (primitive_roots n K).prod (λ (μ : K), polynomial.X - ⇑polynomial.C μ)

If there is a primitive n-th root of unity in K, then cyclotomic n K = ∏ μ in primitive_roots n R, (X - C μ). In particular, cyclotomic n K = cyclotomic' n K

theorem polynomial.eq_cyclotomic_iff {R : Type u_1} [comm_ring R] {n : ℕ} (hpos : 0 < n) (P : polynomial R) :

P = polynomial.cyclotomic n R ↔ P * n.proper_divisors.prod (λ (i : ℕ), polynomial.cyclotomic i R) = polynomial.X ^ n - 1

theorem polynomial.cyclotomic_prime_pow_eq_geom_sum {R : Type u_1} [comm_ring R] {p n : ℕ} (hp : nat.prime p) :

polynomial.cyclotomic (p ^ (n + 1)) R = (finset.range p).sum (λ (i : ℕ), (polynomial.X ^ p ^ n) ^ i)

If p ^ k is a prime power, then cyclotomic (p ^ (n + 1)) R = ∑ i in range p, (X ^ (p ^ n)) ^ i.

theorem polynomial.cyclotomic_prime_pow_mul_X_pow_sub_one (R : Type u_1) [comm_ring R] (p k : ℕ) [hn : fact (nat.prime p)] :

polynomial.cyclotomic (p ^ (k + 1)) R * (polynomial.X ^ p ^ k - 1) = polynomial.X ^ p ^ (k + 1) - 1

theorem polynomial.cyclotomic_coeff_zero (R : Type u_1) [comm_ring R] {n : ℕ} (hn : 1 < n) :

(polynomial.cyclotomic n R).coeff 0 = 1

The constant term of cyclotomic n R is 1 if 2 ≤ n.

theorem polynomial.coprime_of_root_cyclotomic {n : ℕ} (hpos : 0 < n) {p : ℕ} [hprime : fact (nat.prime p)] {a : ℕ} (hroot : (polynomial.cyclotomic n (zmod p)).is_root (⇑(nat.cast_ring_hom (zmod p)) a)) :

If (a : ℕ) is a root of cyclotomic n (zmod p), where p is a prime, then a and p are coprime.

theorem polynomial.order_of_root_cyclotomic_dvd {n : ℕ} (hpos : 0 < n) {p : ℕ} [fact (nat.prime p)] {a : ℕ} (hroot : (polynomial.cyclotomic n (zmod p)).is_root (⇑(nat.cast_ring_hom (zmod p)) a)) :

order_of (zmod.unit_of_coprime a _) ∣ n

If (a : ℕ) is a root of cyclotomic n (zmod p), then the multiplicative order of a modulo p divides n.