Documentation

Mathlib.NumberTheory.Cyclotomic.Rat

Ring of integers of p ^ n-th cyclotomic fields #

We gather results about cyclotomic extensions of . In particular, we compute the ring of integers of a p ^ n-th cyclotomic extension of .

Main results #

theorem IsCyclotomicExtension.Rat.discr_prime_pow_ne_two' {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) (hk : p ^ (k + 1) 2) :
Algebra.discr (IsPrimitiveRoot.subOnePowerBasis ).basis = (-1) ^ ((p ^ (k + 1)).totient / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

The discriminant of the power basis given by ζ - 1.

theorem IsCyclotomicExtension.Rat.discr_odd_prime' {p : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p} K] ( : IsPrimitiveRoot ζ p) (hodd : p 2) :
Algebra.discr (IsPrimitiveRoot.subOnePowerBasis ).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)
theorem IsCyclotomicExtension.Rat.discr_prime_pow' {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} K] ( : IsPrimitiveRoot ζ (p ^ k)) :
Algebra.discr (IsPrimitiveRoot.subOnePowerBasis ).basis = (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

The discriminant of the power basis given by ζ - 1. Beware that in the cases p ^ k = 1 and p ^ k = 2 the formula uses 1 / 2 = 0 and 0 - 1 = 0. It is useful only to have a uniform result. See also IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow'.

theorem IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow' {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} K] ( : IsPrimitiveRoot ζ (p ^ k)) :
∃ (u : ˣ) (n : ), Algebra.discr (IsPrimitiveRoot.subOnePowerBasis ).basis = u * p ^ n

If p is a prime and IsCyclotomicExtension {p ^ k} K L, then there are u : ℤˣ and n : ℕ such that the discriminant of the power basis given by ζ - 1 is u * p ^ n. Often this is enough and less cumbersome to use than IsCyclotomicExtension.Rat.discr_prime_pow'.

If K is a p ^ k-th cyclotomic extension of , then (adjoin ℤ {ζ}) is the integral closure of in K.

The integral closure of inside CyclotomicField (p ^ k) ℚ is CyclotomicRing (p ^ k) ℤ ℚ.

The algebra isomorphism adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K), where ζ is a primitive p ^ k-th root of unity and K is a p ^ k-th cyclotomic extension of .

Equations
    Instances For

      The ring of integers of a p ^ k-th cyclotomic extension of is a cyclotomic extension.

      noncomputable def IsPrimitiveRoot.integralPowerBasis {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} K] ( : IsPrimitiveRoot ζ (p ^ k)) :

      The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a p ^ k cyclotomic extension of .

      Equations
        Instances For
          @[reducible, inline]
          abbrev IsPrimitiveRoot.toInteger {K : Type u} [Field K] {ζ : K} {k : } [NeZero k] ( : IsPrimitiveRoot ζ k) :

          Abbreviation to see a primitive root of unity as a member of the ring of integers.

          Equations
            Instances For
              theorem IsPrimitiveRoot.coe_toInteger {K : Type u} [Field K] {ζ : K} {k : } [NeZero k] ( : IsPrimitiveRoot ζ k) :
              .toInteger = ζ

              𝓞 K ⧸ Ideal.span {ζ - 1} is finite.

              We have that 𝓞 K ⧸ Ideal.span {ζ - 1} has cardinality equal to the norm of ζ - 1.

              See the results below to compute this norm in various cases.

              @[simp]
              theorem IsPrimitiveRoot.integralPowerBasis_gen {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ k} K] ( : IsPrimitiveRoot ζ (p ^ k)) :
              @[simp]
              theorem IsPrimitiveRoot.integralPowerBasis_dim {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ k} K] ( : IsPrimitiveRoot ζ (p ^ k)) :

              The algebra isomorphism adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K), where ζ is a primitive p-th root of unity and K is a p-th cyclotomic extension of .

              Equations
                Instances For

                  The ring of integers of a p-th cyclotomic extension of is a cyclotomic extension.

                  noncomputable def IsPrimitiveRoot.integralPowerBasis' {p : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} K] ( : IsPrimitiveRoot ζ p) :

                  The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a p-th cyclotomic extension of .

                  Equations
                    Instances For
                      @[simp]
                      theorem IsPrimitiveRoot.integralPowerBasis'_gen {p : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} K] ( : IsPrimitiveRoot ζ p) :
                      @[simp]
                      theorem IsPrimitiveRoot.power_basis_int'_dim {p : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} K] ( : IsPrimitiveRoot ζ p) :
                      noncomputable def IsPrimitiveRoot.subOneIntegralPowerBasis {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} K] ( : IsPrimitiveRoot ζ (p ^ k)) :

                      The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a p ^ k cyclotomic extension of .

                      Equations
                        Instances For
                          @[simp]
                          theorem IsPrimitiveRoot.subOneIntegralPowerBasis_gen {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} K] ( : IsPrimitiveRoot ζ (p ^ k)) :

                          The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a p-th cyclotomic extension of .

                          Equations
                            Instances For
                              theorem IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
                              Prime (.toInteger - 1)

                              ζ - 1 is prime if p ≠ 2 and ζ is a primitive p ^ (k + 1)-th root of unity. See zeta_sub_one_prime for a general statement.

                              theorem IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow {k : } {K : Type u} [Field K] {ζ : K} [CharZero K] [IsCyclotomicExtension {2 ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (2 ^ (k + 1))) :
                              Prime (.toInteger - 1)

                              ζ - 1 is prime if ζ is a primitive 2 ^ (k + 1)-th root of unity. See zeta_sub_one_prime for a general statement.

                              theorem IsPrimitiveRoot.zeta_sub_one_prime {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) :
                              Prime (.toInteger - 1)

                              ζ - 1 is prime if ζ is a primitive p ^ (k + 1)-th root of unity.

                              theorem IsPrimitiveRoot.zeta_sub_one_prime' {p : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [h : IsCyclotomicExtension {p} K] ( : IsPrimitiveRoot ζ p) :
                              Prime (.toInteger - 1)

                              ζ - 1 is prime if ζ is a primitive p-th root of unity.

                              theorem IsPrimitiveRoot.norm_toInteger_sub_one_eq_one {K : Type u} [Field K] {ζ : K} [CharZero K] {n : } [IsCyclotomicExtension {n} K] ( : IsPrimitiveRoot ζ n) (h₁ : 2 < n) (h₂ : ∀ {p : }, Nat.Prime p∀ (k : ), p ^ k n) :
                              have this := ; (Algebra.norm ) (.toInteger - 1) = 1

                              The norm, relative to , of ζ - 1 in a n-th cyclotomic extension of where n is not a power of a prime number is 1.

                              theorem IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : } (hs : s k) (htwo : p ^ (k - s + 1) 2) :
                              (Algebra.norm ) (.toInteger ^ p ^ s - 1) = p ^ p ^ s

                              The norm, relative to , of ζ ^ p ^ s - 1 in a p ^ (k + 1)-th cyclotomic extension of is p ^ p ^ sifs ≤ kandp ^ (k - s + 1) ≠ 2`.

                              theorem IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two {k : } {K : Type u} [Field K] {ζ : K} [CharZero K] [IsCyclotomicExtension {2 ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (2 ^ (k + 1))) :
                              (Algebra.norm ) (.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

                              The norm, relative to , of ζ ^ 2 ^ k - 1 in a 2 ^ (k + 1)-th cyclotomic extension of is (-2) ^ 2 ^ k.

                              theorem IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : } (hs : s k) (hodd : p 2) :
                              (Algebra.norm ) (.toInteger ^ p ^ s - 1) = p ^ p ^ s

                              The norm, relative to , of ζ ^ p ^ s - 1 in a p ^ (k + 1)-th cyclotomic extension of is p ^ p ^ s if s ≤ k and p ≠ 2.

                              theorem IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow {k : } {K : Type u_1} [Field K] {ζ : K} [CharZero K] [IsCyclotomicExtension {2 ^ (k + 2)} K] ( : IsPrimitiveRoot ζ (2 ^ (k + 2))) :

                              The norm, relative to , of ζ - 1 in a 2 ^ (k + 2)-th cyclotomic extension of is 2.

                              theorem IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
                              (Algebra.norm ) (.toInteger - 1) = p

                              The norm, relative to , of ζ - 1 in a p ^ (k + 1)-th cyclotomic extension of is p if p ≠ 2.

                              The norm, relative to , of ζ - 1 in a 2-th cyclotomic extension of is -2.

                              theorem IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two' {p : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} K] ( : IsPrimitiveRoot ζ p) (h : p 2) :
                              (Algebra.norm ) (.toInteger - 1) = p

                              The norm, relative to , of ζ - 1 in a p-th cyclotomic extension of is p if p ≠ 2.

                              theorem IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) (htwo : p ^ (k + 1) 2) :

                              The norm, relative to , of ζ - 1 in a p ^ (k + 1)-th cyclotomic extension of is a prime if p ^ (k + 1) ≠ 2.

                              theorem IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :

                              The norm, relative to , of ζ - 1 in a p ^ (k + 1)-th cyclotomic extension of is a prime if p ≠ 2.

                              theorem IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two' {p : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} K] ( : IsPrimitiveRoot ζ p) (hodd : p 2) :

                              The norm, relative to , of ζ - 1 in a p-th cyclotomic extension of is a prime if p ≠ 2.

                              theorem IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) (htwo : p ^ (k + 1) 2) :
                              ¬∃ (n : ), p .toInteger - n

                              In a p ^ (k + 1)-th cyclotomic extension of , we have that ζ is not congruent to an integer modulo p if p ^ (k + 1) ≠ 2.

                              theorem IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
                              ¬∃ (n : ), p .toInteger - n

                              In a p ^ (k + 1)-th cyclotomic extension of , we have that ζ is not congruent to an integer modulo p if p ≠ 2.

                              theorem IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two' {p : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} K] ( : IsPrimitiveRoot ζ p) (hodd : p 2) :
                              ¬∃ (n : ), p .toInteger - n

                              In a p-th cyclotomic extension of , we have that ζ is not congruent to an integer modulo p if p ≠ 2.

                              theorem IsPrimitiveRoot.toInteger_sub_one_dvd_prime {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) :
                              .toInteger - 1 p

                              In a p ^ (k + 1)-th cyclotomic extension of , we have that ζ - 1 divides p in 𝓞 K.

                              theorem IsPrimitiveRoot.toInteger_sub_one_dvd_prime' {p : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} K] ( : IsPrimitiveRoot ζ p) :
                              .toInteger - 1 p

                              In a p-th cyclotomic extension of , we have that ζ - 1 divides p in 𝓞 K.

                              theorem IsPrimitiveRoot.toInteger_sub_one_not_dvd_two {p k : } {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} K] ( : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
                              ¬.toInteger - 1 2

                              We have that hζ.toInteger - 1 does not divide 2.

                              theorem IsPrimitiveRoot.prime_dvd_of_dvd_norm_sub_one {n : } (hn : 2 n) {K : Type u_1} [Field K] [NumberField K] {ζ : K} {p : } [hF : Fact (Nat.Prime p)] ( : IsPrimitiveRoot ζ n) (hp : have x := ; p (Algebra.norm ) (.toInteger - 1)) :
                              p n

                              Let ζ be a primitive root of unity of order n with 2 ≤ n. Any prime number that divides the norm, relative to , of ζ - 1 divides also n.

                              theorem IsCyclotomicExtension.Rat.absdiscr_prime_pow (p k : ) (K : Type u) [Field K] [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} K] :
                              NumberField.discr K = (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

                              We compute the absolute discriminant of a p ^ k-th cyclotomic field. Beware that in the cases p ^ k = 1 and p ^ k = 2 the formula uses 1 / 2 = 0 and 0 - 1 = 0. See also the results below.

                              theorem IsCyclotomicExtension.Rat.absdiscr_prime_pow_succ (p k : ) (K : Type u) [Field K] [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} K] :
                              NumberField.discr K = (-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

                              We compute the absolute discriminant of a p ^ (k + 1)-th cyclotomic field. Beware that in the case p ^ k = 2 the formula uses 1 / 2 = 0. See also the results below.

                              theorem IsCyclotomicExtension.Rat.absdiscr_prime (p : ) (K : Type u) [Field K] [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p} K] :
                              NumberField.discr K = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)

                              We compute the absolute discriminant of a p-th cyclotomic field where p is prime.