Completions of number fields at finite places

• Valuation formula for maps between finite-place completions
• Ramification index under finite-place completion
• Explicit residue-field naturality square
• Places of a number field extension lying over a fixed finite place
• Finite-place completion tensor product maps
• The finite-place completion tensor product
• Global norm and trace as products and sums over finite-place completions

TheoremLocal degree is at most the global degree#✓fully proved

Let \(L/K\) be an extension of number fields, let \(v\) be a nonzero prime ideal of \(\mathcal{O}_K\) (a finite place of \(K\)) and let \(w\) be a nonzero prime ideal of \(\mathcal{O}_L\) lying over \(v\). Regard the \(w\)-adic completion \(L_w\) as an algebra over the \(v\)-adic completion \(K_v\) via the canonical map \(K_v \to L_w\). Then the dimension of \(L_w\) over \(K_v\) is at most \([L : K]\).

theorem finrank_adicCompletion_le :
    Module.finrank (v.adicCompletion K) (w.adicCompletion L) ≤
      Module.finrank K L

TheoremMaximal ideals of completed integer rings lie over each other#✓fully proved

Let \(L/K\) be an extension of number fields, let \(v\) be a nonzero prime ideal of \(\mathcal{O}_K\) and \(w\) a nonzero prime ideal of \(\mathcal{O}_L\) lying over \(v\). Let \(\mathcal{O}_{K_v}\) and \(\mathcal{O}_{L_w}\) be the rings of integers of the completions \(K_v\) and \(L_w\). Then the preimage of the maximal ideal of \(\mathcal{O}_{L_w}\) under the canonical map \(\mathcal{O}_{K_v} \to \mathcal{O}_{L_w}\) is the maximal ideal of \(\mathcal{O}_{K_v}\).

theorem comap_maximalIdeal_adicCompletionIntegersMap :
    Ideal.comap (adicCompletionIntegersMap v w)
      (IsLocalRing.maximalIdeal (w.adicCompletionIntegers L)) =
      IsLocalRing.maximalIdeal (v.adicCompletionIntegers K)

Uses 2 · Used by 5

Statement usesRestriction of the completion map to the rings of integers

Proof usesValuation of the image under the completion map

Used byResidue map of completed integer rings · Naturality of the residue field identifications · The local degree is the product of ramification index and inertia degree · Completion preserves the inertia degree · Completion preserves the ramification index

TheoremCompletion preserves the inertia degree#✓fully proved

Let \(L/K\) be an extension of number fields, let \(v\) be a nonzero prime ideal of \(\mathcal{O}_K\) and \(w\) a nonzero prime ideal of \(\mathcal{O}_L\) lying over \(v\). Let \(\mathcal{O}_{K_v}\) and \(\mathcal{O}_{L_w}\) be the rings of integers of the completions \(K_v\) and \(L_w\), with \(\mathcal{O}_{L_w}\) an algebra over \(\mathcal{O}_{K_v}\) via the canonical map. Then the inertia degree of the maximal ideal of \(\mathcal{O}_{L_w}\) over \(\mathcal{O}_{K_v}\) equals the inertia degree of \(w\) over \(v\).

theorem inertiaDeg_adicCompletionIntegersMap :
    (IsLocalRing.maximalIdeal (w.adicCompletionIntegers L)).inertiaDeg
      (v.adicCompletionIntegers K) =
      w.asIdeal.inertiaDeg (𝓞 K)

Uses 4 · Used by 1

Statement usesRestriction of the completion map to the rings of integers

Proof usesMaximal ideals of completed integer rings lie over each other · Residue field of the completion · Naturality of the residue field identifications

Used byThe local degree is the product of ramification index and inertia degree

TheoremThe local degree is the product of ramification index and inertia degree#✓fully proved

Let \(L/K\) be an extension of number fields, let \(v\) be a nonzero prime ideal of \(\mathcal{O}_K\) (a finite place of \(K\)) and \(w\) a nonzero prime ideal of \(\mathcal{O}_L\) lying over \(v\). Regard the completion \(L_w\) as an algebra over \(K_v\) via the canonical map \(K_v \to L_w\). Then the dimension of \(L_w\) over \(K_v\) equals \(e(w \mid v) \, f(w \mid v)\), the ramification index of \(w\) over \(v\) times the inertia degree of \(w\) over \(v\).

theorem finrank_adicCompletion_eq_ramificationIdx_mul_inertiaDeg :
    Module.finrank (v.adicCompletion K) (w.adicCompletion L) =
      w.asIdeal.ramificationIdx (𝓞 K) * w.asIdeal.inertiaDeg (𝓞 K)

Uses 7 · Used by 1

Proof usesRestriction of the completion map to the rings of integers · The map of completed integer rings is injective · Maximal ideals of completed integer rings lie over each other · Finite residue field of a completed number ring · Completion preserves the inertia degree · Completion preserves the ramification index · Valuation rings dominating a complete DVR are finite over it

Used byLocal degrees sum to the global degree

TheoremThe completed integer map is compatible with the rings of integers#✓fully proved

Let \(L/K\) be an extension of number fields, let \(v\) be a nonzero prime ideal of \(\mathcal{O}_K\) and \(w\) a nonzero prime ideal of \(\mathcal{O}_L\) lying over \(v\). Let \(\mathcal{O}_{K_v}\) and \(\mathcal{O}_{L_w}\) be the rings of integers of the completions \(K_v\) and \(L_w\). For every \(a \in \mathcal{O}_K\), the canonical map \(\mathcal{O}_{K_v} \to \mathcal{O}_{L_w}\) sends the image of \(a\) in \(\mathcal{O}_{K_v}\) to the image in \(\mathcal{O}_{L_w}\) of the image of \(a\) in \(\mathcal{O}_L\).

theorem adicCompletionIntegersMap_algebraMap (a : 𝓞 K) :
    (adicCompletionIntegersMap v w)
      (algebraMap (𝓞 K) (v.adicCompletionIntegers K) a) =
      algebraMap (𝓞 L) (w.adicCompletionIntegers L)
        (algebraMap (𝓞 K) (𝓞 L) a)

Uses 1 · Used by 1

Statement usesRestriction of the completion map to the rings of integers

Used byNaturality of the residue field identifications

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.