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.zeta_sub_one_dvd_intCast_iff (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))) {n : ℤ} : hζ.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n

An integer n is divisible by ζ - 1 in 𝓞 K if and only if it is divisible by p, where ζ is a primitive p ^ (k + 1)-th root of unity.

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 {hζ.toInteger - 1}).inertiaDeg ℤ = 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.span {hζ.toInteger - 1}).ramificationIdx ℤ = 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})] : P.inertiaDeg ℤ = 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})] : P.ramificationIdx ℤ = 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.two_not_mem_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) (h : 2 < p) : 2 ∉ Ideal.span {hζ.toInteger - 1}

If 2 < p, then 2 is not in the ideal (ζ - 1), where ζ is a primitive p-th root of unity.

theorem IsCyclotomicExtension.Rat.associated_sub_one_of_isPrimitiveRoot (p : ℕ) {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) [NeZero p] {η : K} (hη : IsPrimitiveRoot η p) : Associated (hζ.toInteger - 1) (hη.toInteger - 1)

theorem IsCyclotomicExtension.Rat.associated_zeta_sub_one_pow_prime (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) : Associated ((hζ.toInteger - 1) ^ (p - 1)) ↑p

(ζ - 1) ^ (p - 1) is associated to p, where ζ is a primitive p-th root of unity and p is prime.

theorem IsCyclotomicExtension.Rat.isCoprime_of_not_zeta_sub_one_dvd (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) {x : NumberField.RingOfIntegers K} (hx : ¬hζ.toInteger - 1 ∣ x) : IsCoprime (↑p) x

If ζ - 1 does not divide x, then p and x are coprime, where ζ is a primitive p-th root of unity and p is prime.

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 {hζ.toInteger - 1}).inertiaDeg ℤ = 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.span {hζ.toInteger - 1}).ramificationIdx ℤ = p - 1

theorem IsCyclotomicExtension.Rat.zeta_sub_one_dvd_intCast_iff' (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) {n : ℤ} : hζ.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n

An integer n is divisible by ζ - 1 in 𝓞 K if and only if it is divisible by p, where ζ is a primitive p-th root of unity.

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})] : P.inertiaDeg ℤ = 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})] : P.ramificationIdx ℤ = 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

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) : P.inertiaDeg ℤ = orderOf ↑p

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) : P.ramificationIdx ℤ = 1

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

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) : P.inertiaDeg ℤ = 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) : P.ramificationIdx ℤ = p ^ k * (p - 1)