mathlib documentation

number_theory.cyclotomic.primitive_roots

Primitive roots in cyclotomic fields #

If is_cyclotomic_extension {n} A B, we define an element zeta n A B : B that is (under certain assumptions) a primitive n-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 #

Main results #

Implementation details #

zeta n A B is defined as any primitive root of unity in B, that exists by definition. 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] [algebra A B] [is_cyclotomic_extension {n} A 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]

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

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

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] [algebra K L] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ n) :
@[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] [algebra K L] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ n) :
noncomputable def is_primitive_root.sub_one_power_basis {n : ℕ+} (K : Type u) {L : Type v} [field K] [comm_ring L] [is_domain L] [algebra K L] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ n) :

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] [algebra K L] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ n) :
noncomputable def is_primitive_root.embeddings_equiv_primitive_roots {n : ℕ+} {K : Type u} {L : Type v} [field K] [comm_ring L] [is_domain L] [algebra K L] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ n) (C : Type u_1) [comm_ring C] [is_domain C] [algebra K C] (hirr : irreducible (polynomial.cyclotomic n K)) :

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_symm_apply_apply {n : ℕ+} {K : Type u} {L : Type v} [field K] [comm_ring L] [is_domain L] [algebra K L] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ n) (C : Type u_1) [comm_ring C] [is_domain C] [algebra K C] (hirr : irreducible (polynomial.cyclotomic n K)) (ᾰ : (primitive_roots n C)) (ᾰ_1 : L) :
@[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] [algebra K L] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ n) (C : Type u_1) [comm_ring C] [is_domain C] [algebra K C] (hirr : irreducible (polynomial.cyclotomic n K)) (ᾰ : L →ₐ[K] C) :

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} [field L] {ζ : L} [field K] [algebra K L] (hζ : is_primitive_root ζ 2) :

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} [field L] {ζ : L} (hζ : is_primitive_root ζ n) [field K] [algebra K L] [is_cyclotomic_extension {n} K L] (hn : n 2) (hirr : irreducible (polynomial.cyclotomic n K)) :

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} [field L] {ζ : L} (hζ : is_primitive_root ζ n) {K : Type u_1} [linear_ordered_field K] [algebra K 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} [field L] {ζ : L} (hζ : is_primitive_root ζ n) [field K] [algebra K L] [is_cyclotomic_extension {n} K L] (hirr : irreducible (polynomial.cyclotomic n K)) :
(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ζ : is_primitive_root ζ n) [field K] [algebra K L] [is_cyclotomic_extension {n} K L] (h : 2 < n) (hirr : irreducible (polynomial.cyclotomic n K)) :

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ζ : is_primitive_root ζ n) [field K] [algebra K L] (hn : is_prime_pow n) [is_cyclotomic_extension {n} K L] (hirr : irreducible (polynomial.cyclotomic n K)) (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.pow_sub_one_norm_prime_pow_ne_two {p : ℕ+} {K : Type u} {L : Type v} [field L] {ζ : L} [field K] [algebra K L] {k s : } (hζ : is_primitive_root ζ (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] [algebra K L] {k : } (hζ : is_primitive_root ζ (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] [algebra K L] {k : } (hζ : is_primitive_root ζ (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] [algebra K L] [hpri : fact (nat.prime p)] [hcyc : is_cyclotomic_extension {p} K L] (hζ : is_primitive_root ζ p) (hirr : irreducible (polynomial.cyclotomic p K)) (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] [algebra K L] {k : } (hζ : is_primitive_root ζ (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] [algebra K L] {k : } (hζ : is_primitive_root ζ (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_one_le {p : ℕ+} {K : Type u} {L : Type v} [field L] {ζ : L} [field K] [algebra K L] {k s : } (hζ : is_primitive_root ζ (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 : 1 k) :
(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 1 ≤ k.

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

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

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] [algebra K 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] [algebra K 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] [algebra K L] [hpri : fact (nat.prime p)] [hcyc : is_cyclotomic_extension {p} K L] (hirr : irreducible (polynomial.cyclotomic p K)) (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] [algebra K L] {k : } (hk : 2 k) [is_cyclotomic_extension {2 ^ k} K L] (hirr : irreducible (polynomial.cyclotomic (2 ^ k) K)) :

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.