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

• 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) ℤ ℚ.
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) ^ (Nat.totient ↑(p ^ (k + 1)) / 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) ^ (Nat.totient ↑(p ^ k) / 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_apply {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) (a : { x // x }) :
= ↑(IsIntegralClosure.lift { x // } K (_ : Algebra.IsIntegral { x // x })) a
@[simp]
theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) (a : { x // }) :
= ↑(IsIntegralClosure.lift { x // x } K (_ : Algebra.IsIntegral { x // })) a
noncomputable def IsPrimitiveRoot.adjoinEquivRingOfIntegers {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
{ x // x } ≃ₐ[] { x // }

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 ℚ.

Instances For
instance IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegers {p : ℕ+} {k : } {K : Type u} [] [] [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] :
IsCyclotomicExtension {p ^ k} { x // }

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} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
PowerBasis { x // }

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

Instances For
@[simp]
theorem IsPrimitiveRoot.integralPowerBasis_gen {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
().gen = { val := ζ, property := (_ : ) }
@[simp]
theorem IsPrimitiveRoot.integralPowerBasis_dim {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
().dim = Nat.totient ↑(p ^ k)
@[simp]
theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers'_apply {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) (a : { x // x }) :
= ↑(IsIntegralClosure.lift { x // } K (_ : Algebra.IsIntegral { x // x })) a
@[simp]
theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers'_symm_apply {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) (a : { x // }) :
= ↑(IsIntegralClosure.lift { x // x } K (_ : Algebra.IsIntegral { x // })) a
noncomputable def IsPrimitiveRoot.adjoinEquivRingOfIntegers' {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :
{ x // x } ≃ₐ[] { x // }

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

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.

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

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

Instances For
@[simp]
theorem IsPrimitiveRoot.integralPowerBasis'_gen {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :
().gen = { val := ζ, property := (_ : ) }
@[simp]
theorem IsPrimitiveRoot.power_basis_int'_dim {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :
().dim =
noncomputable def IsPrimitiveRoot.subOneIntegralPowerBasis {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
PowerBasis { x // }

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

Instances For
@[simp]
theorem IsPrimitiveRoot.subOneIntegralPowerBasis_gen {p : ℕ+} {k : } {K : Type u} [] [] {ζ : K} [hp : Fact ()] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
= { val := ζ - 1, property := (_ : ) }
noncomputable def IsPrimitiveRoot.subOneIntegralPowerBasis' {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :
PowerBasis { x // }

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

Instances For
@[simp]
theorem IsPrimitiveRoot.subOneIntegralPowerBasis'_gen {p : ℕ+} {K : Type u} [] [] {ζ : K} [hp : Fact ()] [hcycl : ] (hζ : ) :
= { val := ζ - 1, property := (_ : ) }