Explicit residue-field naturality square

DefinitionResidue map of 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\). This is the ring homomorphism \(\mathcal{O}_K/v \to \mathcal{O}_L/w\) induced by the canonical map \(\mathcal{O}_K \to \mathcal{O}_L\).

noncomputable def ringOfIntegersResidueQuotientMap :
    𝓞 K ⧸ v.asIdeal →+* 𝓞 L ⧸ w.asIdeal :=
  Ideal.quotientMap w.asIdeal (algebraMap (𝓞 K) (𝓞 L)) (Ideal.over_def w.asIdeal v.asIdeal).le

Used by 1

Used byNaturality of the residue field identifications

DefinitionResidue map of completed integer rings#✓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 maximal ideals \(\mathfrak{m}_v\) and \(\mathfrak{m}_w\). This is the ring homomorphism \(\mathcal{O}_{K_v}/\mathfrak{m}_v \to \mathcal{O}_{L_w}/\mathfrak{m}_w\) induced by the canonical map \(\mathcal{O}_{K_v} \to \mathcal{O}_{L_w}\).

noncomputable def adicCompletionResidueQuotientMap :
    (↥(v.adicCompletionIntegers K) ⧸
      IsLocalRing.maximalIdeal ↥(v.adicCompletionIntegers K)) →+*
      (↥(w.adicCompletionIntegers L) ⧸
        IsLocalRing.maximalIdeal ↥(w.adicCompletionIntegers L)) :=
  Ideal.quotientMap (IsLocalRing.maximalIdeal (w.adicCompletionIntegers L))
    (adicCompletionIntegersMap v w)
    (comap_maximalIdeal_adicCompletionIntegersMap v w).ge

Uses 2 · Used by 1

Statement usesRestriction of the completion map to the rings of integers · Maximal ideals of completed integer rings lie over each other

Used byNaturality of the residue field identifications

TheoremNaturality of the residue field identifications#✓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 maximal ideals \(\mathfrak{m}_v\) and \(\mathfrak{m}_w\). Then the two maps \(\mathcal{O}_{K_v}/\mathfrak{m}_v \to \mathcal{O}_L/w\) agree: the residue field isomorphism \(\mathcal{O}_{K_v}/\mathfrak{m}_v \cong \mathcal{O}_K/v\) followed by the map \(\mathcal{O}_K/v \to \mathcal{O}_L/w\) induced by \(\mathcal{O}_K \to \mathcal{O}_L\), and the map \(\mathcal{O}_{K_v}/\mathfrak{m}_v \to \mathcal{O}_{L_w}/\mathfrak{m}_w\) induced by the canonical map \(\mathcal{O}_{K_v} \to \mathcal{O}_{L_w}\) followed by the residue field isomorphism \(\mathcal{O}_{L_w}/\mathfrak{m}_w \cong \mathcal{O}_L/w\).

theorem completionResidueFieldEquiv_naturality :
    (ringOfIntegersResidueQuotientMap v w).comp
      (completionResidueFieldEquiv v).toRingHom =
    (completionResidueFieldEquiv w).toRingHom.comp
      (adicCompletionResidueQuotientMap v w)

Uses 9 · Used by 1

Statement usesResidue map of completed integer rings · Residue field of the completion · Residue map of rings of integers

Proof usesRestriction of the completion map to the rings of integers · The completed integer map is compatible with the rings of integers · Maximal ideals of completed integer rings lie over each other · Residue map to the completed residue field · Kernel of the completed residue map · Surjectivity of the completed residue map

Used byCompletion preserves the inertia degree

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.