Ramification and inertia in cyclotomic fields

TheoremInert primes in prime cyclotomic fields#✓fully proved

Let \(\ell\) and \(p\) be distinct prime numbers, and let \(K\) be a number field that is an \(\ell\)-th cyclotomic extension of \(\mathbb{Q}\), with ring of integers \(\mathcal{O}_K\). Then the quotient ring \(\mathcal{O}_K / p\mathcal{O}_K\) is a field (that is, \(p\) is inert in \(K\)) if and only if the multiplicative order of \(p\) modulo \(\ell\) is \(\ell - 1\).

theorem isField_quotient_span_natCast_iff_orderOf_eq
    {ℓ p : ℕ} [Fact ℓ.Prime] [Fact p.Prime] (hne : p ≠ ℓ)
    (K : Type*) [Field K] [NumberField K] [IsCyclotomicExtension {ℓ} ℚ K] :
    IsField (𝓞 K ⧸ Ideal.span {(p : 𝓞 K)}) ↔ orderOf (p : ZMod ℓ) = ℓ - 1

TheoremCyclotomic fields are unramified at primes not dividing \(m\)#✓fully proved

Let \(m \ge 1\) and let \(p\) be a prime number with \(p \nmid m\). If \(K\) is a number field that is an \(m\)-th cyclotomic extension of \(\mathbb{Q}\) (that is, \(K = \mathbb{Q}(\zeta_m)\) for a primitive \(m\)-th root of unity \(\zeta_m\)), then \(p\) is unramified in \(K\): every prime ideal of the ring of integers \(\mathcal{O}_K\) lying over \(p\mathbb{Z}\) is unramified over \(\mathbb{Z}\).

theorem isUnramifiedIn_of_not_dvd
    {m p : ℕ} [NeZero m] (hp : p.Prime)
    (K : Type*) [Field K] [NumberField K]
    [IsCyclotomicExtension {m} ℚ K] (hm : ¬ p ∣ m) :
    Algebra.IsUnramifiedIn (𝓞 K) (Ideal.span {(p : ℤ)})

Used by 2

Used bySubfields of a \(p\)-power cyclotomic field unramified at \(p\) are trivial · The \(p\)-free part of \(m\) gives a cyclotomic field unramified at \(p\)

TheoremThe \(p\)-free part of \(m\) gives a cyclotomic field unramified at \(p\)#✓fully proved

Let \(m \ge 1\), let \(p\) be a prime number, and let \(m'\) be \(m\) divided by the largest power of \(p\) dividing it, so that \(m = p^a m'\) for some \(a \ge 0\) with \(p \nmid m'\). Then \(p\) is unramified in the \(m'\)-th cyclotomic field \(\mathbb{Q}(\zeta_{m'})\), where \(\zeta_{m'}\) is a primitive \(m'\)-th root of unity: every prime ideal of its ring of integers lying over \(p\mathbb{Z}\) is unramified over \(\mathbb{Z}\).

theorem isUnramifiedIn_divMaxPow
    (m p : ℕ) [NeZero m] (hp : p.Prime) :
    Algebra.IsUnramifiedIn
      (𝓞 (CyclotomicField (Nat.divMaxPow m p) ℚ))
      (Ideal.span {(p : ℤ)})

Uses 1

Proof usesCyclotomic fields are unramified at primes not dividing \(m\)

TheoremSubfields of a \(p\)-power cyclotomic field unramified at \(p\) are trivial#✓fully proved

Let \(p\) be a prime number, \(e \ge 0\) an integer and \(L\) a number field. Let \(E_1\) and \(F\) be subfields of \(L\) such that \(E_1\) is a \(p^e\)-th cyclotomic extension of \(\mathbb{Q}\) and \(F \subseteq E_1\). If \(p\) is unramified in \(F\), that is, every prime ideal of the ring of integers \(\mathcal{O}_F\) lying over \(p\mathbb{Z}\) is unramified over \(\mathbb{Z}\), then \(F = \mathbb{Q}\).

theorem eq_bot_of_isUnramifiedIn_prime_pow
    {p e : ℕ} (hp : p.Prime)
    (L : Type*) [Field L] [NumberField L]
    (E₁ : IntermediateField ℚ L) [IsCyclotomicExtension {p ^ e} ℚ E₁]
    (F : IntermediateField ℚ L) (hFE₁ : F ≤ E₁)
    (hF : Algebra.IsUnramifiedIn (𝓞 F) (Ideal.span {(p : ℤ)})) :
    F = ⊥

Sources

• the prime-power vanishing step of the N390 maximality argument (cyclotomic_ppow_unramified_le_bot in the primary source), which takes \(e\) to be the exponent of \(p\) in a positive integer \(m\) and \(L = \mathbb{Q}(\zeta_m)\) for a primitive \(m\)-th root of unity \(\zeta_m\); here \(e\) and \(L\) are arbitrary.

Uses 2

Proof usesCyclotomic fields are unramified at primes not dividing \(m\) · Unramifiedness descends to smaller intermediate fields

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.