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).
IsCyclotomicExtension.Rat.inertiaDeg_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.ramificationIdx_of_not_dvd: if the prime p does not divide m, then the ramification index of p in ℚ(ζₘ) is 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

source

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

source

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

source

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}

source

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

source

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

source

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

source

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

source

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)

source

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

source

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}

source

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

source

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)

source

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

source

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

source

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

source

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

source

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}

source

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

source

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

source

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

source

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

source

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

source

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

Documentation

Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Ideals in cyclotomic fields #

Main results #