mathlib3 documentation

number_theory.cyclotomic.discriminant

Discriminant of cyclotomic fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 is_cyclotomic_extension.discr_prime_pow_ne_two {p : ℕ+} {k : } {K : Type u} {L : Type v} {ζ : L} [field K] [field L] [algebra K L] [is_cyclotomic_extension {p ^ (k + 1)} K L] [hp : fact (nat.prime p)] (hζ : is_primitive_root ζ (p ^ (k + 1))) (hirr : irreducible (polynomial.cyclotomic (p ^ (k + 1)) K)) (hk : p ^ (k + 1) 2) :
algebra.discr K ((is_primitive_root.power_basis K hζ).basis) = (-1) ^ ((p ^ (k + 1)).totient / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

If p is a prime and is_cyclotomic_extension {p ^ (k + 1)} K L, then the discriminant of hζ.power_basis 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 is_cyclotomic_extension.discr_prime_pow_ne_two' {p : ℕ+} {k : } {K : Type u} {L : Type v} {ζ : L} [field K] [field L] [algebra K L] [is_cyclotomic_extension {p ^ (k + 1)} K L] [hp : fact (nat.prime p)] (hζ : is_primitive_root ζ (p ^ (k + 1))) (hirr : irreducible (polynomial.cyclotomic (p ^ (k + 1)) K)) (hk : p ^ (k + 1) 2) :
algebra.discr K ((is_primitive_root.power_basis K hζ).basis) = (-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

If p is a prime and is_cyclotomic_extension {p ^ (k + 1)} K L, then the discriminant of hζ.power_basis 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 is_cyclotomic_extension.discr_prime_pow {p : ℕ+} {k : } {K : Type u} {L : Type v} {ζ : L} [field K] [field L] [algebra K L] [hcycl : is_cyclotomic_extension {p ^ k} K L] [hp : fact (nat.prime p)] (hζ : is_primitive_root ζ (p ^ k)) (hirr : irreducible (polynomial.cyclotomic (p ^ k) K)) :
algebra.discr K ((is_primitive_root.power_basis K hζ).basis) = (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

If p is a prime and is_cyclotomic_extension {p ^ k} K L, then the discriminant of hζ.power_basis 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 is_cyclotomic_extension.discr_prime_pow_eq_unit_mul_pow.

theorem is_cyclotomic_extension.discr_prime_pow_eq_unit_mul_pow {p : ℕ+} {k : } {K : Type u} {L : Type v} {ζ : L} [field K] [field L] [algebra K L] [is_cyclotomic_extension {p ^ k} K L] [hp : fact (nat.prime p)] (hζ : is_primitive_root ζ (p ^ k)) (hirr : irreducible (polynomial.cyclotomic (p ^ k) K)) :

If p is a prime and is_cyclotomic_extension {p ^ k} K L, then there are u : ℤˣ and n : ℕ such that the discriminant of hζ.power_basis K is u * p ^ n. Often this is enough and less cumbersome to use than is_cyclotomic_extension.discr_prime_pow.

theorem is_cyclotomic_extension.discr_odd_prime {p : ℕ+} {K : Type u} {L : Type v} {ζ : L} [field K] [field L] [algebra K L] [is_cyclotomic_extension {p} K L] [hp : fact (nat.prime p)] (hζ : is_primitive_root ζ p) (hirr : irreducible (polynomial.cyclotomic p K)) (hodd : p 2) :
algebra.discr K ((is_primitive_root.power_basis K hζ).basis) = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)

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