English
Let p be prime and hζ a primitive root of order p^(k+1) with irreducible cyclotomic. For s ≤ k and p^(k−s+1) ≠ 2, the norm N_K(ζ^{p^s} − 1) equals (p)^{p^s}.
Русский
Пусть p — простое; ζ примитивного порядка p^(k+1) и ирреducible циклотомическое. При s ≤ k и p^(k−s+1) ≠ 2 нормa N_K(ζ^{p^s} − 1) равна p^{p^s}.
LaTeX
$$$\operatorname{Norm}_{K}(\zeta^{p^s} - 1) = (p)^{p^s}$$$
Lean4
/-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `p ^ (k - s + 1) ≠ 2`. See the next lemmas
for similar results. -/
theorem norm_pow_sub_one_of_prime_pow_ne_two {k s : ℕ} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact p.Prime]
[IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)) (hs : s ≤ k)
(htwo : p ^ (k - s + 1) ≠ 2) : norm K (ζ ^ p ^ s - 1) = (p : K) ^ p ^ s :=
by
have hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K) :=
cyclotomic_irreducible_pow_of_irreducible_pow hpri.1 (by cutsat) hirr
set η := ζ ^ p ^ s - 1
let η₁ : K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
have hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s)) :=
by
rw [sub_add_cancel]
refine IsPrimitiveRoot.pow (pos_of_neZero (p ^ (k + 1))) hζ ?_
rw [← pow_add, add_comm s, Nat.sub_add_cancel (le_trans hs (Nat.le_succ k))]
have : IsCyclotomicExtension {p ^ (k - s + 1)} K K⟮η⟯ :=
by
have HKη : K⟮η⟯ = K⟮η + 1⟯ := by
refine le_antisymm ?_ ?_
all_goals rw [IntermediateField.adjoin_simple_le_iff]
· nth_rw 2 [← add_sub_cancel_right η 1]
exact sub_mem (IntermediateField.mem_adjoin_simple_self K (η + 1)) (one_mem _)
· exact add_mem (IntermediateField.mem_adjoin_simple_self K η) (one_mem _)
rw [HKη]
have H := IntermediateField.adjoin_simple_toSubalgebra_of_integral ((integral {p ^ (k + 1)} K L).isIntegral (η + 1))
refine IsCyclotomicExtension.equiv _ _ _ (h := ?_) (.refl : K⟮η + 1⟯.toSubalgebra ≃ₐ[K] _)
rw [H]
have hη' : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s)) := by simpa using hη
convert hη'.adjoin_isCyclotomicExtension K using 1
rw [Nat.sub_add_comm hs]
replace hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1)) :=
by
apply coe_submonoidClass_iff.1
convert hη using 1
rw [Nat.sub_add_comm hs]
have := IsCyclotomicExtension.finiteDimensional {p ^ (k + 1)} K L
have := IsCyclotomicExtension.isGalois {p ^ (k + 1)} K L
rw [norm_eq_norm_adjoin K]
have H := hη.sub_one_norm_isPrimePow ?_ hirr₁ htwo
swap; · exact hpri.1.isPrimePow.pow (Nat.succ_ne_zero _)
rw [add_sub_cancel_right] at H
rw [H]
congr
· rw [Nat.pow_minFac, hpri.1.minFac_eq]
exact Nat.succ_ne_zero _
have := Module.finrank_mul_finrank K K⟮η⟯ L
rw [IsCyclotomicExtension.finrank L hirr, IsCyclotomicExtension.finrank K⟮η⟯ hirr₁,
Nat.totient_prime_pow hpri.out (k - s).succ_pos, Nat.totient_prime_pow hpri.out k.succ_pos, mul_comm _ (p - 1),
mul_assoc, mul_comm (p ^ (k.succ - 1))] at this
replace this := mul_left_cancel₀ (tsub_pos_iff_lt.2 hpri.out.one_lt).ne' this
have Hex : k.succ - 1 = (k - s).succ - 1 + s :=
by
simp only [Nat.succ_sub_succ_eq_sub, tsub_zero]
exact (Nat.sub_add_cancel hs).symm
rw [Hex, pow_add] at this
exact mul_left_cancel₀ (pow_ne_zero _ hpri.out.ne_zero) this
