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.ramificationIdxIn_eq_of_prime_pow: the ramification index of the prime ideal above p in ℚ(ζ_pᵏ) is p ^ (k - 1) * (p - 1).

• IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd: if the prime p does not divide m, then the inertia degree of p in ℚ(ζₘ) is the order of p modulo m.

• IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd: if the prime p does not divide m, then the ramification index of p in ℚ(ζₘ) is 1.

• IsCyclotomicExtension.Rat.inertiaDegIn_eq: write n = p ^ (k + 1) * m where the prime p does not divide m, then the inertia degree of p in ℚ(ζₙ) is the order of p modulo m.

• IsCyclotomicExtension.Rat.ramificationIdxIn_eq: write n = p ^ (k + 1) * m where the prime p does not divide m, then the ramification index of p in ℚ(ζₙ) is p ^ k * (p - 1).

instance IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : (Ideal.span {hζ.toInteger - 1}).IsPrime

theorem IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p

theorem IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : Ideal.absNorm (Ideal.span {hζ.toInteger - 1}) = p

theorem IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : ↑p ∈ Ideal.span {hζ.toInteger - 1}

theorem IsCyclotomicExtension.Rat.span_zeta_sub_one_ne_bot (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : Ideal.span {hζ.toInteger - 1} ≠ ⊥

instance IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : (Ideal.span {hζ.toInteger - 1}).LiesOver (Ideal.span {↑p})

theorem IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : (Ideal.span {↑p}).inertiaDeg (Ideal.span {hζ.toInteger - 1}) = 1

theorem IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : Ideal.map (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑p}) = Ideal.span {hζ.toInteger - 1} ^ Module.finrank ℚ K

theorem IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : Ideal.ramificationIdx (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑p}) (Ideal.span {hζ.toInteger - 1}) = p ^ k * (p - 1)

theorem IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] : ((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K)).ncard = 1

theorem IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] : P = Ideal.span {hζ.toInteger - 1}

theorem IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime_pow (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] : (Ideal.span {↑p}).inertiaDeg P = 1

theorem IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] : Ideal.ramificationIdx (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑p}) P = p ^ k * (p - 1)

theorem IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] : (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = 1

theorem IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] : (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = p ^ k * (p - 1)

instance IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one' (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) : (Ideal.span {hζ.toInteger - 1}).IsPrime

theorem IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one' (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) : (Ideal.span {↑p}).inertiaDeg (Ideal.span {hζ.toInteger - 1}) = 1

theorem IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one' (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) : Ideal.ramificationIdx (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑p}) (Ideal.span {hζ.toInteger - 1}) = p - 1

theorem IsCyclotomicExtension.Rat.ncard_primesOver_of_prime (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] : ((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K)).ncard = 1

theorem IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver' (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] : P = Ideal.span {hζ.toInteger - 1}

theorem IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] : (Ideal.span {↑p}).inertiaDeg P = 1

theorem IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] : Ideal.ramificationIdx (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑p}) P = p - 1

theorem IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] : (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = 1

theorem IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] : (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = p - 1

@[deprecated IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime (since := "2025-12-03")]

theorem IsCyclotomicExtension.Rat.ramificationIdxIn_of_prime (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] : (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = p - 1

Alias of IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime.

theorem IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K] (hm : ¬p ∣ m) : (Ideal.span {↑p}).inertiaDeg P = orderOf ↑p

@[deprecated IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd (since := "2025-12-10")]

theorem IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K] (hm : ¬p ∣ m) : (Ideal.span {↑p}).inertiaDeg P = orderOf ↑p

Alias of IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd.

theorem IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K] (hm : ¬p ∣ m) : Ideal.ramificationIdx (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑p}) P = 1

@[deprecated IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd (since := "2025-12-10")]

theorem IsCyclotomicExtension.Rat.ramificationIdx_of_not_dvd {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K] (hm : ¬p ∣ m) : Ideal.ramificationIdx (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑p}) P = 1

Alias of IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd.

theorem IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K] (hm : ¬p ∣ m) : (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = orderOf ↑p

theorem IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K] (hm : ¬p ∣ m) : (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = 1

@[deprecated IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd (since := "2025-12-03")]

theorem IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K] (hm : ¬p ∣ m) : (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = orderOf ↑p

Alias of IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd.

@[deprecated IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd (since := "2025-12-03")]

theorem IsCyclotomicExtension.Rat.ramificationIdxIn_of_not_dvd {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K] (hm : ¬p ∣ m) : (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = 1

Alias of IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd.

theorem IsCyclotomicExtension.Rat.inertiaDegIn_eq (n : ℕ) {m p k : ℕ} [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] (hn : n = p ^ (k + 1) * m) (hm : ¬p ∣ m) : (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = orderOf ↑p

Write n = p ^ (k + 1) * m where the prime p does not divide m, then the inertia degree of p in ℚ(ζₙ) is the order of p modulo m.

theorem IsCyclotomicExtension.Rat.ramificationIdxIn_eq (n : ℕ) {m p k : ℕ} [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] (hn : n = p ^ (k + 1) * m) (hm : ¬p ∣ m) : (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = p ^ k * (p - 1)

Write n = p ^ (k + 1) * m where the prime p does not divide m, then the ramification index of p in ℚ(ζₙ) is p ^ k * (p - 1).

theorem IsCyclotomicExtension.Rat.inertiaDeg_eq (n : ℕ) {m p k : ℕ} [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] [IsCyclotomicExtension {n} ℚ K] (hn : n = p ^ (k + 1) * m) (hm : ¬p ∣ m) : (Ideal.span {↑p}).inertiaDeg P = orderOf ↑p

theorem IsCyclotomicExtension.Rat.ramificationIdx_eq (n : ℕ) {m p k : ℕ} [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] [IsCyclotomicExtension {n} ℚ K] (hn : n = p ^ (k + 1) * m) (hm : ¬p ∣ m) : Ideal.ramificationIdx (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑p}) P = p ^ k * (p - 1)