Ring of integers of cyclotomic fields #
We gather results about cyclotomic extensions of ℚ. In particular, we compute the ring of
integers of a cyclotomic extension of ℚ.
Main results #
IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton: ifKis a cyclotomic extension ofℚ, thenadjoin ℤ {ζ}is the integral closure ofℤinK.IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure: the integral closure ofℤinsideCyclotomicField n ℚisCyclotomicRing n ℤ ℚ.IsCyclotomicExtension.Rat.discrand related results: the absolute discriminant of cyclotomic fields.
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'.
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 integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a p ^ k
cyclotomic extension of ℚ.
Equations
Instances For
Abbreviation to see a primitive root of unity as a member of the ring of integers.
Instances For
𝓞 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.
The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a p ^ k cyclotomic
extension of ℚ.
Equations
Instances For
ζ - 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.
ζ - 1 is prime if ζ is a primitive 2 ^ (k + 1)-th root of unity.
See zeta_sub_one_prime for a general statement.
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.
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 ^ (k - s + 1) ≠ 2.
The norm, relative to ℤ, of ζ ^ 2 ^ k - 1 in a 2 ^ (k + 1)-th cyclotomic extension of ℚ
is (-2) ^ 2 ^ k.
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.
The norm, relative to ℤ, of ζ - 1 in a 2 ^ (k + 2)-th cyclotomic extension of ℚ is 2.
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.
The norm, relative to ℤ, of ζ - 1 in a p-th cyclotomic extension of ℚ is p if
p ≠ 2.
The norm, relative to ℤ, of ζ - 1 in a p ^ (k + 1)-th cyclotomic extension of ℚ is
a prime if p ^ (k + 1) ≠ 2.
The norm, relative to ℤ, of ζ - 1 in a p ^ (k + 1)-th cyclotomic extension of ℚ is
a prime if p ≠ 2.
The norm, relative to ℤ, of ζ - 1 in a p-th cyclotomic extension of ℚ is a prime if
p ≠ 2.
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.
In a p ^ (k + 1)-th cyclotomic extension of ℚ , we have that ζ is not congruent to an
integer modulo p if p ≠ 2.
In a p-th cyclotomic extension of ℚ , we have that ζ is not congruent to an
integer modulo p if p ≠ 2.
In a p ^ (k + 1)-th cyclotomic extension of ℚ, we have that
ζ - 1 divides p in 𝓞 K.
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.
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.
Alias of IsCyclotomicExtension.Rat.discr_prime_pow.
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.
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.
Alias of IsCyclotomicExtension.Rat.discr_prime_pow_succ.
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.
Alias of IsCyclotomicExtension.Rat.discr_prime.
We compute the absolute discriminant of a p-th cyclotomic field where p is prime.
Computes the absolute discriminant of the n-th cyclotomic field.
The integral closure of ℤ inside CyclotomicField n ℚ is CyclotomicRing n ℤ ℚ.
The algebra isomorphism adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K), where ζ is a primitive n-th root of
unity and K is a n-th cyclotomic extension of ℚ.
Equations
Instances For
The ring of integers of a n-th cyclotomic extension of ℚ is a cyclotomic extension.
Alias of IsCyclotomicExtension.ringOfIntegers.
The ring of integers of a n-th cyclotomic extension of ℚ is a cyclotomic extension.
The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a n-th
cyclotomic extension of ℚ.
Equations
Instances For
The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a cyclotomic
extension of ℚ.
Equations
Instances For
Alias of IsPrimitiveRoot.integralPowerBasis.
The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a n-th
cyclotomic extension of ℚ.
Instances For
Alias of IsPrimitiveRoot.integralPowerBasis_gen.
Alias of IsPrimitiveRoot.integralPowerBasis_dim.
Alias of IsPrimitiveRoot.subOneIntegralPowerBasis.
The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a cyclotomic
extension of ℚ.