# 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 #

• IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow: if K is a p ^ k-th cyclotomic extension of ℚ, then (adjoin ℤ {ζ}) is the integral closure of ℤ in K.
• IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow: the integral closure of ℤ inside CyclotomicField (p ^ k) ℚ is CyclotomicRing (p ^ k) ℤ ℚ.
• IsCyclotomicExtension.Rat.absdiscr_prime_pow and related results: the absolute discriminant of cyclotomic fields.
theorem IsCyclotomicExtension.Rat.discr_prime_pow_ne_two' {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hk : p ^ (k + 1) 2) :
Algebra.discr .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} [] [] {ζ : K} [hp : Fact ()] [] (hζ : ) (hodd : p 2) :
Algebra.discr .basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)
theorem IsCyclotomicExtension.Rat.discr_prime_pow' {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
Algebra.discr .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} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
∃ (u : ) (n : ), Algebra.discr .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'.

theorem IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :

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

theorem IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :

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

@[simp]
theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) (a : ) :
.adjoinEquivRingOfIntegers.symm a = (IsIntegralClosure.lift (()) K) a
@[simp]
theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) (a : ()) :
noncomputable def IsPrimitiveRoot.adjoinEquivRingOfIntegers {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (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
• .adjoinEquivRingOfIntegers = let x := ;
Instances For
instance IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegers {p : ℕ+} {k : } {K : Type u} [] [] [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] :

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

Equations
• =
noncomputable def IsPrimitiveRoot.integralPowerBasis {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : 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} [] {ζ : K} {k : ℕ+} (hζ : ) :

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

Equations
• .toInteger = ζ,
Instances For
theorem IsPrimitiveRoot.coe_toInteger {K : Type u} [] {ζ : K} {k : ℕ+} (hζ : ) :
.toInteger = ζ
theorem IsPrimitiveRoot.finite_quotient_toInteger_sub_one {K : Type u} [] {ζ : K} [] {k : ℕ+} (hk : 1 < k) (hζ : ) :
Finite ( Ideal.span {.toInteger - 1})

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

theorem IsPrimitiveRoot.card_quotient_toInteger_sub_one {K : Type u} [] {ζ : K} [] {k : ℕ+} (hk : 1 < k) (hζ : ) :
Nat.card ( Ideal.span {.toInteger - 1}) = ( (.toInteger - 1)).natAbs

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.

theorem IsPrimitiveRoot.toInteger_isPrimitiveRoot {K : Type u} [] {ζ : K} {k : ℕ+} (hζ : ) :
IsPrimitiveRoot .toInteger k
@[simp]
theorem IsPrimitiveRoot.integralPowerBasis_gen {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
.integralPowerBasis.gen = .toInteger
@[simp]
theorem IsPrimitiveRoot.integralPowerBasis_dim {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
.integralPowerBasis.dim = (p ^ k).totient
@[simp]
theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers'_apply {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) (a : ()) :
@[simp]
theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers'_symm_apply {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) (a : ) :
.adjoinEquivRingOfIntegers'.symm a = (IsIntegralClosure.lift (()) K) a
noncomputable def IsPrimitiveRoot.adjoinEquivRingOfIntegers' {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :

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
instance IsCyclotomicExtension.ring_of_integers' {p : ℕ+} {K : Type u} [] [] [hp : Fact ()] [] :

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

Equations
• =
noncomputable def IsPrimitiveRoot.integralPowerBasis' {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :

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

Equations
• .integralPowerBasis' = .integralPowerBasis
Instances For
@[simp]
theorem IsPrimitiveRoot.integralPowerBasis'_gen {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :
.integralPowerBasis'.gen = .toInteger
@[simp]
theorem IsPrimitiveRoot.power_basis_int'_dim {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :
.integralPowerBasis'.dim = (p).totient
noncomputable def IsPrimitiveRoot.subOneIntegralPowerBasis {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : 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} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
.subOneIntegralPowerBasis.gen = ζ - 1,
noncomputable def IsPrimitiveRoot.subOneIntegralPowerBasis' {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :

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

Equations
• .subOneIntegralPowerBasis' = .subOneIntegralPowerBasis
Instances For
@[simp]
theorem IsPrimitiveRoot.subOneIntegralPowerBasis'_gen {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :
.subOneIntegralPowerBasis'.gen = .toInteger - 1
theorem IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : 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} [] [] {ζ : K} [IsCyclotomicExtension {2 ^ (k + 1)} K] (hζ : 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} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : 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} [] [] {ζ : K} [hp : Fact ()] [h : ] (hζ : ) :
Prime (.toInteger - 1)

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

theorem IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) :
Prime .subOneIntegralPowerBasis.gen
theorem IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [] (hζ : ) :
Prime .subOneIntegralPowerBasis'.gen
theorem IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : } (hs : s k) (htwo : p ^ (k - s + 1) 2) :
(.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} [] [] {ζ : K} [IsCyclotomicExtension {2 ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) :
(.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} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : } (hs : s k) (hodd : p 2) :
(.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_prime_ne_two {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
(.toInteger - 1) = p

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

theorem IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two' {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) (h : p 2) :
(.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} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (htwo : p ^ (k + 1) 2) :
Prime ( (.toInteger - 1))

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} [] [] {ζ : K} [hp : Fact ()] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
Prime ( (.toInteger - 1))

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} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) (hodd : p 2) :
Prime ( (.toInteger - 1))

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} [] [] {ζ : K} [hp : Fact ()] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : 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} [] [] {ζ : K} [hp : Fact ()] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : 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} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) (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.finite_quotient_span_sub_one {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) :
Finite ( Ideal.span {.toInteger - 1})
theorem IsPrimitiveRoot.finite_quotient_span_sub_one' {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :
Finite ( Ideal.span {.toInteger - 1})
theorem IsPrimitiveRoot.toInteger_sub_one_dvd_prime {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : 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} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :
.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} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
¬.toInteger - 1 2

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

theorem IsCyclotomicExtension.Rat.absdiscr_prime_pow (p : ℕ+) (k : ) (K : Type u) [] [] [hp : Fact ()] [IsCyclotomicExtension {p ^ k} 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) [] [] [hp : Fact ()] [IsCyclotomicExtension {p ^ (k + 1)} 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) [] [] [hp : Fact ()] [] :
= (-1) ^ ((p - 1) / 2) * p ^ (p - 2)

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