discr_prime_pow_ne_two — Mathlib

English

If p is prime and IsCyclotomicExtension {p^(k+1)} K L with ζ primitive root and irreducible cyclotomic, then discr K (hζ.powerBasis K).basis equals (-1)^{((p^(k+1)) totient)/2} * p^{p^k * ((p-1)*(k+1)-1)}.

Русский

Для простого p и IsCyclotomicExtension {p^(k+1)} K L при ζ примитивного корня и ирреducибльной циклотоми, дискриминант равен (-1)^{phi(p^(k+1))/2} * p^{p^k * ((p-1)*(k+1)-1)}.

LaTeX

$$$\\mathrm{discr}_K( h\\zeta.powerBasis K).basis = (-1)^{\\frac{\\varphi(p^{k+1})}{2}} \\cdot p^{p^k((p-1)(k+1)-1)}$$$

Lean4

/-- 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 discr_prime_pow_ne_two [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact p.Prime]
    (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)) (hk : p ^ (k + 1) ≠ 2) :
    discr K (hζ.powerBasis K).basis = (-1) ^ ((p ^ (k + 1)).totient / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1)) :=
  by
  haveI hne := IsCyclotomicExtension.neZero' (p ^ (k + 1)) K L
  haveI mf : Module.Finite K L := finiteDimensional {p ^ (k + 1)} K L
  haveI se : Algebra.IsSeparable K L := isSeparable {p ^ (k + 1)} K L
  rw [discr_powerBasis_eq_norm, finrank L hirr, hζ.powerBasis_gen _, ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr,
    totient_prime_pow hp.out (succ_pos k), Nat.add_one_sub_one]
  have hp2 : p = 2 → k ≠ 0 := by
    rintro rfl rfl
    exact absurd rfl hk
  congr 1
  · rcases eq_or_ne p 2 with (rfl | hp2)
    · rcases Nat.exists_eq_succ_of_ne_zero (hp2 rfl) with ⟨k, rfl⟩
      rw [succ_sub_succ_eq_sub, tsub_zero, mul_one]; simp only [_root_.pow_succ']
      rw [mul_assoc, Nat.mul_div_cancel_left _ zero_lt_two, Nat.mul_div_cancel_left _ zero_lt_two]
      cases k
      · simp
      · simp_rw [_root_.pow_succ', (even_two.mul_right _).neg_one_pow, ((even_two.mul_right _).mul_right _).neg_one_pow]
    · have hpo : Odd p := hp.out.odd_of_ne_two hp2
      obtain ⟨a, ha⟩ := (hp.out.even_sub_one hp2).two_dvd
      rw [ha, mul_left_comm, mul_assoc, Nat.mul_div_cancel_left _ two_pos, Nat.mul_div_cancel_left _ two_pos,
        mul_right_comm, pow_mul, (hpo.pow.mul _).neg_one_pow, pow_mul, hpo.pow.neg_one_pow]
      refine Nat.Even.sub_odd ?_ (even_two_mul _) odd_one
      rw [mul_left_comm, ← ha]
      exact one_le_mul (one_le_pow _ _ hp.1.pos) (succ_le_iff.2 <| tsub_pos_of_lt hp.1.one_lt)
  · have H := congr_arg (@derivative K _) (cyclotomic_prime_pow_mul_X_pow_sub_one K p k)
    rw [derivative_mul, derivative_sub, derivative_one, sub_zero, derivative_X_pow, C_eq_natCast, derivative_sub,
      derivative_one, sub_zero, derivative_X_pow, C_eq_natCast, hζ.minpoly_eq_cyclotomic_of_irreducible hirr] at H
    replace H := congr_arg (fun P => aeval ζ P) H
    simp only [aeval_add, aeval_mul, minpoly.aeval, zero_mul, add_zero, aeval_natCast, map_sub, aeval_one,
      aeval_X_pow] at H
    replace H := congr_arg (Algebra.norm K) H
    have hnorm : (norm K) (ζ ^ p ^ k - 1) = (p : K) ^ p ^ k :=
      by
      by_cases hp : p = 2
      · exact mod_cast hζ.norm_pow_sub_one_eq_prime_pow_of_ne_zero hirr le_rfl (hp2 hp)
      · exact mod_cast hζ.norm_pow_sub_one_of_prime_ne_two hirr le_rfl hp
    rw [MonoidHom.map_mul, hnorm, MonoidHom.map_mul, ← map_natCast (algebraMap K L), Algebra.norm_algebraMap,
      finrank L hirr, ← succ_eq_add_one, totient_prime_pow hp.out (succ_pos k), Nat.sub_one, Nat.pred_succ] at H
    rw [← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_pow, hζ.norm_eq_one hk hirr, one_pow, mul_one, cast_pow, ←
      pow_mul, ← mul_assoc, mul_comm (k + 1), mul_assoc] at H
    have := mul_pos (succ_pos k) (tsub_pos_of_lt hp.out.one_lt)
    rw [← succ_pred_eq_of_pos this, mul_succ, pow_add _ _ (p ^ k)] at H
    replace H := (mul_left_inj' fun h => ?_).1 H
    · simp only [H, mul_comm _ (k + 1)]; norm_cast
    · have := hne.1
      rw [Nat.cast_pow, Ne, pow_eq_zero_iff (by cutsat)] at this
      exact absurd (pow_eq_zero h) this

Похожие утверждения