[Merged by Bors] - feat(NumberField/Cyclotomic): splitting of the prime p in the p^k-th cyclotomic field

Mathlib.lean

@@ -4976,6 +4976,7 @@ import Mathlib.NumberTheory.NumberField.ClassNumber
 import Mathlib.NumberTheory.NumberField.Completion
 import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
 import Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
+import Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
 import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
 import Mathlib.NumberTheory.NumberField.Cyclotomic.Three
 import Mathlib.NumberTheory.NumberField.DedekindZeta

Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean

@@ -36,6 +36,10 @@ namespace IsCyclotomicExtension.Rat
 
 variable [CharZero K]
 
+variable (k K) in
+theorem finrank [NeZero k] [IsCyclotomicExtension {k} ℚ K] : Module.finrank ℚ K = k.totient :=
+  IsCyclotomicExtension.finrank K <| Polynomial.cyclotomic.irreducible_rat (NeZero.pos _)
+
 /-- The discriminant of the power basis given by `ζ - 1`. -/
 theorem discr_prime_pow_ne_two' [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
     (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hk : p ^ (k + 1) ≠ 2) :

Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

@@ -0,0 +1,141 @@
+/-
+Copyright (c) 2025 Xavier Roblot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Xavier Roblot
+-/
+import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
+import Mathlib.NumberTheory.RamificationInertia.Galois
+import Mathlib.RingTheory.Ideal.Int
+import Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
+
+/-!
+# Ideals in cyclotomic fields
+
+In this file, we prove results about ideals in cyclotomic extensions of `ℚ`.
+
+## Main results
+
+* `IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow`: there is only one prime ideal above
+  the prime `p` in `ℚ(ζ_pᵏ)`
+
+* `IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime_pow`: the residual degree of the prime ideal
+  above `p` in `ℚ(ζ_pᵏ)` is `1`.
+
+* `IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow`: the ramification index of the prime
+  ideal above `p` in `ℚ(ζ_pᵏ)` is `p ^ (k - 1) * (p - 1)`.
+-/
+
+namespace IsCyclotomicExtension.Rat
+
+open Ideal NumberField
+
+section PrimePow
+
+variable (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type*} [Field K] [NumberField K]
+  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
+
+local notation3 "𝒑" => (Ideal.span {(p : ℤ)})
+
+instance isPrime_span_zeta_sub_one : IsPrime (span {hζ.toInteger - 1}) := by
+  rw [Ideal.span_singleton_prime]
+  · exact hζ.zeta_sub_one_prime
+  · exact Prime.ne_zero hζ.zeta_sub_one_prime
+
+theorem associated_norm_zeta_sub_one : Associated (Algebra.norm ℤ (hζ.toInteger - 1)) (p : ℤ) := by
+  by_cases h : p = 2
+  · cases k with
+    | zero =>
+      rw [h, zero_add, pow_one] at hK hζ
+      rw [hζ.norm_toInteger_sub_one_of_eq_two, h, Int.ofNat_two, Associated.neg_left_iff]
+    | succ n =>
+      rw [h, add_assoc, show 1 + 1 = 2 by rfl] at hK hζ
+      rw [hζ.norm_toInteger_sub_one_of_eq_two_pow, h, Int.ofNat_two]
+  · rw [hζ.norm_toInteger_sub_one_of_prime_ne_two h]
+
+theorem absNorm_span_zeta_sub_one : absNorm (span {hζ.toInteger - 1}) = p := by
+  simpa using congr_arg absNorm <|
+    span_singleton_eq_span_singleton.mpr <| associated_norm_zeta_sub_one p k hζ
+
+theorem p_mem_span_zeta_sub_one : (p : 𝓞 K) ∈ span {hζ.toInteger - 1} := by
+  convert Ideal.absNorm_mem _
+  exact (absNorm_span_zeta_sub_one ..).symm
+
+theorem span_zeta_sub_one_ne_bot : span {hζ.toInteger - 1} ≠ ⊥ :=
+  (Submodule.ne_bot_iff _).mpr ⟨p, p_mem_span_zeta_sub_one p k hζ, NeZero.natCast_ne p (𝓞 K)⟩
+
+theorem liesOver_span_zeta_sub_one : (span {hζ.toInteger - 1}).LiesOver 𝒑 := by
+  rw [liesOver_iff]
+  refine Ideal.IsMaximal.eq_of_le (Int.ideal_span_isMaximal_of_prime p) IsPrime.ne_top' ?_
+  rw [span_singleton_le_iff_mem, mem_comap, algebraMap_int_eq, map_natCast]
+  exact p_mem_span_zeta_sub_one p k hζ
+
+theorem inertiaDeg_span_zeta_sub_one : inertiaDeg 𝒑 (span {hζ.toInteger - 1}) = 1 := by
+  have := liesOver_span_zeta_sub_one p k hζ
+  rw [← Nat.pow_right_inj hp.out.one_lt, pow_one, ← absNorm_eq_pow_inertiaDeg' _ hp.out,
+    absNorm_span_zeta_sub_one]
+
+attribute [local instance] FractionRing.liftAlgebra in
+theorem map_eq_span_zeta_sub_one_pow :
+    (map (algebraMap ℤ (𝓞 K)) 𝒑) = span {hζ.toInteger - 1} ^ Module.finrank ℚ K := by
+  have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
+  have : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K)) := by
+    refine IsGalois.of_equiv_equiv (f := (FractionRing.algEquiv ℤ ℚ).toRingEquiv.symm)
+      (g := (FractionRing.algEquiv (𝓞 K) K).toRingEquiv.symm) <|
+        RingHom.ext fun x ↦ IsFractionRing.algEquiv_commutes (FractionRing.algEquiv ℤ ℚ).symm
+          (FractionRing.algEquiv (𝓞 K) K).symm _
+  rw [map_span, Set.image_singleton, span_singleton_eq_span_singleton.mpr
+    ((associated_norm_zeta_sub_one p k hζ).symm.map (algebraMap ℤ (𝓞 K))),
+    ← Algebra.intNorm_eq_norm, Algebra.algebraMap_intNorm_of_isGalois, ← prod_span_singleton]
+  conv_lhs =>
+    enter [2, σ]
+    rw [span_singleton_eq_span_singleton.mpr
+      (hζ.toInteger_isPrimitiveRoot.associated_sub_one_map_sub_one σ).symm]
+  rw [Finset.prod_const, Finset.card_univ, ← Fintype.card_congr (galRestrict ℤ ℚ K (𝓞 K)).toEquiv,
+    ← Nat.card_eq_fintype_card, IsGalois.card_aut_eq_finrank]
+
+theorem ramificationIdx_span_zeta_sub_one :
+    ramificationIdx (algebraMap ℤ (𝓞 K)) 𝒑 (span {hζ.toInteger - 1}) = p ^ k * (p - 1) := by
+  have := liesOver_span_zeta_sub_one p k hζ
+  have h := isPrime_span_zeta_sub_one p k hζ
+  rw [← Nat.totient_prime_pow_succ hp.out, ← finrank _ K,
+    IsDedekindDomain.ramificationIdx_eq_multiplicity _ h, map_eq_span_zeta_sub_one_pow p k hζ,
+    multiplicity_pow_self (span_zeta_sub_one_ne_bot p k hζ) (isUnit_iff.not.mpr h.ne_top)]
+  exact map_ne_bot_of_ne_bot <| by simpa using hp.out.ne_zero
+
+variable (K)
+
+include hK in
+theorem ncard_primesOver_of_prime_pow :
+    (primesOver 𝒑 (𝓞 K)).ncard = 1 := by
+  have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
+  have : 𝒑 ≠ ⊥ := by simpa using hp.out.ne_zero
+  have h_main := ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn this (𝓞 K) ℚ K
+  have hζ := hK.zeta_spec
+  have := liesOver_span_zeta_sub_one p k hζ
+  rwa [ramificationIdxIn_eq_ramificationIdx 𝒑 (span {hζ.toInteger - 1}) ℚ K,
+    inertiaDegIn_eq_inertiaDeg 𝒑 (span {hζ.toInteger - 1}) ℚ K, inertiaDeg_span_zeta_sub_one,
+    ramificationIdx_span_zeta_sub_one, mul_one, ← Nat.totient_prime_pow_succ hp.out,
+    ← finrank _ K, Nat.mul_eq_right] at h_main
+  exact Module.finrank_pos.ne'
+
+theorem eq_span_zeta_sub_one_of_liesOver (P : Ideal (𝓞 K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver 𝒑] :
+    P = span {hζ.toInteger - 1} := by
+  have : P ∈ primesOver 𝒑 (𝓞 K) := ⟨hP₁, hP₂⟩
+  have : span {hζ.toInteger - 1} ∈ primesOver 𝒑 (𝓞 K) :=
+    ⟨isPrime_span_zeta_sub_one p k hζ, liesOver_span_zeta_sub_one p k hζ⟩
+  have := ncard_primesOver_of_prime_pow p k K
+  aesop
+
+include hK in
+theorem inertiaDeg_eq_of_prime_pow (P : Ideal (𝓞 K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver 𝒑] :
+    inertiaDeg 𝒑 P = 1 := by
+  rw [eq_span_zeta_sub_one_of_liesOver p k K hK.zeta_spec P, inertiaDeg_span_zeta_sub_one]
+
+include hK in
+theorem ramificationIdx_eq_of_prime_pow (P : Ideal (𝓞 K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver 𝒑] :
+    ramificationIdx (algebraMap ℤ (𝓞 K)) 𝒑 P = p ^ k * (p - 1) := by
+  rw [eq_span_zeta_sub_one_of_liesOver p k K hK.zeta_spec P, ramificationIdx_span_zeta_sub_one]
+
+end PrimePow
+
+end IsCyclotomicExtension.Rat

Mathlib/NumberTheory/RamificationInertia/Basic.lean

@@ -319,7 +319,8 @@ end DecEq
 section absNorm
 
 /-- The absolute norm of an ideal `P` above a rational prime `p` is
-`|p| ^ ((span {p}).inertiaDeg P)`. -/
+`|p| ^ ((span {p}).inertiaDeg P)`.
+See `absNorm_eq_pow_inertiaDeg'` for a version with `p` of type `ℕ`. -/
 lemma absNorm_eq_pow_inertiaDeg [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {p : ℤ}
     (P : Ideal R) [P.LiesOver (span {p})] (hp : Prime p) :
     absNorm P = p.natAbs ^ ((span {p}).inertiaDeg P) := by
@@ -331,6 +332,14 @@ lemma absNorm_eq_pow_inertiaDeg [IsDedekindDomain R] [Module.Free ℤ R] [Module
     Module.natCard_eq_pow_finrank (K := ℤ ⧸ span {p})]
   simp [Nat.card_congr (Int.quotientSpanEquivZMod p).toEquiv]
 
+/-- The absolute norm of an ideal `P` above a rational (positive) prime `p` is
+`p ^ ((span {p}).inertiaDeg P)`.
+See `absNorm_eq_pow_inertiaDeg` for a version with `p` of type `ℤ`. -/
+lemma absNorm_eq_pow_inertiaDeg' [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {p : ℕ}
+    (P : Ideal R) [P.LiesOver (span {(p : ℤ)})] (hp : p.Prime) :
+    absNorm P = p ^ ((span {(p : ℤ)}).inertiaDeg P) :=
+  absNorm_eq_pow_inertiaDeg P ( Nat.prime_iff_prime_int.mp hp)
+
 end absNorm
 section FinrankQuotientMap
 

Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean

@@ -33,7 +33,7 @@ open Polynomial Finset Nat
 
 variable {n i j p : ℕ} {A K : Type*} {ζ : A}
 
-variable [CommRing A] [IsDomain A]
+variable [CommRing A] [IsDomain A] {R : Type*} [CommRing R] [Algebra R A]
 
 namespace IsPrimitiveRoot
 
@@ -59,6 +59,22 @@ theorem associated_pow_sub_one_pow_of_coprime (hζ : IsPrimitiveRoot ζ n)
     grind [Associated.trans, Associated.symm]
   exact hζ.associated_sub_one_pow_sub_one_of_coprime
 
+/-- Given an `n`-th primitive root of unity `ζ`, we have that `ζ - 1` is associated to any of its
+  conjugate. -/
+theorem associated_sub_one_map_sub_one {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n)
+    (σ : A ≃ₐ[R] A) : Associated (ζ - 1) (σ (ζ - 1)) := by
+  rw [map_sub, map_one, ← hζ.autToPow_spec R σ]
+  apply hζ.associated_sub_one_pow_sub_one_of_coprime
+  exact ZMod.val_coe_unit_coprime ((autToPow R hζ) σ)
+
+/-- Given an `n`-th primitive root of unity `ζ`, we have that two conjugates of `ζ - 1`
+  are associated. -/
+theorem associated_map_sub_one_map_sub_one {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n)
+    (σ τ : A ≃ₐ[R] A) : Associated (σ (ζ - 1)) (τ (ζ - 1)) := by
+  rw [map_sub, map_sub, map_one, map_one, ← hζ.autToPow_spec R σ, ← hζ.autToPow_spec R τ]
+  apply hζ.associated_pow_sub_one_pow_of_coprime <;>
+  exact ZMod.val_coe_unit_coprime ((autToPow R hζ) _)
+
 /-- Given an `n`-th primitive root of unity `ζ`, where `2 ≤ n`, we have that `∑ i ∈ range j, ζ ^ i`
   is a unit for all `j` coprime with `n`. This is the unit given by
   `associated_pow_sub_one_pow_of_coprime` (see