Documentation

TauCeti.NumberTheory.NumberField.RamifiedPrimes

The ramified rational primes of a number field #

The genus theory of a quadratic field is governed by the number t of rational primes that ramify in it: the genus field has degree 2 ^ t over ℚ and the 2-rank of the narrow class group is t - 1. This file names that set of primes and records its basic properties.

Mathlib phrases ramification of a rational prime p in a number field K as Algebra.IsUnramifiedIn (𝓞 K) (Ideal.span {(p : ℤ)}), and characterises it by divisibility of the discriminant (NumberField.not_dvd_discr_iff_isUnramifiedIn). We package the negation as a set of natural primes, which is the form in which t is counted.

Main definitions #

Main results #

source
def NumberField.ramifiedPrimes (K : Type u_1) [Field K] :
Set ℕ

The ramified rational primes of a number field. The set of natural primes p such that p — as the ideal span {p} of ℤ — ramifies in the ring of integers of K. For a quadratic field K, its cardinality is the t of genus theory.

Equations
Instances For
    source
    @[simp]
    theorem NumberField.mem_ramifiedPrimes_iff {K : Type u_1} [Field K] {p : ℕ} :
    p ∈ ramifiedPrimes K ↔ Nat.Prime p ∧ ¬Algebra.IsUnramifiedIn (RingOfIntegers K) (Ideal.span {↑p})

    The defining condition for membership in ramifiedPrimes.

    source
    theorem NumberField.prime_of_mem_ramifiedPrimes {K : Type u_1} [Field K] {p : ℕ} (hp : p ∈ ramifiedPrimes K) :
    Nat.Prime p

    A ramified prime is prime.

    source
    theorem NumberField.mem_ramifiedPrimes_iff_dvd_discr {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) :
    p ∈ ramifiedPrimes K ↔ ↑p ∣ discr K

    Ramification is divisibility of the discriminant. A natural prime p ramifies in K iff p divides NumberField.discr K. This is NumberField.not_dvd_discr_iff_isUnramifiedIn in the ramifiedPrimes packaging.

    source
    theorem AlgEquiv.ramifiedPrimes_eq {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (f : K ≃ₐ[ℚ] L) :
    NumberField.ramifiedPrimes K = NumberField.ramifiedPrimes L

    Isomorphic number fields have the same ramified primes, since they have the same discriminant (NumberField.discr_eq_discr_of_algEquiv).

    source
    @[simp]
    theorem NumberField.ramifiedPrimes_rat :
    ramifiedPrimes ℚ = ∅

    No prime ramifies in ℚ, whose discriminant is 1.

    source
    theorem NumberField.coprime_natAbs_discr_of_isUnramifiedIn {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) (hur : Algebra.IsUnramifiedIn (RingOfIntegers K) (Ideal.span {↑p})) :
    (discr K).natAbs.Coprime p

    An unramified prime is coprime to the discriminant. If the rational prime p is unramified in K then it does not divide NumberField.discr K, so |discr K| and p are coprime.

    This is mem_ramifiedPrimes_iff_dvd_discr in the form the cyclotomic-crossing lemmas consume. They take ((NumberField.discr _).natAbs).Coprime m as an undischarged hypothesis, and IsCyclotomicExtension.finrank_eq_totient records in its implementation notes that a caller is expected to arrange it "by choosing m to be a prime unramified in K". This is that sentence as a lemma, so the hypothesis can be discharged rather than propagated.

    source
    theorem NumberField.finite_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] :
    (ramifiedPrimes K).Finite

    Only finitely many primes ramify, since they all divide the nonzero integer NumberField.discr K.

    source
    theorem NumberField.ramifiedPrimes_nonempty {K : Type u_1} [Field K] [NumberField K] (h : Module.finrank ℚ K ≠ 1) :
    (ramifiedPrimes K).Nonempty

    Some prime ramifies in a number field other than ℚ. This is Minkowski's bound in the form NumberField.exists_not_isUnramifiedIn.