English
The absolute discriminant of a p^k-th cyclotomic field is given by a closed formula; in particular this holds for primes p and K over Q.
Русский
Модульный дискриминант p^k-й циклотомической поля задаётся формулой; в частности для простого p и K над Q.
LaTeX
$$NumberField.discr K = (-1)^{((p^k).totient)/2} p^{p^{k-1}((p-1)k-1)}$$
Lean4
/-- We compute the absolute discriminant of a `p ^ k`-th cyclotomic field.
Beware that in the cases `p ^ k = 1` and `p ^ k = 2` the formula uses `1 / 2 = 0` and `0 - 1 = 0`.
See also the results below. -/
theorem absdiscr_prime_pow [IsCyclotomicExtension {p ^ k} ℚ K] :
haveI : NumberField K := IsCyclotomicExtension.numberField {p ^ k} ℚ K
NumberField.discr K = (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) :=
by
have hζ := IsCyclotomicExtension.zeta_spec (p ^ k) ℚ K
have : NumberField K := IsCyclotomicExtension.numberField {p ^ k} ℚ K
let pB₁ := integralPowerBasis hζ
apply (algebraMap ℤ ℚ).injective_int
rw [← NumberField.discr_eq_discr _ pB₁.basis, ← Algebra.discr_localizationLocalization ℤ ℤ⁰ K]
convert IsCyclotomicExtension.discr_prime_pow hζ (cyclotomic.irreducible_rat (NeZero.pos _)) using 1
· have : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim :=
by
rw [← PowerBasis.finrank, ← PowerBasis.finrank]
exact RingOfIntegers.rank K
rw [← Algebra.discr_reindex _ _ (finCongr this)]
congr 1
ext i
simp_rw [Function.comp_apply, Module.Basis.localizationLocalization_apply, powerBasis_dim, PowerBasis.coe_basis,
pB₁, integralPowerBasis_gen]
convert ← ((IsPrimitiveRoot.powerBasis ℚ hζ).basis_eq_pow i).symm using 1
· simp_rw [algebraMap_int_eq, map_mul, map_pow, map_neg, map_one, map_natCast]
