Multiplicities of ideals in a completed integer ring

Extending an ideal of a Dedekind domain to the integer ring of its completion preserves its multiplicity at the selected prime. The prime generates the maximal ideal of the completion, so its ramification index in this extension is one. This comparison lets coefficients of global ideals be read in the completed ring.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.multiplicity_map_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (I : Ideal R) (hI : I ≠ ⊥) : multiplicity (IsLocalRing.maximalIdeal ↥(adicCompletionIntegers K v)) (Ideal.map (algebraMap R ↥(adicCompletionIntegers K v)) I) = multiplicity v.asIdeal I

The coefficient at v of a nonzero ideal equals the coefficient at the maximal ideal after extension to the integer ring of the v-adic completion.