Places of a number field extension lying over a fixed finite place

DefinitionFinite places lying over a finite place#✓fully proved

Let \(L/K\) be an extension of number fields and let \(v\) be a finite place of \(K\), given as a height-one prime of the ring of integers \(\mathcal{O}_K\). The finite places of \(L\) lying over \(v\) form the type of height-one primes \(w\) of \(\mathcal{O}_L\) that lie over \(v\), that is, whose preimage in \(\mathcal{O}_K\) is \(v\).

def placesOver (v : HeightOneSpectrum (𝓞 K)) (L : Type*) [Field L] [NumberField L]
    [Algebra K L] : Type _ :=
  { w : HeightOneSpectrum (𝓞 L) // w.asIdeal.LiesOver v.asIdeal }

Used by 13

Used byComponent at a place of the completion tensor product map · The completion tensor product map · Global norm as a product of local norms · Global trace as a sum of local traces · Places over a finite place correspond to primes over it · Base change to a finite completion as a product of completions · The canonical map to the product of completions is bijective · The canonical map to the product of completions is injective · Tensor product decomposition at a finite place · Coordinate law for the tensor product decomposition · Tensor product decomposition at a finite place over the base field · Dimension count for the base change to a finite completion · Local degrees sum to the global degree

DefinitionPlaces over a finite place correspond to primes over it#✓fully proved

Let \(L/K\) be an extension of number fields and let \(v\) be a finite place of \(K\), given as a height-one prime of the ring of integers \(\mathcal{O}_K\). Sending a finite place \(w\) of \(L\) lying over \(v\) to its prime ideal of \(\mathcal{O}_L\) is a bijection from the finite places of \(L\) lying over \(v\) onto the set of prime ideals of \(\mathcal{O}_L\) lying over \(v\).

noncomputable def placesOverEquivPrimesOver (v : HeightOneSpectrum (𝓞 K)) (L : Type*)
    [Field L] [NumberField L] [Algebra K L] :
    v.placesOver L ≃ v.asIdeal.primesOver (𝓞 L) :=
  { toFun := fun w => ⟨w.val.asIdeal, w.val.isPrime, w.property⟩
    invFun := fun Q =>
      ⟨⟨Q.val, Q.property.1, Ideal.ne_bot_of_mem_primesOver v.ne_bot Q.property⟩,
        Q.property.2⟩
    left_inv := fun _w => Subtype.ext (HeightOneSpectrum.ext rfl)
    right_inv := fun _Q => Subtype.ext rfl }

Uses 1 · Used by 4

Statement usesFinite places lying over a finite place

Used byThe canonical map to the product of completions is bijective · The canonical map to the product of completions is injective · Dimension count for the base change to a finite completion · Local degrees sum to the global degree

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.