Valuation formula for maps between finite-place completions

TheoremValuation of the image under the completion map#✓fully proved

Let \(L/K\) be an extension of number fields, let \(v\) be a finite place of \(K\), given as a height-one prime of the ring of integers \(\mathcal{O}_K\), let \(w\) be a finite place of \(L\) lying over \(v\), and let \(e\) be the ramification index of \(w\) over \(v\). Let \(\iota : K_v \to L_w\) be the continuous ring homomorphism between the completions that extends \(K \to L\). Then for every \(x \in K_v\), the valuation of \(\iota(x)\) on \(L_w\) equals the \(e\)-th power of the valuation of \(x\) on \(K_v\), where both valuations are the multiplicative adic valuations extended to the completions.

theorem valuation_adicCompletionMap (x : v.adicCompletion K) :
    Valued.v (adicCompletionMap v w x) =
      Valued.v x ^ v.asIdeal.ramificationIdx' w.asIdeal

Used by 3

Used byMaximal ideals of completed integer rings lie over each other · Completion preserves the ramification index · The completion map preserves integrality

TheoremThe completion map preserves integrality#✓fully proved

Let \(L/K\) be an extension of number fields, let \(v\) be a finite place of \(K\), given as a height-one prime of the ring of integers \(\mathcal{O}_K\), and let \(w\) be a finite place of \(L\) lying over \(v\). The continuous ring homomorphism \(K_v \to L_w\) between the completions that extends \(K \to L\) maps every element of the ring of integers of \(K_v\) into the ring of integers of \(L_w\).

theorem adicCompletionMap_mem_integers (x : v.adicCompletion K)
    (hx : x ∈ v.adicCompletionIntegers K) :
    adicCompletionMap v w x ∈ w.adicCompletionIntegers L

Uses 1 · Used by 1

Proof usesValuation of the image under the completion map

Used byRestriction of the completion map to the rings of integers

DefinitionRestriction of the completion map to the rings of integers#✓fully proved

Let \(L/K\) be an extension of number fields, let \(v\) be a finite place of \(K\), given as a height-one prime of the ring of integers \(\mathcal{O}_K\), and let \(w\) be a finite place of \(L\) lying over \(v\). Let \(K_v\) and \(L_w\) be the completions, with rings of integers \(\mathcal{O}_v\) and \(\mathcal{O}_w\). The continuous ring homomorphism \(K_v \to L_w\) extending \(K \to L\) restricts to a ring homomorphism \(\mathcal{O}_v \to \mathcal{O}_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 _ _ _)

Uses 1 · Used by 8

Statement usesThe completion map preserves integrality

Used byThe completed integer map is compatible with the rings of integers · Maximal ideals of completed integer rings lie over each other · Residue 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 · The map of completed integer rings is injective · Completion preserves the ramification index

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.