Discriminant of cyclotomic fields

We compute the discriminant of a p ^ n-th cyclotomic extension.

Main results

• IsCyclotomicExtension.discr_odd_prime : if p is an odd prime such that IsCyclotomicExtension {p} K L and Irreducible (cyclotomic p K), then discr K (hζ.powerBasis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2) for any hζ : IsPrimitiveRoot ζ p.

theorem IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one {n : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [ce : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ ↑n) : Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis

The discriminant of the power basis given by a primitive root of unity ζ is the same as the discriminant of the power basis given by ζ - 1.

theorem IsCyclotomicExtension.discr_prime_pow_ne_two {p : ℕ+} {k : ℕ} {K : Type u} {L : Type v} {ζ : L} [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact (Nat.Prime ↑p)] (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)) (hk : p ^ (k + 1) ≠ 2) : Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p ^ (k + 1)).totient / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

If p is a prime and IsCyclotomicExtension {p ^ (k + 1)} K L, then the discriminant of hζ.powerBasis K is (-1) ^ ((p ^ (k + 1).totient) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1)) if Irreducible (cyclotomic (p ^ (k + 1)) K)), and p ^ (k + 1) ≠ 2.

theorem IsCyclotomicExtension.discr_prime_pow_ne_two' {p : ℕ+} {k : ℕ} {K : Type u} {L : Type v} {ζ : L} [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact (Nat.Prime ↑p)] (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)) (hk : p ^ (k + 1) ≠ 2) : Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (↑p ^ k * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

If p is a prime and IsCyclotomicExtension {p ^ (k + 1)} K L, then the discriminant of hζ.powerBasis K is (-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1)) if Irreducible (cyclotomic (p ^ (k + 1)) K)), and p ^ (k + 1) ≠ 2.

theorem IsCyclotomicExtension.discr_prime_pow {p : ℕ+} {k : ℕ} {K : Type u} {L : Type v} {ζ : L} [Field K] [Field L] [Algebra K L] [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact (Nat.Prime ↑p)] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ k)) K)) : Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p ^ k).totient / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

If p is a prime and IsCyclotomicExtension {p ^ k} K L, then the discriminant of hζ.powerBasis K is (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) if Irreducible (cyclotomic (p ^ k) K)). 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.discr_prime_pow_eq_unit_mul_pow.

theorem IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow {p : ℕ+} {k : ℕ} {K : Type u} {L : Type v} {ζ : L} [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {p ^ k} K L] [hp : Fact (Nat.Prime ↑p)] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ k)) K)) : ∃ (u : ℤˣ) (n : ℕ), Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K 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 hζ.powerBasis K is u * p ^ n. Often this is enough and less cumbersome to use than IsCyclotomicExtension.discr_prime_pow.

theorem IsCyclotomicExtension.discr_odd_prime {p : ℕ+} {K : Type u} {L : Type v} {ζ : L} [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {p} K L] [hp : Fact (Nat.Prime ↑p)] (hζ : IsPrimitiveRoot ζ ↑p) (hirr : Irreducible (Polynomial.cyclotomic (↑p) K)) (hodd : p ≠ 2) : Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)

If p is an odd prime and IsCyclotomicExtension {p} K L, then discr K (hζ.powerBasis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2) if Irreducible (cyclotomic p K).