Local structure of an adic completion #

Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f. Exact-pin changes are documented in PORTING.md.

Let A be a Dedekind domain with fraction field K, and let v be a height-one prime of A. This file provides

IsDedekindDomain.HeightOneSpectrum.valuation_maximalIdeal_adicCompletionIntegers: the valuation associated to the height-one prime of the ring of integers 𝒪_v (a discrete valuation ring) of a completion K_v is the valuation of the completion;
the residue-field equivalence A ⧸ v ≃+* 𝒪_v ⧸ 𝔪_v;
IsDedekindDomain.HeightOneSpectrum.henselianLocalRing_adicCompletionIntegers (and the instances leading up to it): the subspace topology on 𝒪_v is the 𝔪-adic topology (isAdic_maximalIdeal_adicCompletionIntegers, via mem_maximalIdeal_pow_iff), 𝒪_v is complete, hence 𝔪-adically complete, hence a Henselian local ring.

source

theorem IsDedekindDomain.HeightOneSpectrum.valued_irreducible_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {π : ↥(adicCompletionIntegers K v)} (hπ : Irreducible π) :

Valued.v ((algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v)) π) = WithZero.exp (-1)

An irreducible element of the ring of integers of a completion has valuation exp (-1).

source

theorem IsDedekindDomain.HeightOneSpectrum.valuation_maximalIdeal_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : adicCompletion K v) :

(valuation (adicCompletion K v) (IsDiscreteValuationRing.maximalIdeal ↥(adicCompletionIntegers K v))) x = Valued.v x

The valuation associated to the maximal ideal of the ring of integers of an adic completion is the valuation of the completion.

source

theorem IsDedekindDomain.HeightOneSpectrum.span_singleton_eq_maximalIdeal_pow {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {x : ↥(adicCompletionIntegers K v)} {e : ℕ} (hx : Valued.v ((algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v)) x) = WithZero.exp (-↑e)) :

Ideal.span {x} = IsLocalRing.maximalIdeal ↥(adicCompletionIntegers K v) ^ e

An element of the ring of integers of a completion of valuation exp (-e) generates the e-th power of the maximal ideal.

source

theorem IsDedekindDomain.HeightOneSpectrum.valued_of_span_singleton_eq_maximalIdeal_pow {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {x : ↥(adicCompletionIntegers K v)} {e : ℕ} (hx : Ideal.span {x} = IsLocalRing.maximalIdeal ↥(adicCompletionIntegers K v) ^ e) :

Valued.v ((algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v)) x) = WithZero.exp (-↑e)

Conversely, a generator of the e-th power of the maximal ideal of the ring of integers of a completion has valuation exp (-e).

source

theorem IsDedekindDomain.HeightOneSpectrum.exists_valued_sub_lt_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : ↥(adicCompletionIntegers K v)) :

∃ (a : R), Valued.v (↑x - (algebraMap R (adicCompletion K v)) a) < 1

Any element of the ring of integers of the completion is congruent to an element of R modulo the maximal ideal.

source

noncomputable def IsDedekindDomain.HeightOneSpectrum.residueFieldEquivAdicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :

R ⧸ v.asIdeal ≃+* ↥(adicCompletionIntegers K v) ⧸ IsLocalRing.maximalIdeal ↥(adicCompletionIntegers K v)

The residue field of v maps isomorphically onto the residue field of the ring of integers of the completion at v.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.residueFieldEquivAdicCompletionIntegers_mk {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : R) :

v.residueFieldEquivAdicCompletionIntegers ((Ideal.Quotient.mk v.asIdeal) a) = (IsLocalRing.residue ↥(adicCompletionIntegers K v)) ((algebraMap R ↥(adicCompletionIntegers K v)) a)

residueFieldEquivAdicCompletionIntegers sends the class of a : R to the residue of the image of a in 𝒪_v.

source

theorem IsDedekindDomain.HeightOneSpectrum.exists_unit_not_isSquare {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Finite (R ⧸ v.asIdeal)] (hv2 : 2 ∉ v.asIdeal) :

∃ (c : (↥(adicCompletionIntegers K v))ˣ), ¬IsSquare ((algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v)) ↑c)

At a place of odd residue characteristic, the ring of integers of the completion has a unit that is not a square in the completion: any lift of a non-square of the residue field.

source

theorem IsDedekindDomain.HeightOneSpectrum.mem_maximalIdeal_pow_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {x : ↥(adicCompletionIntegers K v)} {n : ℕ} :

x ∈ IsLocalRing.maximalIdeal ↥(adicCompletionIntegers K v) ^ n ↔ Valued.v ↑x ≤ WithZero.exp (-↑n)

An element of 𝒪_v lies in the n-th power of the maximal ideal exactly when its valuation is at most exp (-n).

source

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_mem_maximalIdeal_pow_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {r : R} {n : ℕ} :

(algebraMap R ↥(adicCompletionIntegers K v)) r ∈ IsLocalRing.maximalIdeal ↥(adicCompletionIntegers K v) ^ n ↔ r ∈ v.asIdeal ^ n

An element of R lies in v ^ n exactly when its image in 𝒪_v lies in 𝔪 ^ n: passing to the completion changes neither the valuation nor the v-adic filtration of R.

source