# Documentation

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

# Primitive roots in cyclotomic fields #

If IsCyclotomicExtension {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 #

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

## Main results #

• IsCyclotomicExtension.zeta_spec: zeta n A B is a primitive n-th root of unity.
• IsCyclotomicExtension.finrank: if Irreducible (cyclotomic n K) (in particular for K = ℚ), then the finrank of a cyclotomic extension is n.totient.
• IsPrimitiveRoot.norm_eq_one: if Irreducible (cyclotomic n K) (in particular for K = ℚ), the norm of a primitive root is 1 if n ≠ 2.
• IsPrimitiveRoot.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.
• IsPrimitiveRoot.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.
• IsPrimitiveRoot.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.
• IsPrimitiveRoot.embeddingsEquivPrimitiveRoots: the equivalence between L →ₐ[K] A and primitiveRoots 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 IsCyclotomicExtension. It is not true in general that it is a root of cyclotomic n B, but this holds if isDomain B and NeZero (↑n : B).

zeta n A B is defined using Exists.choose, 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 IsCyclotomicExtension.zeta (n : ℕ+) (A : Type w) (B : Type z) [] [] [Algebra A B] [] :
B

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

Instances For
@[simp]
theorem IsCyclotomicExtension.zeta_spec (n : ℕ+) (A : Type w) (B : Type z) [] [] [Algebra A B] [] :

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

theorem IsCyclotomicExtension.aeval_zeta (n : ℕ+) (A : Type w) (B : Type z) [] [] [Algebra A B] [] [] [NeZero n] :
↑() () = 0
theorem IsCyclotomicExtension.zeta_isRoot (n : ℕ+) (A : Type w) (B : Type z) [] [] [Algebra A B] [] [] [NeZero n] :
theorem IsCyclotomicExtension.zeta_pow (n : ℕ+) (A : Type w) (B : Type z) [] [] [Algebra A B] [] :
^ n = 1
@[simp]
theorem IsPrimitiveRoot.powerBasis_dim {n : ℕ+} (K : Type u) {L : Type v} [] [] [] [Algebra K L] [] {ζ : L} (hζ : ) :
().dim =
@[simp]
theorem IsPrimitiveRoot.powerBasis_gen {n : ℕ+} (K : Type u) {L : Type v} [] [] [] [Algebra K L] [] {ζ : L} (hζ : ) :
().gen = ζ
noncomputable def IsPrimitiveRoot.powerBasis {n : ℕ+} (K : Type u) {L : Type v} [] [] [] [Algebra K L] [] {ζ : L} (hζ : ) :

The PowerBasis given by a primitive root η.

Instances For
theorem IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_one {n : ℕ+} (K : Type u) {L : Type v} [] [] [] [Algebra K L] [] {ζ : L} (hζ : ) :
().gen Algebra.adjoin K {ζ - 1}
@[simp]
theorem IsPrimitiveRoot.subOnePowerBasis_dim {n : ℕ+} (K : Type u) {L : Type v} [] [] [] [Algebra K L] [] {ζ : L} (hζ : ) :
().dim = Polynomial.natDegree (minpoly K (ζ - 1))
@[simp]
theorem IsPrimitiveRoot.subOnePowerBasis_gen {n : ℕ+} (K : Type u) {L : Type v} [] [] [] [Algebra K L] [] {ζ : L} (hζ : ) :
().gen = ζ - 1
noncomputable def IsPrimitiveRoot.subOnePowerBasis {n : ℕ+} (K : Type u) {L : Type v} [] [] [] [Algebra K L] [] {ζ : L} (hζ : ) :

The PowerBasis given by η - 1.

Instances For
noncomputable def IsPrimitiveRoot.embeddingsEquivPrimitiveRoots {n : ℕ+} {K : Type u} {L : Type v} [] [] [] [Algebra K L] [] {ζ : L} (hζ : ) (C : Type u_1) [] [] [Algebra K C] (hirr : Irreducible ()) :
(L →ₐ[K] C) { x // x primitiveRoots (n) C }

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

Instances For
@[simp]
theorem IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe {n : ℕ+} {K : Type u} {L : Type v} [] [] [] [Algebra K L] [] {ζ : L} (hζ : ) (C : Type u_1) [] [] [Algebra K C] (hirr : Irreducible ()) (φ' : L →ₐ[K] C) :
↑(↑() φ') = φ' ζ
theorem IsCyclotomicExtension.finrank {n : ℕ+} {K : Type u} (L : Type v) [] [] [] [Algebra K L] [] (hirr : Irreducible ()) :

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

theorem IsPrimitiveRoot.norm_eq_neg_one_pow {K : Type u} {L : Type v} [] {ζ : L} [] [Algebra K L] (hζ : ) [] :
↑() ζ = (-1) ^

This mathematically trivial result is complementary to norm_eq_one below.

theorem IsPrimitiveRoot.norm_eq_one {n : ℕ+} {K : Type u} {L : Type v} [] {ζ : L} (hζ : ) [] [Algebra K L] [] [] (hn : n 2) (hirr : Irreducible ()) :
↑() ζ = 1

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

theorem IsPrimitiveRoot.norm_eq_one_of_linearly_ordered {n : ℕ+} {L : Type v} [] {ζ : L} (hζ : ) {K : Type u_1} [Algebra K L] (hodd : Odd n) :
↑() ζ = 1

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

theorem IsPrimitiveRoot.norm_of_cyclotomic_irreducible {n : ℕ+} (A : Type w) (B : Type z) {K : Type u} {L : Type v} [] [] [Algebra A B] [] [] {ζ : L} (hζ : ) [] [Algebra K L] [] [] (hirr : Irreducible ()) :
↑() ζ = if n = 2 then -1 else 1
theorem IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic {n : ℕ+} {K : Type u} {L : Type v} [] {ζ : L} (hζ : ) [] [Algebra K L] [] (h : 2 < n) (hirr : Irreducible ()) :
↑() (ζ - 1) = ↑()

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

theorem IsPrimitiveRoot.sub_one_norm_isPrimePow {n : ℕ+} {K : Type u} {L : Type v} [] {ζ : L} (hζ : ) [] [Algebra K L] (hn : ) [] (hirr : Irreducible ()) (h : n 2) :
↑() (ζ - 1) = ↑()

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

theorem IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp {n : ℕ+} {A : Type w} {K : Type u} [] [] [Algebra K A] [] {ζ : A} [] (hζ : ) (h : Irreducible ()) :
minpoly K (ζ - 1) = Polynomial.comp () (Polynomial.X + 1)
theorem IsPrimitiveRoot.pow_sub_one_norm_prime_pow_ne_two {p : ℕ+} {K : Type u} {L : Type v} [] {ζ : L} [] [Algebra K L] {k : } {s : } (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) [hpri : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)) (hs : s k) (htwo : p ^ (k - s + 1) 2) :
↑() (ζ ^ 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 IsPrimitiveRoot.pow_sub_one_norm_prime_ne_two {p : ℕ+} {K : Type u} {L : Type v} [] {ζ : L} [] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) [hpri : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)) {s : } (hs : s k) (hodd : p 2) :
↑() (ζ ^ 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 IsPrimitiveRoot.sub_one_norm_prime_ne_two {p : ℕ+} {K : Type u} {L : Type v} [] {ζ : L} [] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) [hpri : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)) (h : p 2) :
↑() (ζ - 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 IsPrimitiveRoot.sub_one_norm_prime {p : ℕ+} {K : Type u} {L : Type v} [] {ζ : L} [] [Algebra K L] [hpri : Fact ()] [hcyc : ] (hζ : ) (hirr : Irreducible ()) (h : p 2) :
↑() (ζ - 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 IsPrimitiveRoot.pow_sub_one_norm_two {K : Type u} {L : Type v} [] {ζ : L} [] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) [IsCyclotomicExtension {2 ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ (k + 1)) 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 IsPrimitiveRoot.sub_one_norm_two {K : Type u} {L : Type v} [] {ζ : L} [] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (2 ^ k)) (hk : 2 k) [H : IsCyclotomicExtension {2 ^ k} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ k) 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 IsPrimitiveRoot.pow_sub_one_norm_prime_pow_of_ne_zero {p : ℕ+} {K : Type u} {L : Type v} [] {ζ : L} [] [Algebra K L] {k : } {s : } (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) [hpri : Fact ()] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)) (hs : s k) (hk : k 0) :
↑() (ζ ^ 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 IsCyclotomicExtension.norm_zeta_eq_one {n : ℕ+} {K : Type u} (L : Type v) [] [] [Algebra K L] [] (hn : n 2) (hirr : Irreducible ()) :
↑() () = 1

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

theorem IsCyclotomicExtension.isPrimePow_norm_zeta_sub_one {n : ℕ+} {K : Type u} (L : Type v) [] [] [Algebra K L] (hn : ) [] (hirr : Irreducible ()) (h : n 2) :
↑() ( - 1) = ↑()

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

theorem IsCyclotomicExtension.prime_ne_two_pow_norm_zeta_pow_sub_one {p : ℕ+} {K : Type u} (L : Type v) [] [] [Algebra K L] {k : } [Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)) {s : } (hs : s k) (htwo : p ^ (k - s + 1) 2) :
↑() (IsCyclotomicExtension.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 IsCyclotomicExtension.prime_ne_two_pow_norm_zeta_sub_one {p : ℕ+} {K : Type u} (L : Type v) [] [] [Algebra K L] {k : } [Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)) (h : p 2) :
↑() (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L - 1) = p

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 IsCyclotomicExtension.prime_ne_two_norm_zeta_sub_one {p : ℕ+} {K : Type u} (L : Type v) [] [] [Algebra K L] [Fact ()] [] (hirr : Irreducible ()) (h : p 2) :
↑() ( - 1) = p

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 IsCyclotomicExtension.two_pow_norm_zeta_sub_one {K : Type u} (L : Type v) [] [] [Algebra K L] {k : } (hk : 2 k) [IsCyclotomicExtension {2 ^ k} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ k) K)) :
↑() (IsCyclotomicExtension.zeta (2 ^ 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.