English
Under IsCyclotomicExtension {p^k} K L, discr K (hζ.powerBasis K).basis equals u * p^n for some unit u and natural n.
Русский
При IsCyclotomicExtension {p^k} K L дискриминант равен u * p^n.
LaTeX
$$$\\exists u∈ℤ^{\\times},\\exists n∈ℕ,\\; \\mathrm{discr}_K( h\\zeta.powerBasis K).basis = u \\cdot p^{n}$$$
Lean4
/-- 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 discr_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact p.Prime] (hζ : IsPrimitiveRoot ζ (p ^ k))
(hirr : Irreducible (cyclotomic (p ^ k) K)) :
discr K (hζ.powerBasis K).basis = (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) :=
by
rcases k with - | k
· simp only [coe_basis, _root_.pow_zero, powerBasis_gen _ hζ, totient_one, mul_zero, show 1 / 2 = 0 by rfl, discr,
traceMatrix]
have hζone : ζ = 1 := by simpa using hζ
rw [hζ.powerBasis_dim _, hζone, ← (algebraMap K L).map_one,
minpoly.eq_X_sub_C_of_algebraMap_inj _ (algebraMap K L).injective, natDegree_X_sub_C]
simp only [map_one, one_pow, Matrix.det_unique, traceForm_apply, mul_one]
rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]
simp
· by_cases hk : p ^ (k + 1) = 2
· obtain rfl : p = 2 := by
rw [← pow_one 2] at hk
exact eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 Nat.prime_two) (succ_pos _) hk
nth_rw 2 [← pow_one 2] at hk
replace hk := Nat.pow_right_injective rfl.le hk
rw [add_eq_right] at hk
subst hk
rw [pow_one] at hζ hcycl
have : natDegree (minpoly K ζ) = 1 :=
by
rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp,
minpoly.eq_X_sub_C_of_algebraMap_inj _ (FaithfulSMul.algebraMap_injective K L)]
exact natDegree_X_sub_C (-1)
rcases Fin.equiv_iff_eq.2 this with ⟨e⟩
rw [← Algebra.discr_reindex K (hζ.powerBasis K).basis e, coe_basis, powerBasis_gen]; norm_num
simp_rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp]
convert_to (discr K fun i : Fin 1 ↦ (algebraMap K L) (-1) ^ ↑i) = _
· congr 1
ext i
simp only [map_neg, map_one, Function.comp_apply, Fin.val_eq_zero, _root_.pow_zero]
suffices (e.symm i : ℕ) = 0 by simp [this]
rw [← Nat.lt_one_iff]
convert (e.symm i).2
rw [this]
· simp only [discr, traceMatrix_apply, Matrix.det_unique, Fin.default_eq_zero, Fin.val_zero, _root_.pow_zero,
traceForm_apply, mul_one]
rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]; simp
· exact discr_prime_pow_ne_two hζ hirr hk
