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} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hk : p ^ (k + 1) ≠ 2) : Algebra.discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).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} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ ↑p) (hodd : p ≠ 2) : Algebra.discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑((-1) ^ ((↑p - 1) / 2)) * ↑↑(p ^ (↑p - 2))

theorem IsCyclotomicExtension.Rat.discr_prime_pow' {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : Algebra.discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).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} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : ∃ u n, Algebra.discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).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} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : IsIntegralClosure { x // x ∈ Algebra.adjoin ℤ {ζ} } ℤ 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} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ ↑p) : IsIntegralClosure { x // x ∈ Algebra.adjoin ℤ {ζ} } ℤ K

theorem IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow {p : ℕ+} {k : ℕ} [hp : Fact (Nat.Prime ↑p)] : IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)

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

theorem IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime {p : ℕ+} [hp : Fact (Nat.Prime ↑p)] : IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ)

@[simp]

theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) (a : { x // x ∈ Algebra.adjoin ℤ {ζ} }) : ↑(IsPrimitiveRoot.adjoinEquivRingOfIntegers hζ) a = ↑(IsIntegralClosure.lift { x // x ∈ NumberField.ringOfIntegers K } K (_ : Algebra.IsIntegral ℤ { x // x ∈ Algebra.adjoin ℤ {ζ} })) a

@[simp]

theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) (a : { x // x ∈ NumberField.ringOfIntegers K }) : ↑(AlgEquiv.symm (IsPrimitiveRoot.adjoinEquivRingOfIntegers hζ)) a = ↑(IsIntegralClosure.lift { x // x ∈ Algebra.adjoin ℤ {ζ} } K (_ : Algebra.IsIntegral ℤ { x // x ∈ NumberField.ringOfIntegers K })) a

noncomputable def IsPrimitiveRoot.adjoinEquivRingOfIntegers {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : { x // x ∈ Algebra.adjoin ℤ {ζ} } ≃ₐ[ℤ] { x // x ∈ NumberField.ringOfIntegers 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

• One or more equations did not get rendered due to their size.

instance IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegers {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p ^ k} ℚ K] : IsCyclotomicExtension {p ^ k} ℤ { x // x ∈ NumberField.ringOfIntegers K }

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

Equations

• @IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegers = @IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegers.proof_1

noncomputable def IsPrimitiveRoot.integralPowerBasis {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : PowerBasis ℤ { x // x ∈ NumberField.ringOfIntegers K }

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

Equations

• IsPrimitiveRoot.integralPowerBasis hζ = PowerBasis.map (Algebra.adjoin.powerBasis' (_ : IsIntegral ℤ ζ)) (IsPrimitiveRoot.adjoinEquivRingOfIntegers hζ)

@[simp]

theorem IsPrimitiveRoot.integralPowerBasis_gen {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : (IsPrimitiveRoot.integralPowerBasis hζ).gen = { val := ζ, property := (_ : IsIntegral ℤ ζ) }

@[simp]

theorem IsPrimitiveRoot.integralPowerBasis_dim {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : (IsPrimitiveRoot.integralPowerBasis hζ).dim = Nat.totient ↑(p ^ k)

@[simp]

theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers'_apply {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ ↑p) (a : { x // x ∈ Algebra.adjoin ℤ {ζ} }) : ↑(IsPrimitiveRoot.adjoinEquivRingOfIntegers' hζ) a = ↑(IsIntegralClosure.lift { x // x ∈ NumberField.ringOfIntegers K } K (_ : Algebra.IsIntegral ℤ { x // x ∈ Algebra.adjoin ℤ {ζ} })) a

@[simp]

theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers'_symm_apply {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ ↑p) (a : { x // x ∈ NumberField.ringOfIntegers K }) : ↑(AlgEquiv.symm (IsPrimitiveRoot.adjoinEquivRingOfIntegers' hζ)) a = ↑(IsIntegralClosure.lift { x // x ∈ Algebra.adjoin ℤ {ζ} } K (_ : Algebra.IsIntegral ℤ { x // x ∈ NumberField.ringOfIntegers K })) a

noncomputable def IsPrimitiveRoot.adjoinEquivRingOfIntegers' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ ↑p) : { x // x ∈ Algebra.adjoin ℤ {ζ} } ≃ₐ[ℤ] { x // x ∈ NumberField.ringOfIntegers K }

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

Equations

• IsPrimitiveRoot.adjoinEquivRingOfIntegers' hζ = IsPrimitiveRoot.adjoinEquivRingOfIntegers (_ : IsPrimitiveRoot ζ ↑(p ^ 1))

instance IsCyclotomicExtension.ring_of_integers' {p : ℕ+} {K : Type u} [Field K] [CharZero K] [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p} ℚ K] : IsCyclotomicExtension {p} ℤ { x // x ∈ NumberField.ringOfIntegers K }

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

Equations

• @IsCyclotomicExtension.ring_of_integers' = @IsCyclotomicExtension.ring_of_integers'.proof_1

noncomputable def IsPrimitiveRoot.integralPowerBasis' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ ↑p) : PowerBasis ℤ { x // x ∈ NumberField.ringOfIntegers K }

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

Equations

• IsPrimitiveRoot.integralPowerBasis' hζ = IsPrimitiveRoot.integralPowerBasis (_ : IsPrimitiveRoot ζ ↑(p ^ 1))

@[simp]

theorem IsPrimitiveRoot.integralPowerBasis'_gen {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ ↑p) : (IsPrimitiveRoot.integralPowerBasis' hζ).gen = { val := ζ, property := (_ : IsIntegral ℤ ζ) }

@[simp]

theorem IsPrimitiveRoot.power_basis_int'_dim {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ ↑p) : (IsPrimitiveRoot.integralPowerBasis' hζ).dim = Nat.totient ↑p

noncomputable def IsPrimitiveRoot.subOneIntegralPowerBasis {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : PowerBasis ℤ { x // x ∈ NumberField.ringOfIntegers K }

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsPrimitiveRoot.subOneIntegralPowerBasis_gen {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : (IsPrimitiveRoot.subOneIntegralPowerBasis hζ).gen = { val := ζ - 1, property := (_ : ζ - 1 ∈ NumberField.ringOfIntegers K) }

noncomputable def IsPrimitiveRoot.subOneIntegralPowerBasis' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ ↑p) : PowerBasis ℤ { x // x ∈ NumberField.ringOfIntegers K }

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

Equations

• IsPrimitiveRoot.subOneIntegralPowerBasis' hζ = IsPrimitiveRoot.subOneIntegralPowerBasis (_ : IsPrimitiveRoot ζ ↑(p ^ 1))

@[simp]

theorem IsPrimitiveRoot.subOneIntegralPowerBasis'_gen {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ ↑p) : (IsPrimitiveRoot.subOneIntegralPowerBasis' hζ).gen = { val := ζ - 1, property := (_ : ζ - 1 ∈ NumberField.ringOfIntegers K) }