Norms and multiplicities of prime ideals over a rational prime

noncomputable def NairTenenbaum.rationalPrimeBelow {K : Type u_1} [Field K] (P : Ideal (NumberField.RingOfIntegers K)) : ℕ

The rational prime below a prime ideal.

Equations

• NairTenenbaum.rationalPrimeBelow P = Ideal.absNorm (Ideal.under ℤ P)

theorem NairTenenbaum.rationalPrimeBelow_prime {K : Type u_1} [Field K] [NumberField K] {P : Ideal (NumberField.RingOfIntegers K)} (hP : Prime P) : Nat.Prime (rationalPrimeBelow P)

theorem NairTenenbaum.idealNorm_eq_primeBelow_pow {K : Type u_1} [Field K] [NumberField K] {P : Ideal (NumberField.RingOfIntegers K)} (hP : Prime P) : Ideal.absNorm P = rationalPrimeBelow P ^ P.inertiaDeg ℤ

theorem NairTenenbaum.rationalPrimeBelow_le_norm {K : Type u_1} [Field K] [NumberField K] {P : Ideal (NumberField.RingOfIntegers K)} (hP : Prime P) : rationalPrimeBelow P ≤ Ideal.absNorm P

theorem NairTenenbaum.rationalPrimeBelow_sq_le_norm {K : Type u_1} [Field K] [NumberField K] {P : Ideal (NumberField.RingOfIntegers K)} (hP : Prime P) (hneq : Ideal.absNorm P ≠ rationalPrimeBelow P) : rationalPrimeBelow P ^ 2 ≤ Ideal.absNorm P

theorem NairTenenbaum.card_primesOver_nat_le_degree {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) : Nat.card ↑((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K)) ≤ Module.finrank ℚ K

theorem NairTenenbaum.primeIdeals_fiber_card_le {K : Type u_1} [Field K] [NumberField K] (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : ∀ P ∈ S, Prime P) {p : ℕ} (hp : Nat.Prime p) : {P ∈ S | rationalPrimeBelow P = p}.card ≤ Module.finrank ℚ K