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 #

Main results #

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) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} 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.

Equations
Instances For
    @[simp]

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

    @[simp]
    theorem IsPrimitiveRoot.powerBasis_dim {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
    @[simp]
    theorem IsPrimitiveRoot.powerBasis_gen {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
    noncomputable def IsPrimitiveRoot.powerBasis {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :

    The PowerBasis given by a primitive root η.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem IsPrimitiveRoot.subOnePowerBasis_dim {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
      @[simp]
      theorem IsPrimitiveRoot.subOnePowerBasis_gen {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
      noncomputable def IsPrimitiveRoot.subOnePowerBasis {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :

      The PowerBasis given by η - 1.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        noncomputable def IsPrimitiveRoot.embeddingsEquivPrimitiveRoots {n : ℕ+} {K : Type u} {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) (C : Type u_1) [CommRing C] [IsDomain C] [Algebra K C] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) :
        (L →ₐ[K] C) { x // x primitiveRoots (n) C }

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe {n : ℕ+} {K : Type u} {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) (C : Type u_1) [CommRing C] [IsDomain C] [Algebra K C] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) (φ' : L →ₐ[K] C) :
          ↑(↑(IsPrimitiveRoot.embeddingsEquivPrimitiveRoots C hirr) φ') = φ' ζ

          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} [CommRing L] {ζ : L} [Field K] [Algebra K L] (hζ : IsPrimitiveRoot ζ 2) [IsDomain L] :

          This mathematically trivial result is complementary to norm_eq_one below.

          theorem IsPrimitiveRoot.norm_eq_one {n : ℕ+} {K : Type u} {L : Type v} [CommRing L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) [Field K] [Algebra K L] [IsDomain L] [IsCyclotomicExtension {n} K L] (hn : n 2) (hirr : Irreducible (Polynomial.cyclotomic (n) K)) :
          ↑(Algebra.norm K) ζ = 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} [CommRing L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) {K : Type u_1} [LinearOrderedField K] [Algebra K L] (hodd : Odd n) :
          ↑(Algebra.norm K) ζ = 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} [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [CommRing L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) [Field K] [Algebra K L] [IsDomain L] [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) :
          ↑(Algebra.norm K) ζ = if n = 2 then -1 else 1
          theorem IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic {n : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) [Field K] [Algebra K L] [IsCyclotomicExtension {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 IsPrimitiveRoot.sub_one_norm_isPrimePow {n : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) [Field K] [Algebra K L] (hn : IsPrimePow n) [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) (h : n 2) :
          ↑(Algebra.norm K) (ζ - 1) = ↑(Nat.minFac n)

          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} [CommRing A] [Field K] [Algebra K A] [IsDomain A] {ζ : A} [IsCyclotomicExtension {n} K A] (hζ : IsPrimitiveRoot ζ n) (h : Irreducible (Polynomial.cyclotomic (n) K)) :
          minpoly K (ζ - 1) = Polynomial.comp (Polynomial.cyclotomic (n) K) (Polynomial.X + 1)
          theorem IsPrimitiveRoot.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ζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {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 IsPrimitiveRoot.pow_sub_one_norm_prime_ne_two {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {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 IsPrimitiveRoot.sub_one_norm_prime_ne_two {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {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 IsPrimitiveRoot.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 : IsCyclotomicExtension {p} K L] (hζ : IsPrimitiveRoot ζ 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 IsPrimitiveRoot.pow_sub_one_norm_two {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) [IsCyclotomicExtension {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 IsPrimitiveRoot.sub_one_norm_two {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (2 ^ k)) (hk : 2 k) [H : IsCyclotomicExtension {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 IsPrimitiveRoot.pow_sub_one_norm_prime_pow_of_ne_zero {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } {s : } (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {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 IsCyclotomicExtension.norm_zeta_eq_one {n : ℕ+} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {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.

          theorem IsCyclotomicExtension.isPrimePow_norm_zeta_sub_one {n : ℕ+} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (hn : IsPrimePow n) [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) (h : n 2) :

          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) [Field K] [Field L] [Algebra K L] {k : } [Fact (Nat.Prime p)] [IsCyclotomicExtension {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) (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) [Field K] [Field L] [Algebra K L] {k : } [Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)) (h : p 2) :
          ↑(Algebra.norm K) (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) [Field K] [Field L] [Algebra K L] [Fact (Nat.Prime p)] [IsCyclotomicExtension {p} K L] (hirr : Irreducible (Polynomial.cyclotomic (p) K)) (h : p 2) :
          ↑(Algebra.norm K) (IsCyclotomicExtension.zeta p K L - 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) [Field K] [Field L] [Algebra K L] {k : } (hk : 2 k) [IsCyclotomicExtension {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.