# mathlib3documentation

number_theory.cyclotomic.primitive_roots

# Primitive roots in cyclotomic fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. If is_cyclotomic_extension {n} A B, we define an element zeta n A B : B that is a primitive nth-root of unity in B and we study its properties. We also prove related theorems under the more general assumption of just being a primitive root, for reasons described in the implementation details section.

## Main definitions #

• is_cyclotomic_extension.zeta n A B: if is_cyclotomic_extension {n} A B, than zeta n A B is a primitive n-th root of unity in B.
• is_primitive_root.power_basis: if K and L are fields such that is_cyclotomic_extension {n} K L, then is_primitive_root.power_basis gives a K-power basis for L given a primitive root ζ.
• is_primitive_root.embeddings_equiv_primitive_roots: the equivalence between L →ₐ[K] A and primitive_roots n A given by the choice of ζ.

## Main results #

• is_cyclotomic_extension.zeta_spec: zeta n A B is a primitive n-th root of unity.
• is_cyclotomic_extension.finrank: if irreducible (cyclotomic n K) (in particular for K = ℚ), then the finrank of a cyclotomic extension is n.totient.
• is_primitive_root.norm_eq_one: if irreducible (cyclotomic n K) (in particular for K = ℚ), the norm of a primitive root is 1 if n ≠ 2.
• is_primitive_root.sub_one_norm_eq_eval_cyclotomic: if irreducible (cyclotomic n K) (in particular for K = ℚ), then the norm of ζ - 1 is eval 1 (cyclotomic n ℤ), for a primitive root ζ. We also prove the analogous of this result for zeta.
• is_primitive_root.pow_sub_one_norm_prime_pow_ne_two : if irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of ζ ^ (p ^ s) - 1 is p ^ (p ^ s) p ^ (k - s + 1) ≠ 2. See the following lemmas for similar results. We also prove the analogous of this result for zeta.
• is_primitive_root.sub_one_norm_prime_ne_two : if irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is an odd prime, then the norm of ζ - 1 is p. We also prove the analogous of this result for zeta.
• is_primitive_root.embeddings_equiv_primitive_roots: the equivalence between L →ₐ[K] A and primitive_roots n A given by the choice of ζ.

## Implementation details #

zeta n A B is defined as any primitive root of unity in B, - this must exist, by definition of is_cyclotomic_extension. It is not true in general that it is a root of cyclotomic n B, but this holds if is_domain B and ne_zero (↑n : B).

zeta n A B is defined using exists.some, which means we cannot control it. For example, in normal mathematics, we can demand that (zeta p ℤ ℤ[ζₚ] : ℚ(ζₚ)) is equal to zeta p ℚ ℚ(ζₚ), as we are just choosing "an arbitrary primitive root" and we can internally specify that our choices agree. This is not the case here, and it is indeed impossible to prove that these two are equal. Therefore, whenever possible, we prove our results for any primitive root, and only at the "final step", when we need to provide an "explicit" primitive root, we use zeta.

noncomputable def is_cyclotomic_extension.zeta (n : ℕ+) (A : Type w) (B : Type z) [comm_ring A] [comm_ring B] [ B] [ B] :
B

If B is a n-th cyclotomic extension of A, then zeta n A B is a primitive root of unity in B.

Equations
@[simp]
theorem is_cyclotomic_extension.zeta_spec (n : ℕ+) (A : Type w) (B : Type z) [comm_ring A] [comm_ring B] [ B] [ B] :

zeta n A B is a primitive n-th root of unity.

theorem is_cyclotomic_extension.aeval_zeta (n : ℕ+) (A : Type w) (B : Type z) [comm_ring A] [comm_ring B] [ B] [ B] [is_domain B] [ne_zero n] :
= 0
theorem is_cyclotomic_extension.zeta_is_root (n : ℕ+) (A : Type w) (B : Type z) [comm_ring A] [comm_ring B] [ B] [ B] [is_domain B] [ne_zero n] :
B)
theorem is_cyclotomic_extension.zeta_pow (n : ℕ+) (A : Type w) (B : Type z) [comm_ring A] [comm_ring B] [ B] [ B] :
= 1
@[simp]
theorem is_primitive_root.power_basis_dim {n : ℕ+} (K : Type u) {L : Type v} [field K] [comm_ring L] [is_domain L] [ L] [ L] {ζ : L} (hζ : n) :
@[protected]
noncomputable def is_primitive_root.power_basis {n : ℕ+} (K : Type u) {L : Type v} [field K] [comm_ring L] [is_domain L] [ L] [ L] {ζ : L} (hζ : n) :
L

The power_basis given by a primitive root η.

Equations
@[simp]
theorem is_primitive_root.power_basis_gen {n : ℕ+} (K : Type u) {L : Type v} [field K] [comm_ring L] [is_domain L] [ L] [ L] {ζ : L} (hζ : n) :
.gen = ζ
theorem is_primitive_root.power_basis_gen_mem_adjoin_zeta_sub_one {n : ℕ+} (K : Type u) {L : Type v} [field K] [comm_ring L] [is_domain L] [ L] [ L] {ζ : L} (hζ : n) :
.gen - 1}
@[simp]
theorem is_primitive_root.sub_one_power_basis_gen {n : ℕ+} (K : Type u) {L : Type v} [field K] [comm_ring L] [is_domain L] [ L] [ L] {ζ : L} (hζ : n) :
= ζ - 1
noncomputable def is_primitive_root.sub_one_power_basis {n : ℕ+} (K : Type u) {L : Type v} [field K] [comm_ring L] [is_domain L] [ L] [ L] {ζ : L} (hζ : n) :
L

The power_basis given by η - 1.

Equations
@[simp]
theorem is_primitive_root.sub_one_power_basis_dim {n : ℕ+} (K : Type u) {L : Type v} [field K] [comm_ring L] [is_domain L] [ L] [ L] {ζ : L} (hζ : n) :
= (minpoly K - 1)).nat_degree
noncomputable def is_primitive_root.embeddings_equiv_primitive_roots {n : ℕ+} {K : Type u} {L : Type v} [field K] [comm_ring L] [is_domain L] [ L] [ L] {ζ : L} (hζ : n) (C : Type u_1) [comm_ring C] [is_domain C] [ C] (hirr : irreducible ) :
(L →ₐ[K] C) C)

The equivalence between L →ₐ[K] C and primitive_roots n C given by a primitive root ζ.

Equations
@[simp]
theorem is_primitive_root.embeddings_equiv_primitive_roots_apply_coe {n : ℕ+} {K : Type u} {L : Type v} [field K] [comm_ring L] [is_domain L] [ L] [ L] {ζ : L} (hζ : n) (C : Type u_1) [comm_ring C] [is_domain C] [ C] (hirr : irreducible ) (φ : L →ₐ[K] C) :
( hirr) φ) = φ ζ
theorem is_cyclotomic_extension.finrank {n : ℕ+} {K : Type u} (L : Type v) [field K] [comm_ring L] [is_domain L] [ L] [ L] (hirr : irreducible ) :

If irreducible (cyclotomic n K) (in particular for K = ℚ), then the finrank of a cyclotomic extension is n.totient.

theorem is_primitive_root.norm_eq_neg_one_pow {K : Type u} {L : Type v} [comm_ring L] {ζ : L} [field K] [ L] (hζ : 2) [is_domain L] :
(algebra.norm K) ζ = (-1) ^

This mathematically trivial result is complementary to norm_eq_one below.

theorem is_primitive_root.norm_eq_one {n : ℕ+} {K : Type u} {L : Type v} [comm_ring L] {ζ : L} (hζ : n) [field K] [ L] [is_domain L] [ L] (hn : n 2) (hirr : irreducible ) :

If irreducible (cyclotomic n K) (in particular for K = ℚ), the norm of a primitive root is 1 if n ≠ 2.

theorem is_primitive_root.norm_eq_one_of_linearly_ordered {n : ℕ+} {L : Type v} [comm_ring L] {ζ : L} (hζ : n) {K : Type u_1} [ L] (hodd : odd n) :

If K is linearly ordered, the norm of a primitive root is 1 if n is odd.

theorem is_primitive_root.norm_of_cyclotomic_irreducible {n : ℕ+} {K : Type u} {L : Type v} [comm_ring L] {ζ : L} (hζ : n) [field K] [ L] [is_domain L] [ L] (hirr : irreducible ) :
(algebra.norm K) ζ = ite (n = 2) (-1) 1
theorem is_primitive_root.sub_one_norm_eq_eval_cyclotomic {n : ℕ+} {K : Type u} {L : Type v} [field L] {ζ : L} (hζ : n) [field K] [ L] [ L] (h : 2 < n) (hirr : irreducible ) :
(algebra.norm K) - 1) =

If irreducible (cyclotomic n K) (in particular for K = ℚ), then the norm of ζ - 1 is eval 1 (cyclotomic n ℤ).

theorem is_primitive_root.sub_one_norm_is_prime_pow {n : ℕ+} {K : Type u} {L : Type v} [field L] {ζ : L} (hζ : n) [field K] [ L] (hn : is_prime_pow n) [ L] (hirr : irreducible ) (h : n 2) :

If is_prime_pow (n : ℕ), n ≠ 2 and irreducible (cyclotomic n K) (in particular for K = ℚ), then the norm of ζ - 1 is (n : ℕ).min_fac.

theorem is_primitive_root.minpoly_sub_one_eq_cyclotomic_comp {n : ℕ+} {A : Type w} {K : Type u} [comm_ring A] [field K] [ A] [is_domain A] {ζ : A} [ A] (hζ : n) (h : irreducible ) :
- 1) = .comp
theorem is_primitive_root.pow_sub_one_norm_prime_pow_ne_two {p : ℕ+} {K : Type u} {L : Type v} [field L] {ζ : L} [field K] [ L] {k s : } (hζ : (p ^ (k + 1))) [hpri : fact (nat.prime p)] [is_cyclotomic_extension {p ^ (k + 1)} K L] (hirr : irreducible (polynomial.cyclotomic (p ^ (k + 1)) K)) (hs : s k) (htwo : p ^ (k - s + 1) 2) :
(algebra.norm K) ^ p ^ s - 1) = p ^ p ^ s

If irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of ζ ^ (p ^ s) - 1 is p ^ (p ^ s) if p ^ (k - s + 1) ≠ 2. See the next lemmas for similar results.

theorem is_primitive_root.pow_sub_one_norm_prime_ne_two {p : ℕ+} {K : Type u} {L : Type v} [field L] {ζ : L} [field K] [ L] {k : } (hζ : (p ^ (k + 1))) [hpri : fact (nat.prime p)] [is_cyclotomic_extension {p ^ (k + 1)} K L] (hirr : irreducible (polynomial.cyclotomic (p ^ (k + 1)) K)) {s : } (hs : s k) (hodd : p 2) :
(algebra.norm K) ^ p ^ s - 1) = p ^ p ^ s

If irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of ζ ^ (p ^ s) - 1 is p ^ (p ^ s) if p ≠ 2.

theorem is_primitive_root.sub_one_norm_prime_ne_two {p : ℕ+} {K : Type u} {L : Type v} [field L] {ζ : L} [field K] [ L] {k : } (hζ : (p ^ (k + 1))) [hpri : fact (nat.prime p)] [is_cyclotomic_extension {p ^ (k + 1)} K L] (hirr : irreducible (polynomial.cyclotomic (p ^ (k + 1)) K)) (h : p 2) :
(algebra.norm K) - 1) = p

If irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is an odd prime, then the norm of ζ - 1 is p.

theorem is_primitive_root.sub_one_norm_prime {p : ℕ+} {K : Type u} {L : Type v} [field L] {ζ : L} [field K] [ L] [hpri : fact (nat.prime p)] [hcyc : L] (hζ : p) (hirr : irreducible ) (h : p 2) :
(algebra.norm K) - 1) = p

If irreducible (cyclotomic p K) (in particular for K = ℚ) and p is an odd prime, then the norm of ζ - 1 is p.

theorem is_primitive_root.pow_sub_one_norm_two {K : Type u} {L : Type v} [field L] {ζ : L} [field K] [ L] {k : } (hζ : (2 ^ (k + 1))) [is_cyclotomic_extension {2 ^ (k + 1)} K L] (hirr : irreducible (polynomial.cyclotomic (2 ^ (k + 1)) K)) :
(algebra.norm K) ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

If irreducible (cyclotomic (2 ^ (k + 1)) K) (in particular for K = ℚ), then the norm of ζ ^ (2 ^ k) - 1 is (-2) ^ (2 ^ k).

theorem is_primitive_root.sub_one_norm_two {K : Type u} {L : Type v} [field L] {ζ : L} [field K] [ L] {k : } (hζ : (2 ^ k)) (hk : 2 k) [H : is_cyclotomic_extension {2 ^ k} K L] (hirr : irreducible (polynomial.cyclotomic (2 ^ k) K)) :
(algebra.norm K) - 1) = 2

If irreducible (cyclotomic (2 ^ k) K) (in particular for K = ℚ) and k is at least 2, then the norm of ζ - 1 is 2.

theorem is_primitive_root.pow_sub_one_norm_prime_pow_of_ne_zero {p : ℕ+} {K : Type u} {L : Type v} [field L] {ζ : L} [field K] [ L] {k s : } (hζ : (p ^ (k + 1))) [hpri : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p ^ (k + 1)} K L] (hirr : irreducible (polynomial.cyclotomic (p ^ (k + 1)) K)) (hs : s k) (hk : k 0) :
(algebra.norm K) ^ p ^ s - 1) = p ^ p ^ s

If irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of ζ ^ (p ^ s) - 1 is p ^ (p ^ s) if k ≠ 0 and s ≤ k.

theorem is_cyclotomic_extension.norm_zeta_eq_one {n : ℕ+} {K : Type u} (L : Type v) [field K] [field L] [ L] [ L] (hn : n 2) (hirr : irreducible ) :

If irreducible (cyclotomic n K) (in particular for K = ℚ), the norm of zeta n K L is 1 if n is odd.

theorem is_cyclotomic_extension.is_prime_pow_norm_zeta_sub_one {n : ℕ+} {K : Type u} (L : Type v) [field K] [field L] [ L] (hn : is_prime_pow n) [ L] (hirr : irreducible ) (h : n 2) :

If is_prime_pow (n : ℕ), n ≠ 2 and irreducible (cyclotomic n K) (in particular for K = ℚ), then the norm of zeta n K L - 1 is (n : ℕ).min_fac.

theorem is_cyclotomic_extension.prime_ne_two_pow_norm_zeta_pow_sub_one {p : ℕ+} {K : Type u} (L : Type v) [field K] [field L] [ L] {k : } [hpri : fact (nat.prime p)] [is_cyclotomic_extension {p ^ (k + 1)} K L] (hirr : irreducible (polynomial.cyclotomic (p ^ (k + 1)) K)) {s : } (hs : s k) (htwo : p ^ (k - s + 1) 2) :
(algebra.norm K) (is_cyclotomic_extension.zeta (p ^ (k + 1)) K L ^ p ^ s - 1) = p ^ p ^ s

If irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of (zeta (p ^ (k + 1)) K L) ^ (p ^ s) - 1 is p ^ (p ^ s) if p ^ (k - s + 1) ≠ 2.

theorem is_cyclotomic_extension.prime_ne_two_pow_norm_zeta_sub_one {p : ℕ+} {K : Type u} (L : Type v) [field K] [field L] [ L] {k : } [hpri : fact (nat.prime p)] [is_cyclotomic_extension {p ^ (k + 1)} K L] (hirr : irreducible (polynomial.cyclotomic (p ^ (k + 1)) K)) (h : p 2) :

If irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is an odd prime, then the norm of zeta (p ^ (k + 1)) K L - 1 is p.

theorem is_cyclotomic_extension.prime_ne_two_norm_zeta_sub_one {p : ℕ+} {K : Type u} (L : Type v) [field K] [field L] [ L] [hpri : fact (nat.prime p)] [hcyc : L] (hirr : irreducible ) (h : p 2) :

If irreducible (cyclotomic p K) (in particular for K = ℚ) and p is an odd prime, then the norm of zeta p K L - 1 is p.

theorem is_cyclotomic_extension.two_pow_norm_zeta_sub_one {K : Type u} (L : Type v) [field K] [field L] [ L] {k : } (hk : 2 k) [is_cyclotomic_extension {2 ^ k} K L] (hirr : irreducible (polynomial.cyclotomic (2 ^ k) K)) :
(algebra.norm K) K L - 1) = 2

If irreducible (cyclotomic (2 ^ k) K) (in particular for K = ℚ) and k is at least 2, then the norm of zeta (2 ^ k) K L - 1 is 2.