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).

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} ≠ ⊥

theorem 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)