Prime ideals of rings of integers

This file records general utilities for the prime ideals of a number field above a rational prime: packaging them as non-zero-divisors so that their classes can be taken with ClassGroup.mk0, counting them, and factoring an unramified rational prime into them.

Main results

• NumberField.mem_nonZeroDivisors_of_prime_of_liesOver: a prime ideal above a rational prime is a non-zero-divisor in the ideal monoid.
• NumberField.exists_primeIdealFamily: a finite set of rational primes admits a family of prime ideals above it, packaged for ClassGroup.mk0.
• TauCeti.NumberField.card_primesOverFinset_le_finrank: at most [K : ℚ] primes of 𝓞 K lie over a nonzero prime of ℤ.
• TauCeti.NumberField.span_natCast_eq_prod_primesOverFinset: a rational prime unramified in K generates the squarefree product of the primes of 𝓞 K above it.
• TauCeti.NumberField.isPrime_span_natCast_iff_of_eq_prod_primesOverFinset_pow: if a rational prime generates a power e of the product of the primes above it, it stays prime iff a single prime lies above it and e = 1.

theorem NumberField.mem_nonZeroDivisors_of_prime_of_liesOver {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.LiesOver (Ideal.span {↑p})] : 𝔭 ∈ nonZeroDivisors (Ideal (RingOfIntegers K))

An ideal lying over a rational prime is a non-zero-divisor in the ideal monoid, so it can be passed to ClassGroup.mk0.

theorem NumberField.exists_primeIdealFamily {K : Type u_1} [Field K] [NumberField K] (s : Finset ℕ) (hs : ∀ p ∈ s, Nat.Prime p) : ∃ (Q : ℕ → ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))), (∀ p ∈ s, (↑(Q p)).IsPrime) ∧ ∀ p ∈ s, (↑(Q p)).LiesOver (Ideal.span {↑p})

A finite set of rational primes admits a family of prime ideals above it, packaged as non-zero-divisors so their classes can be taken with ClassGroup.mk0. Away from the specified finite set the family is filled with the unit ideal.

theorem TauCeti.NumberField.card_primesOverFinset_le_finrank {K : Type u_1} [Field K] [NumberField K] {p : Ideal ℤ} [p.IsMaximal] (hp0 : p ≠ ⊥) : (IsDedekindDomain.primesOverFinset p (NumberField.RingOfIntegers K)).card ≤ Module.finrank ℚ K

At most [K : ℚ] primes of 𝓞 K lie over a given nonzero prime of ℤ, since each contributes a positive ramificationIdx * inertiaDeg to the fundamental identity.

theorem TauCeti.NumberField.span_natCast_eq_prod_primesOverFinset {K : Type u_1} [Field K] [NumberField K] {p : ℕ} [Fact (Nat.Prime p)] (hun : ∀ (P : Ideal (NumberField.RingOfIntegers K)) [inst : P.IsPrime] [P.LiesOver (Ideal.span {↑p})], Algebra.IsUnramifiedAt (NumberField.RingOfIntegers ℚ) P) : Ideal.span {↑p} = ∏ P ∈ IsDedekindDomain.primesOverFinset (Ideal.span {↑p}) (NumberField.RingOfIntegers K), P

An unramified rational prime is the product of the primes above it. If every prime P of 𝓞 K above the rational prime p is unramified, then p generates the squarefree product of those primes: each occurs with ramification index one.

theorem TauCeti.NumberField.isPrime_span_natCast_iff_of_eq_prod_primesOverFinset_pow {K : Type u_1} [Field K] [NumberField K] {p e : ℕ} [hp : Fact (Nat.Prime p)] (hfac : Ideal.span {↑p} = (∏ P ∈ IsDedekindDomain.primesOverFinset (Ideal.span {↑p}) (NumberField.RingOfIntegers K), P) ^ e) : (Ideal.span {↑p}).IsPrime ↔ ((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K)).ncard = 1 ∧ e = 1

When a rational prime stays prime. If p 𝓞 K is the product of the primes above the rational prime p raised to a common power e, then p 𝓞 K is prime iff a single prime lies above p and e = 1.