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: ifKis ap ^ k-th cyclotomic extension ofℚ, then(adjoin ℤ {ζ})is the integral closure ofℤinK.IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow: the integral closure ofℤinsideCyclotomicField (p ^ k) ℚisCyclotomicRing (p ^ k) ℤ ℚ.IsCyclotomicExtension.Rat.absdiscr_prime_powand related results: the absolute discriminant of cyclotomic fields.
The discriminant of the power basis given by ζ - 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'.
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
- hζ.adjoinEquivRingOfIntegers = let x := ⋯; IsIntegralClosure.equiv ℤ (↥(Algebra.adjoin ℤ {ζ})) K (NumberField.RingOfIntegers K)
Instances For
The ring of integers of a p ^ k-th cyclotomic extension of ℚ is a cyclotomic extension.
Equations
- ⋯ = ⋯
The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a p ^ k
cyclotomic extension of ℚ.
Equations
- hζ.integralPowerBasis = (Algebra.adjoin.powerBasis' ⋯).map hζ.adjoinEquivRingOfIntegers
Instances For
Abbreviation to see a primitive root of unity as a member of the ring of integers.
Equations
- hζ.toInteger = ⟨ζ, ⋯⟩
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 algebra isomorphism adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K), where ζ is a primitive p-th root of
unity and K is a p-th cyclotomic extension of ℚ.
Equations
- hζ.adjoinEquivRingOfIntegers' = ⋯.adjoinEquivRingOfIntegers
Instances For
The ring of integers of a p-th cyclotomic extension of ℚ is a cyclotomic extension.
Equations
- ⋯ = ⋯
The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a p-th
cyclotomic extension of ℚ.
Equations
- hζ.integralPowerBasis' = ⋯.integralPowerBasis
Instances For
The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a p ^ k cyclotomic
extension of ℚ.
Equations
- hζ.subOneIntegralPowerBasis = hζ.integralPowerBasis.ofGenMemAdjoin' ⋯ ⋯
Instances For
The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a p-th cyclotomic
extension of ℚ.
Equations
- hζ.subOneIntegralPowerBasis' = ⋯.subOneIntegralPowerBasis
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.
ζ - 1 is prime if ζ is a primitive p ^ (k + 1)-th root of unity.
ζ - 1 is prime if ζ is a primitive p-th root of unity.
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`.
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 p ^ (k + 1)-th cyclotomic extension of ℚ is
p if p ≠ 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.
In a p-th cyclotomic extension of ℚ, we have that ζ - 1 divides p in 𝓞 K.
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.
We compute the absolute discriminant of a p-th cyclotomic field where p is prime.