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
- IsPrimitiveRoot.adjoinEquivRingOfIntegers hζ = 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
Instances For
Abbreviation to see a primitive root of unity as a member of the ring of integers.
Equations
- IsPrimitiveRoot.toInteger hζ = { val := ζ, property := ⋯ }
Instances For
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.
Equations
- ⋯ = ⋯
The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a p-th
cyclotomic extension of ℚ.
Instances For
The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a p ^ k cyclotomic
extension of ℚ.
Equations
Instances For
The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a p-th cyclotomic
extension of ℚ.
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.
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.