Completions of Dedekind domains at primes

TheoremExtension of a prime to the completed valuation ring#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(v\) be a height-one prime of \(A\), and let \(\mathcal{O}_v\) be the valuation ring of the \(v\)-adic completion of \(K\). Then the ideal of \(\mathcal{O}_v\) generated by the image of \(v\) under the canonical map \(A \to \mathcal{O}_v\) is the maximal ideal of \(\mathcal{O}_v\).

theorem map_asIdeal_eq_maximalIdeal (v : HeightOneSpectrum A) :
    Ideal.map (algebraMap A ↥(v.adicCompletionIntegers K)) v.asIdeal =
      IsLocalRing.maximalIdeal ↥(v.adicCompletionIntegers K)

DefinitionResidue map to the completed residue field#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(\mathfrak{p}\) be a height-one prime of \(A\), and let \(\mathcal{O}_\mathfrak{p}\) be the valuation ring of the \(\mathfrak{p}\)-adic completion of \(K\), with maximal ideal \(\mathfrak{m}_\mathfrak{p}\). The residue map is the ring homomorphism \(A \to \mathcal{O}_\mathfrak{p}/\mathfrak{m}_\mathfrak{p}\) obtained by composing the canonical map \(A \to \mathcal{O}_\mathfrak{p}\) with the quotient map \(\mathcal{O}_\mathfrak{p} \to \mathcal{O}_\mathfrak{p}/\mathfrak{m}_\mathfrak{p}\).

noncomputable def completionResidueMap :
    A →+* (𝔭.adicCompletionIntegers K ⧸
      IsLocalRing.maximalIdeal (𝔭.adicCompletionIntegers K)) :=
  (Ideal.Quotient.mk (IsLocalRing.maximalIdeal (𝔭.adicCompletionIntegers K))).comp
    (algebraMap A (𝔭.adicCompletionIntegers K))

Used by 4

Used byNaturality of the residue field identifications · Residue field of the completion · Kernel of the completed residue map · Surjectivity of the completed residue map

TheoremKernel of the completed residue map#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(\mathfrak{p}\) be a height-one prime of \(A\), and let \(\mathcal{O}_\mathfrak{p}\) be the valuation ring of the \(\mathfrak{p}\)-adic completion of \(K\), with maximal ideal \(\mathfrak{m}_\mathfrak{p}\). The kernel of the residue map \(A \to \mathcal{O}_\mathfrak{p}/\mathfrak{m}_\mathfrak{p}\), the canonical map \(A \to \mathcal{O}_\mathfrak{p}\) followed by the quotient map, is \(\mathfrak{p}\).

theorem ker_completionResidueMap :
    RingHom.ker (𝔭.completionResidueMap (K := K)) = 𝔭.asIdeal

Uses 1 · Used by 2

Statement usesResidue map to the completed residue field

Used byNaturality of the residue field identifications · Residue field of the completion

TheoremSurjectivity of the completed residue map#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(\mathfrak{p}\) be a height-one prime of \(A\), and let \(\mathcal{O}_\mathfrak{p}\) be the valuation ring of the \(\mathfrak{p}\)-adic completion of \(K\), with maximal ideal \(\mathfrak{m}_\mathfrak{p}\). The residue map \(A \to \mathcal{O}_\mathfrak{p}/\mathfrak{m}_\mathfrak{p}\), the canonical map \(A \to \mathcal{O}_\mathfrak{p}\) followed by the quotient map, is surjective.

theorem surjective_completionResidueMap :
    Function.Surjective (𝔭.completionResidueMap (K := K))

Uses 1 · Used by 2

Statement usesResidue map to the completed residue field

Used byNaturality of the residue field identifications · Residue field of the completion

DefinitionResidue field of the completion#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(\mathfrak{p}\) be a height-one prime of \(A\), and let \(\mathcal{O}_\mathfrak{p}\) be the valuation ring of the \(\mathfrak{p}\)-adic completion of \(K\), with maximal ideal \(\mathfrak{m}_\mathfrak{p}\). This is the ring isomorphism \(\mathcal{O}_\mathfrak{p}/\mathfrak{m}_\mathfrak{p} \cong A/\mathfrak{p}\) that sends the residue class of the image of each \(a \in A\) to the class of \(a\) modulo \(\mathfrak{p}\). It is induced by the residue map \(A \to \mathcal{O}_\mathfrak{p}/\mathfrak{m}_\mathfrak{p}\) (the canonical map \(A \to \mathcal{O}_\mathfrak{p}\) followed by the quotient map), which is surjective with kernel \(\mathfrak{p}\).

noncomputable def completionResidueFieldEquiv :
    (↥(𝔭.adicCompletionIntegers K) ⧸
      IsLocalRing.maximalIdeal ↥(𝔭.adicCompletionIntegers K)) ≃+* (A ⧸ 𝔭.asIdeal) :=
  (RingHom.quotientKerEquivOfSurjective
    (𝔭.surjective_completionResidueMap (K := K))).symm.trans
    (Ideal.quotEquivOfEq (𝔭.ker_completionResidueMap (K := K)))

Uses 3 · Used by 4

Statement usesResidue map to the completed residue field · Kernel of the completed residue map · Surjectivity of the completed residue map

Used byFinite residue field of a completed number ring · Naturality of the residue field identifications · Completion preserves the inertia degree · Finite residue field of adic completion integers

TheoremLocalization at a prime as a preimage of the completed valuation ring#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\), let \(v\) be a height-one prime of \(R\), and let \(\mathcal{O}_v\) be the valuation ring of the \(v\)-adic completion \(K_v\) of \(K\). Then the localization \(R_v\) of \(R\) at \(v\), viewed as a subring of \(K\), is the preimage of \(\mathcal{O}_v\) under the canonical embedding \(K \to K_v\).

theorem valuationSubringAtPrime_eq_comap_adicCompletionIntegers (v : HeightOneSpectrum R) :
    (valuationSubringAtPrime (K := K) v).toSubring =
      Subring.comap (algebraMap K (adicCompletion K v))
        (adicCompletionIntegers K v).toSubring

TheoremFinite residue field of adic completion integers#✓fully proved

The residue field of the adic completion integers at a place with finite residue field is finite.

theorem finite_residueField_adicCompletionIntegers (K : Type v) [Field K] [Algebra R K]
    [IsFractionRing R K] (v : HeightOneSpectrum R) [Finite (R ⧸ v.asIdeal)] :
    Finite (IsLocalRing.ResidueField (v.adicCompletionIntegers K))

Uses 1

Proof usesResidue field of the completion

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.