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) ℤ ℚ.
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)
:
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)
:
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))
:
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 ↥(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 ↥(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_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 : ↥(NumberField.ringOfIntegers K))
:
(AlgEquiv.symm (IsPrimitiveRoot.adjoinEquivRingOfIntegers hζ)) a = (IsIntegralClosure.lift (↥(Algebra.adjoin ℤ {ζ})) K (_ : Algebra.IsIntegral ℤ ↥(NumberField.ringOfIntegers K))) a
@[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 : ↥(Algebra.adjoin ℤ {ζ}))
:
(IsPrimitiveRoot.adjoinEquivRingOfIntegers hζ) a = (IsIntegralClosure.lift (↥(NumberField.ringOfIntegers K)) K (_ : Algebra.IsIntegral ℤ ↥(Algebra.adjoin ℤ {ζ}))) 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))
:
↥(Algebra.adjoin ℤ {ζ}) ≃ₐ[ℤ] ↥(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
- IsPrimitiveRoot.adjoinEquivRingOfIntegers hζ = let x := (_ : IsIntegralClosure ↥(Algebra.adjoin ℤ {ζ}) ℤ K); IsIntegralClosure.equiv ℤ (↥(Algebra.adjoin ℤ {ζ})) K ↥(NumberField.ringOfIntegers K)
Instances For
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} ℤ ↥(NumberField.ringOfIntegers K)
The ring of integers of a p ^ k-th cyclotomic extension of ℚ is a cyclotomic extension.
Equations
- (_ : IsCyclotomicExtension {p ^ k} ℤ ↥(NumberField.ringOfIntegers K)) = (_ : IsCyclotomicExtension {p ^ k} ℤ ↥(NumberField.ringOfIntegers K))
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))
:
The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a p ^ k
cyclotomic extension of ℚ.
Equations
Instances For
@[inline, reducible]
abbrev
IsPrimitiveRoot.toInteger
{K : Type u}
[Field K]
{ζ : K}
{k : ℕ+}
(hζ : IsPrimitiveRoot ζ ↑k)
:
Abbreviation to see a primitive root of unity as a member of the ring of integers.
Equations
- IsPrimitiveRoot.toInteger hζ = { val := ζ, property := (_ : IsIntegral ℤ ζ) }
Instances For
@[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))
:
@[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'_symm_apply
{p : ℕ+}
{K : Type u}
[Field K]
[CharZero K]
{ζ : K}
[hp : Fact (Nat.Prime ↑p)]
[hcycl : IsCyclotomicExtension {p} ℚ K]
(hζ : IsPrimitiveRoot ζ ↑p)
(a : ↥(NumberField.ringOfIntegers K))
:
(AlgEquiv.symm (IsPrimitiveRoot.adjoinEquivRingOfIntegers' hζ)) a = (IsIntegralClosure.lift (↥(Algebra.adjoin ℤ {ζ})) K (_ : Algebra.IsIntegral ℤ ↥(NumberField.ringOfIntegers K))) a
@[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 : ↥(Algebra.adjoin ℤ {ζ}))
:
(IsPrimitiveRoot.adjoinEquivRingOfIntegers' hζ) a = (IsIntegralClosure.lift (↥(NumberField.ringOfIntegers K)) K (_ : Algebra.IsIntegral ℤ ↥(Algebra.adjoin ℤ {ζ}))) 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)
:
↥(Algebra.adjoin ℤ {ζ}) ≃ₐ[ℤ] ↥(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
Instances For
instance
IsCyclotomicExtension.ring_of_integers'
{p : ℕ+}
{K : Type u}
[Field K]
[CharZero K]
[hp : Fact (Nat.Prime ↑p)]
[IsCyclotomicExtension {p} ℚ K]
:
The ring of integers of a p-th cyclotomic extension of ℚ is a cyclotomic extension.
Equations
- (_ : IsCyclotomicExtension {p} ℤ ↥(NumberField.ringOfIntegers K)) = (_ : IsCyclotomicExtension {p} ℤ ↥(NumberField.ringOfIntegers K))
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)
:
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))
Instances For
@[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)
:
@[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))
:
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.
Instances For
@[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)
:
The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a p-th cyclotomic
extension of ℚ.
Equations
Instances For
@[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 = IsPrimitiveRoot.toInteger hζ - 1
theorem
IsPrimitiveRoot.zeta_sub_one_prime_of_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)))
(hodd : p ≠ 2)
:
Prime (IsPrimitiveRoot.toInteger hζ - 1)
ζ - 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.
theorem
IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow
{k : ℕ}
{K : Type u}
[Field K]
[CharZero K]
{ζ : K}
[IsCyclotomicExtension {2 ^ (k + 1)} ℚ K]
(hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1)))
:
Prime (IsPrimitiveRoot.toInteger hζ - 1)
ζ - 1 is prime if ζ is a primitive 2 ^ (k + 1)-th root of unity.
See zeta_sub_one_prime for a general statement.
theorem
IsPrimitiveRoot.zeta_sub_one_prime
{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)))
:
Prime (IsPrimitiveRoot.toInteger hζ - 1)
ζ - 1 is prime if ζ is a primitive p ^ (k + 1)-th root of unity.
theorem
IsPrimitiveRoot.zeta_sub_one_prime'
{p : ℕ+}
{K : Type u}
[Field K]
[CharZero K]
{ζ : K}
[hp : Fact (Nat.Prime ↑p)]
[h : IsCyclotomicExtension {p} ℚ K]
(hζ : IsPrimitiveRoot ζ ↑p)
:
Prime (IsPrimitiveRoot.toInteger hζ - 1)
ζ - 1 is prime if ζ is a primitive p-th root of unity.
theorem
IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime
{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)))
:
theorem
IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime
{p : ℕ+}
{K : Type u}
[Field K]
[CharZero K]
{ζ : K}
[hp : Fact (Nat.Prime ↑p)]
[IsCyclotomicExtension {p} ℚ K]
(hζ : IsPrimitiveRoot ζ ↑p)
: