Ramification index under finite-place completion

TheoremThe map of completed integer rings is injective#✓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\). Then the canonical map \(\mathcal{O}_{K_v} \to \mathcal{O}_{L_w}\) from the ring of integers of the completion \(K_v\) to the ring of integers of the completion \(L_w\) is injective.

theorem adicCompletionIntegersMap_injective :
    Function.Injective (adicCompletionIntegersMap v w)

noncomputable def adicCompletionIntegersMap :
    v.adicCompletionIntegers K →+* w.adicCompletionIntegers L where
  toFun x := ⟨adicCompletionMap v w x.val, adicCompletionMap_mem_integers v w x.val x.property⟩
  map_one' := Subtype.ext (map_one _)
  map_mul' := fun _x _y => Subtype.ext (map_mul _ _ _)
  map_zero' := Subtype.ext (map_zero _)
  map_add' := fun _x _y => Subtype.ext (map_add _ _ _)

MathlibExt/NumberTheory/NumberField/Completion/FiniteLiesOverValuation.lean:108

Uses 1 · Used by 2

Statement usesRestriction of the completion map to the rings of integers

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

TheoremCompletion preserves the ramification index#✓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 ramification index of the maximal ideal of \(\mathcal{O}_{L_w}\) over \(\mathcal{O}_{K_v}\) equals the ramification index of \(w\) over \(v\).

theorem ramificationIdx_adicCompletionIntegersMap :
    (IsLocalRing.maximalIdeal (w.adicCompletionIntegers L)).ramificationIdx
      (v.adicCompletionIntegers K) =
      w.asIdeal.ramificationIdx (𝓞 K)

Uses 5 · Used by 1

Statement usesRestriction of the completion map to the rings of integers

Proof usesThe map of completed integer rings is injective · Maximal ideals of completed integer rings lie over each other · Valuation of the image under the completion map · Additive valuations scale by the ramification index

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

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.