The finite set of prime ideals above a rational prime

noncomputable def NairTenenbaum.primeIdealSupport (K : Type u_2) [Field K] [NumberField K] (p : ℕ) : Finset (Ideal (NumberField.RingOfIntegers K))

The finite set of prime ideals above a specified rational prime.

Equations

• NairTenenbaum.primeIdealSupport K p = (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑p})).toFinset

theorem NairTenenbaum.span_prime_natCast_ne_bot {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) : Ideal.span {↑p} ≠ ⊥

theorem NairTenenbaum.primeIdealSupport_mem_iff {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) {P : Ideal (NumberField.RingOfIntegers K)} : P ∈ primeIdealSupport K p ↔ Prime P ∧ rationalPrimeBelow P = p

theorem NairTenenbaum.normalizedFactors_subset_primeIdealSupport {K : Type u_1} [Field K] [NumberField K] {I : Ideal (NumberField.RingOfIntegers K)} {p k : ℕ} (hp : Nat.Prime p) (hI : Ideal.absNorm I = p ^ k) : (UniqueFactorizationMonoid.normalizedFactors I).toFinset ⊆ primeIdealSupport K p

theorem NairTenenbaum.primeIdealSupport_norm {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) {P : Ideal (NumberField.RingOfIntegers K)} (hP : P ∈ primeIdealSupport K p) : Ideal.absNorm P = p ^ P.inertiaDeg ℤ

theorem NairTenenbaum.primeIdealSupport_inertiaDeg_pos {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) {P : Ideal (NumberField.RingOfIntegers K)} (hP : P ∈ primeIdealSupport K p) : 0 < P.inertiaDeg ℤ