Ramification index and inertia degree

TheoremBounds on the ramification index#✓fully proved

Let \(R\) and \(S\) be Dedekind domains, with \(S\) an \(R\)-algebra that is finitely generated and torsion-free as an \(R\)-module, and let \(n\) be the rank of \(S\) as an \(R\)-module. If \(\mathfrak{p}\) is a maximal ideal of \(R\) and \(\mathfrak{q}\) is a prime ideal of \(S\) lying over \(\mathfrak{p}\), then the ramification index \(e_{\mathfrak{q}}\) of \(\mathfrak{q}\) over \(\mathfrak{p}\) satisfies \(1 \le e_{\mathfrak{q}} \le n\).

theorem ramificationIdx_mem_Icc (p : Ideal R) [p.IsMaximal]
    (q : Ideal S) [q.IsPrime] [q.LiesOver p] :
    q.ramificationIdx R ∈ Set.Icc 1 (Module.finrank R S)

Sources

• ATLAS NumberTheoryI, Corollary 5.36 (the \(e_{\mathfrak{q}}\) part).

Used by 1

Used byBounds on ramification, inertia and splitting

TheoremBounds on the inertia degree#✓fully proved

Let \(R\) and \(S\) be Dedekind domains, with \(S\) an \(R\)-algebra that is finitely generated and torsion-free as an \(R\)-module, and let \(n\) be the rank of \(S\) as an \(R\)-module. If \(\mathfrak{p}\) is a maximal ideal of \(R\) and \(\mathfrak{q}\) is a prime ideal of \(S\) lying over \(\mathfrak{p}\), then the inertia degree \(f_{\mathfrak{q}}\) of \(\mathfrak{q}\) over \(\mathfrak{p}\) satisfies \(1 \le f_{\mathfrak{q}} \le n\).

theorem inertiaDeg_mem_Icc (p : Ideal R) [p.IsMaximal]
    (q : Ideal S) [q.IsPrime] [q.LiesOver p] :
    q.inertiaDeg R ∈ Set.Icc 1 (Module.finrank R S)

Sources

• ATLAS NumberTheoryI, Corollary 5.36 (the \(f_{\mathfrak{q}}\) part).

Used by 1

Used byBounds on ramification, inertia and splitting

TheoremBounds on the number of primes above a prime#✓fully proved

Let \(R\) and \(S\) be Dedekind domains, with \(S\) an \(R\)-algebra that is finitely generated and torsion-free as an \(R\)-module, and let \(n\) be the rank of \(S\) as an \(R\)-module. If \(\mathfrak{p}\) is a maximal ideal of \(R\), then the number \(g_{\mathfrak{p}}\) of prime ideals of \(S\) lying over \(\mathfrak{p}\) satisfies \(1 \le g_{\mathfrak{p}} \le n\).

theorem ncard_primesOver_mem_Icc (p : Ideal R) [p.IsMaximal] :
    (p.primesOver S).ncard ∈ Set.Icc 1 (Module.finrank R S)

Sources

• ATLAS NumberTheoryI, Corollary 5.36 (the \(g_{\mathfrak{p}}\) part).

Used by 1

Used byBounds on ramification, inertia and splitting

TheoremBounds on ramification, inertia and splitting#✓fully proved

Let \(R\) and \(S\) be Dedekind domains, with \(S\) an \(R\)-algebra that is finitely generated and torsion-free as an \(R\)-module, and let \(n\) be the rank of \(S\) as an \(R\)-module. If \(\mathfrak{p}\) is a maximal ideal of \(R\) and \(\mathfrak{q}\) is a prime ideal of \(S\) lying over \(\mathfrak{p}\), then the ramification index \(e_{\mathfrak{q}}\) and the inertia degree \(f_{\mathfrak{q}}\) of \(\mathfrak{q}\) over \(\mathfrak{p}\) and the number \(g_{\mathfrak{p}}\) of prime ideals of \(S\) lying over \(\mathfrak{p}\) all lie in the interval \([1, n]\).

theorem ramification_inertia_card_mem_Icc (p : Ideal R) [p.IsMaximal]
    (q : Ideal S) [q.IsPrime] [q.LiesOver p] :
    q.ramificationIdx R ∈ Set.Icc 1 (Module.finrank R S) ∧
      q.inertiaDeg R ∈ Set.Icc 1 (Module.finrank R S) ∧
      (p.primesOver S).ncard ∈ Set.Icc 1 (Module.finrank R S)

Sources

• ATLAS NumberTheoryI, Corollary 5.36.

Uses 3 · Used by 1

Proof usesBounds on the inertia degree · Bounds on the number of primes above a prime · Bounds on the ramification index

Used byBounds on ramification, inertia and splitting, fraction-field form

TheoremBounds on ramification, inertia and splitting, fraction-field form#✓fully proved

Let \(R\) and \(S\) be Dedekind domains, with \(S\) an \(R\)-algebra that is finitely generated and torsion-free as an \(R\)-module. Let \(K\) be the fraction field of \(R\) and \(L\) the fraction field of \(S\), with \(L\) a \(K\)-algebra compatible with the maps \(R \to K \to L\) and \(R \to S \to L\), and let \(n = [L : K]\). If \(\mathfrak{p}\) is a maximal ideal of \(R\) and \(\mathfrak{q}\) is a prime ideal of \(S\) lying over \(\mathfrak{p}\), then the ramification index \(e_{\mathfrak{q}}\) and the inertia degree \(f_{\mathfrak{q}}\) of \(\mathfrak{q}\) over \(\mathfrak{p}\) and the number \(g_{\mathfrak{p}}\) of prime ideals of \(S\) lying over \(\mathfrak{p}\) all lie in the interval \([1, n]\).

theorem ramification_inertia_card_mem_Icc_of_isFractionRing
    (K L : Type*) [Field K] [Field L] [Algebra R K] [IsFractionRing R K]
    [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L]
    [IsScalarTower R K L] [IsScalarTower R S L]
    (p : Ideal R) [p.IsMaximal] (q : Ideal S) [q.IsPrime] [q.LiesOver p] :
    q.ramificationIdx R ∈ Set.Icc 1 (Module.finrank K L) ∧
      q.inertiaDeg R ∈ Set.Icc 1 (Module.finrank K L) ∧
      (p.primesOver S).ncard ∈ Set.Icc 1 (Module.finrank K L)

Sources

• ATLAS NumberTheoryI, Corollary 5.36.

Uses 1

Proof usesBounds on ramification, inertia and splitting

TheoremThe extended maximal ideal is a power of the maximal ideal#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\), \(\mathfrak m_B\), and let \(B\) be an \(A\)-algebra that is torsion-free as an \(A\)-module and whose structure map is a local homomorphism. Let \(e\) be the ramification index of \(\mathfrak m_B\) over \(A\). Then the ideal \(\mathfrak m_A B\) of \(B\) generated by the image of \(\mathfrak m_A\) equals \(\mathfrak m_B^e\).

theorem map_maximalIdeal_eq_pow_ramificationIdx :
    Ideal.map (algebraMap A B) (maximalIdeal A) =
      maximalIdeal B ^ (maximalIdeal B).ramificationIdx A

Used by 2

Used byImages of the base maximal ideal lie in the ramification power · Totally ramified extensions are generated by an Eisenstein uniformizer

TheoremImages of the base maximal ideal lie in the ramification power#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\), \(\mathfrak m_B\), and let \(B\) be an \(A\)-algebra that is torsion-free as an \(A\)-module and whose structure map is a local homomorphism. Let \(e\) be the ramification index of \(\mathfrak m_B\) over \(A\). Then for every \(x \in \mathfrak m_A\), the image of \(x\) in \(B\) lies in \(\mathfrak m_B^e\).

theorem algebraMap_mem_maximalIdeal_pow_ramificationIdx {x : A}
    (hx : x ∈ maximalIdeal A) :
    algebraMap A B x ∈ maximalIdeal B ^ (maximalIdeal B).ramificationIdx A

Uses 1

Proof usesThe extended maximal ideal is a power of the maximal ideal

TheoremRelative norm is the base prime to the inertia degree, separable case#✓fully proved

Theorem 6.10 of ATLAS NumberTheoryI, in the separable (rather than Galois or perfect-field) form: the relative norm of a maximal ideal lying over a maximal ideal is the base prime raised to the inertia degree.

theorem relNorm_eq_pow_inertiaDeg_of_isSeparable
    {R S : Type*} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
    [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S]
    [Module.Finite R S] [Module.IsTorsionFree R S]
    [IsDedekindDomain R] [IsDedekindDomain S]
    [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
    (P : Ideal S) (p : Ideal R) [P.LiesOver p] [P.IsMaximal] [p.IsMaximal] :
    relNorm R P = p ^ P.inertiaDeg R

TheoremMultiplicity of the maximal ideal equals the additive valuation#✓fully proved

Let \(R\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) and normalized additive valuation \(v \colon R \to \mathbb{N} \cup \{\infty\}\). For every \(x \in R\), the multiplicity of \(\mathfrak{m}\) in the principal ideal \((x)\), that is, the supremum in \(\mathbb{N} \cup \{\infty\}\) of the \(n \in \mathbb{N}\) such that \(\mathfrak{m}^n\) divides \((x)\) as ideals, equals \(v(x)\).

theorem emultiplicity_maximalIdeal_span_eq_addVal
    {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (x : R) :
    emultiplicity (IsLocalRing.maximalIdeal R) (Ideal.span {x}) = addVal R x

Used by 1

Used byAdditive valuations scale by the ramification index

TheoremAdditive valuations scale by the ramification index#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings, and let \(B\) be an \(A\)-algebra that is torsion-free as an \(A\)-module and whose structure map \(\varphi \colon A \to B\) is a local homomorphism. Let \(v_A\) and \(v_B\) be the normalized additive valuations of \(A\) and \(B\), with values in \(\mathbb{N} \cup \{\infty\}\), and let \(e\) be the ramification index of the maximal ideal of \(B\) over \(A\). Then \(v_B(\varphi(x)) = e \cdot v_A(x)\) for every \(x \in A\).

theorem IsDiscreteValuationRing.addVal_algebraMap_eq_ramificationIdx_mul
    {A B : Type*} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
    [Algebra A B] [Module.IsTorsionFree A B]
    [IsLocalHom (algebraMap A B)] (x : A) :
    addVal B (algebraMap A B x) =
      ((IsLocalRing.maximalIdeal B).ramificationIdx A : ℕ∞) * addVal A x

Uses 1 · Used by 1

Proof usesMultiplicity of the maximal ideal equals the additive valuation

Used byCompletion preserves the ramification index

TheoremNatural numbers that are units in a local ring#✓fully proved

Let \(R\) be a commutative local ring and let \(p\) be the characteristic of its residue field. For every natural number \(n\), the image of \(n\) in \(R\) is a unit if and only if \(p\) does not divide \(n\).

theorem IsLocalRing.isUnit_natCast_iff_ringChar_not_dvd
    {R : Type*} [CommRing R] [IsLocalRing R] (n : ℕ) :
    IsUnit (n : R) ↔ ¬ ringChar (IsLocalRing.ResidueField R) ∣ n

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.