Ramification of cyclotomic extensions

TheoremWithout primitive \(p\)-th roots of unity, every \(p\)-th root of unity is trivial#✓fully proved

Let \(p\) be a prime and let \(L\) be a field containing no primitive \(p\)-th root of unity. Then every \(\eta \in L\) with \(\eta^p = 1\) equals \(1\).

The order of \(\eta\) divides the prime \(p\), so it is \(1\) or \(p\), and \(p\) is excluded.

theorem pth_root_unity_eq_one_of_no_prim_root
    (L : Type*) [Field L] (p : ℕ) [hp : Fact (Nat.Prime p)]
    (hno : ∀ ω : L, ¬IsPrimitiveRoot ω p)
    (η : L) (hη : η ^ p = 1) : η = 1

Used by 1

Used byOver a complete base with maximal ideal \((p)\) and no primitive \(p\)-th root of unity, an index-one extension has no nontrivial \(p\)-th roots of unity

TheoremNo primitive p-th root in an unramified DVR extension#✓fully proved

For a complete DVR base whose maximal ideal is generated by p, a primitive p-th root cannot appear in an index-one DVR extension: if the residue characteristic is p, (p) is the maximal ideal, the ramification index is 1, and the base field has no primitive p-th root, then neither does the extension.

The proof is the valuation argument: a primitive root b ∈ B reduces to 1 in the residue field (characteristic p), so each factor 1 - b ^ (k + 1) lies in the maximal ideal, while their product is exactly p; hence p ∈ 𝔪_B ^ (p - 1), which forces p ∈ 𝔪_B ^ 2, contradicting ramification index 1 (for p = 2 the argument is replaced by the observation that -1 would be a primitive square root in the base field).

no_prim_root_in_unramified_ext_of_prime_spans_maximal_ideal · 16 lines

theorem no_prim_root_in_unramified_ext_of_prime_spans_maximal_ideal
    (A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    (K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
    [Fintype (IsLocalRing.ResidueField A)]
    (p : ℕ) [hp : Fact (Nat.Prime p)]
    [CharP (IsLocalRing.ResidueField A) p]
    (L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
    (B : Type*) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
    [Algebra A B] [Algebra B L] [Algebra A L] [IsFractionRing B L]
    [IsScalarTower A B L] [IsScalarTower A K L]
    (habsunram : Ideal.span {(↑p : A)} = IsLocalRing.maximalIdeal A)
    (he : Ideal.ramificationIdx' (IsLocalRing.maximalIdeal A)
      (IsLocalRing.maximalIdeal B) = 1)
    (hnoroot : ∀ ω : K, ¬IsPrimitiveRoot ω p)
    (ω : L) : ¬IsPrimitiveRoot ω p

Used by 1

Used byOver a complete base with maximal ideal \((p)\) and no primitive \(p\)-th root of unity, an index-one extension has no nontrivial \(p\)-th roots of unity

TheoremOver a complete base with maximal ideal \((p)\) and no primitive \(p\)-th root of unity, an index-one extension has no nontrivial \(p\)-th roots of unity#✓fully proved

Over a complete base with maximal ideal \((p)\) and no primitive \(p\)-th root of unity, an index-one extension has no nontrivial \(p\)-th roots of unity. Let \(A\) be a discrete valuation ring, complete with respect to its maximal ideal \(\mathfrak m_A\), with fraction field \(K\) and finite residue field of characteristic a prime \(p\), and suppose \(\mathfrak m_A = (p)\). Let \(L\) be a finite extension of \(K\), and let \(B\) be a discrete valuation ring with fraction field \(L\) and an \(A\)-algebra structure such that the maps \(A \to B \to L\) and \(A \to K \to L\) agree. Suppose the ramification index of the maximal ideal \(\mathfrak m_B\) of \(B\) over \(\mathfrak m_A\) (the largest \(n\) with \(\mathfrak m_A B \subseteq \mathfrak m_B^n\)) is \(1\). If \(K\) contains no primitive \(p\)-th root of unity, then every \(\eta \in L\) with \(\eta^p = 1\) equals \(1\).

no_prim_pth_root_in_unramified_ext_of_prime_spans_maximal_ideal · 16 lines

theorem no_prim_pth_root_in_unramified_ext_of_prime_spans_maximal_ideal
    (A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    (K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
    [Fintype (IsLocalRing.ResidueField A)]
    (p : ℕ) [hp : Fact (Nat.Prime p)]
    [CharP (IsLocalRing.ResidueField A) p]
    (L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
    (B : Type*) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
    [Algebra A B] [Algebra B L] [Algebra A L] [IsFractionRing B L]
    [IsScalarTower A B L] [IsScalarTower A K L]
    (habsunram : Ideal.span {(↑p : A)} = IsLocalRing.maximalIdeal A)
    (he : Ideal.ramificationIdx' (IsLocalRing.maximalIdeal A)
      (IsLocalRing.maximalIdeal B) = 1)
    (hnoroot : ∀ ω : K, ¬IsPrimitiveRoot ω p)
    (η : L) (hη : η ^ p = 1) : η = 1

Uses 2 · Used by 1

Proof usesNo primitive p-th root in an unramified DVR extension · Without primitive \(p\)-th roots of unity, every \(p\)-th root of unity is trivial

Used byOver a complete base with maximal ideal \((p)\), the \(p\)-th roots of unity in an index-one extension come from the base

TheoremOver a complete base with maximal ideal \((p)\), the \(p\)-th roots of unity in an index-one extension come from the base#✓fully proved

Over a complete base with maximal ideal \((p)\), the \(p\)-th roots of unity in an index-one extension come from the base. Let \(A\) be a discrete valuation ring, complete with respect to its maximal ideal \(\mathfrak m_A\), with fraction field \(K\) and finite residue field of characteristic a prime \(p\), and suppose \(\mathfrak m_A = (p)\). Let \(L\) be a finite extension of \(K\), and let \(B\) be a discrete valuation ring with fraction field \(L\) and an \(A\)-algebra structure such that the maps \(A \to B \to L\) and \(A \to K \to L\) agree. Suppose the ramification index of the maximal ideal \(\mathfrak m_B\) of \(B\) over \(\mathfrak m_A\) (the largest \(n\) with \(\mathfrak m_A B \subseteq \mathfrak m_B^n\)) is \(1\). Then every \(\eta \in L\) with \(\eta^p = 1\) is the image of an element of \(K\).

unramified_pth_root_in_base_of_prime_spans_maximal_ideal · 16 lines

theorem unramified_pth_root_in_base_of_prime_spans_maximal_ideal
    (A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    (K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
    [Fintype (IsLocalRing.ResidueField A)]
    (p : ℕ) [hp : Fact (Nat.Prime p)]
    [CharP (IsLocalRing.ResidueField A) p]
    (L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
    (B : Type*) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
    [Algebra A B] [Algebra B L] [Algebra A L] [IsFractionRing B L]
    [IsScalarTower A B L] [IsScalarTower A K L]
    (habsunram : Ideal.span {(↑p : A)} = IsLocalRing.maximalIdeal A)
    (he : Ideal.ramificationIdx' (IsLocalRing.maximalIdeal A)
      (IsLocalRing.maximalIdeal B) = 1)
    (η : L) (hη : η ^ p = 1) :
    ∃ ζ : K, algebraMap K L ζ = η

Uses 1 · Used by 1

Proof usesOver a complete base with maximal ideal \((p)\) and no primitive \(p\)-th root of unity, an index-one extension has no nontrivial \(p\)-th roots of unity

Used byOver a complete base with maximal ideal \((p)\) and no nontrivial \(p\)-th roots of unity, cyclotomic extensions of order divisible by \(p\) ramify

TheoremOver a complete base with maximal ideal \((p)\) and no nontrivial \(p\)-th roots of unity, cyclotomic extensions of order divisible by \(p\) ramify#✓fully proved

Over a complete base with maximal ideal \((p)\) and no nontrivial \(p\)-th roots of unity, cyclotomic extensions of order divisible by \(p\) ramify. Let \(A\) be a discrete valuation ring, complete with respect to its maximal ideal \(\mathfrak m_A\), with fraction field \(K\) and finite residue field of characteristic a prime \(p\), and suppose \(\mathfrak m_A = (p)\). Suppose \(1\) is the only \(p\)-th root of unity in \(K\). Let \(m > 0\) be divisible by \(p\), let \(L\) be an \(m\)-th cyclotomic extension of \(K\) that is finite over \(K\), and let \(B\) be a discrete valuation ring with fraction field \(L\) and an \(A\)-algebra structure such that the maps \(A \to B \to L\) and \(A \to K \to L\) agree. Then the ramification index of the maximal ideal \(\mathfrak m_B\) of \(B\) over \(\mathfrak m_A\) (the largest \(n\) with \(\mathfrak m_A B \subseteq \mathfrak m_B^n\)) is not \(1\).

dvr_pth_root_ramified_of_prime_spans_maximal_ideal · 18 lines

theorem dvr_pth_root_ramified_of_prime_spans_maximal_ideal
    (A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    (K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
    (p : ℕ) [hp : Fact (Nat.Prime p)]
    [Fintype (IsLocalRing.ResidueField A)]
    [CharP (IsLocalRing.ResidueField A) p]
    (hno_prim : ∀ ζ : K, ζ ^ p = 1 → ζ = 1)
    (m : ℕ) (hm : 0 < m) (hdvd : p ∣ m)
    (L : Type*) [Field L] [Algebra K L]
    [IsCyclotomicExtension {m} K L]
    [FiniteDimensional K L]
    (B : Type*) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
    [Algebra A B] [Algebra B L] [Algebra A L] [IsFractionRing B L]
    [IsScalarTower A B L] [IsScalarTower A K L]
    (habsunram : Ideal.span {(↑p : A)} = IsLocalRing.maximalIdeal A) :
    Ideal.ramificationIdx' (IsLocalRing.maximalIdeal A)
      (IsLocalRing.maximalIdeal B) ≠ 1

Sources

• ATLAS NumberTheoryI, Section 10.2, Corollary 10.18, a special case of the ramified implication: the source does not assume \(\mathfrak m_A = (p)\), and the converse is not proved.

Uses 1

Proof usesOver a complete base with maximal ideal \((p)\), the \(p\)-th roots of unity in an index-one extension come from the base

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.