Documentation

Mathlib.NumberTheory.Cyclotomic.Discriminant

Discriminant of cyclotomic fields #

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

Main results #

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 (p).Prime] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) (hk : p ^ (k + 1) 2) :
Algebra.discr K (IsPrimitiveRoot.powerBasis K ).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 (p).Prime] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) (hk : p ^ (k + 1) 2) :
Algebra.discr K (IsPrimitiveRoot.powerBasis K ).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 (p).Prime] (hζ : IsPrimitiveRoot ζ (p ^ k)) (hirr : Irreducible (Polynomial.cyclotomic ((p ^ k)) K)) :
Algebra.discr K (IsPrimitiveRoot.powerBasis K ).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 (p).Prime] (hζ : IsPrimitiveRoot ζ (p ^ k)) (hirr : Irreducible (Polynomial.cyclotomic ((p ^ k)) K)) :
∃ (u : ˣ) (n : ), Algebra.discr K (IsPrimitiveRoot.powerBasis K ).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 (p).Prime] (hζ : IsPrimitiveRoot ζ p) (hirr : Irreducible (Polynomial.cyclotomic (p) K)) (hodd : p 2) :
Algebra.discr K (IsPrimitiveRoot.powerBasis K ).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).