Adic Completions

If A is a valued ring with field of fractions K there are two different complete rings containing A one might define, the first is 𝒪_v = {x ∈ K_v | v x ≤ 1} (defined in Lean as adicCompletionIntegers K v) and the second is the v-adic completion of A. In the case when A is a Dedekind domain these definitions give isomorphic topological A-algebras. This file makes some progress towards this.

Main theorems/defs

• IsDedekindDomain.HeightOneSpectrum.closureAlgebraMapIntegers_eq_integers : The closure of A in K_v is 𝒪_v.
• IsDedekindDomain.HeightOneSpectrum.ResidueFieldEquivCompletionResidueField : The canonical isomorphism A ⧸ v ≅ 𝓞ᵥ / v.
• IsDedekindDomain.HeightOneSpectrum.closureAlgebraMapIntegers_eq_prodIntegers : If s is a set of primes of A, then the closure of A in ∏_{v ∈ s} K_v is ∏_{v ∈ s} 𝒪_v.
• IsDedekindDomain.HeightOneSpectrum.denseRange_of_prodAlgebraMap : If s is a finite set of primes of A, then K is dense in ∏_{v ∈ s} K_v.
• We show (as an unnamed instance) IsDiscreteValuationRing (𝒪[v.adicCompletion K])

theorem IsDedekindDomain.HeightOneSpectrum.exists_ofAdd_natCast_of_le_one {x : WithZero (Multiplicative ℤ)} (hx : x ≠ 0) (hx' : x ≤ 1) : ∃ (k : ℕ), ↑(Multiplicative.ofAdd (-↑k)) = x

theorem IsDedekindDomain.HeightOneSpectrum.exists_ofAdd_natCast_lt {x : WithZero (Multiplicative ℤ)} (hx : x ≠ 0) : ∃ (k : ℕ), ↑(Multiplicative.ofAdd (-↑k)) < x

theorem IsDedekindDomain.HeightOneSpectrum.ne_zero_of_some_le_intValuation {A : Type u_1} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {a : A} {m : Multiplicative ℤ} (h : ↑m ≤ v.intValuation a) : a ≠ 0

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_eq_coe_neg_multiplicity {A : Type u_1} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {a : A} (hnz : a ≠ 0) : v.intValuation a = ↑(Multiplicative.ofAdd (-↑(multiplicity v.asIdeal (Ideal.span {a}))))

theorem IsDedekindDomain.HeightOneSpectrum.emultiplicity_eq_of_valuation_eq_ofAdd {A : Type u_1} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {a : A} {k : ℕ} (hv : v.intValuation a = ↑(Multiplicative.ofAdd (-↑k))) : emultiplicity v.asIdeal (Ideal.span {a}) = ↑k

theorem IsDedekindDomain.HeightOneSpectrum.exists_adicValued_mul_sub_le {A : Type u_1} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {a b : A} {γ : WithZero (Multiplicative ℤ)} (hγ : γ ≠ 0) (hle : γ ≤ v.intValuation a) (hle' : v.intValuation b ≤ v.intValuation a) : ∃ (y : A), v.intValuation (y * a - b) ≤ γ

Given a, b ∈ A and v b ≤ v a we can find y in A such that y is close to a / b by the valuation v.

theorem IsDedekindDomain.HeightOneSpectrum.exists_adicValued_sub_lt_of_adicValued_le_one {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) {x : WithVal (valuation K v)} (γ : (WithZero (Multiplicative ℤ))ˣ) (hx : Valued.v x ≤ 1) : ∃ (a : A), Valued.v (↑((algebraMap A K) a) - ↑x) < ↑γ

theorem IsDedekindDomain.HeightOneSpectrum.closureAlgebraMapIntegers_eq_integers {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : closure ↑(algebraMap A (adicCompletion K v)).range = ↑(adicCompletionIntegers K v)

The closure of A in K_v is 𝒪_v.

theorem IsDedekindDomain.HeightOneSpectrum.denseRange_of_integerAlgebraMap {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : DenseRange ⇑(algebraMap A ↥(adicCompletionIntegers K v))

A is dense in 𝒪_v.

theorem IsDedekindDomain.HeightOneSpectrum.exists_adicValued_sub_lt_of_adicCompletionInteger {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) (x : ↥(adicCompletionIntegers K v)) (γ : (WithZero (Multiplicative ℤ))ˣ) : ∃ (a : A), Valued.v (↑((algebraMap A K) a) - ↑x) < ↑γ

An element of 𝒪_v can be approximated by an element of A.

@[reducible, inline]

noncomputable abbrev IsDedekindDomain.HeightOneSpectrum.completionIdeal {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : Ideal ↥(adicCompletionIntegers K v)

The maximal ideal of the integers of the completion of v.

Equations

• IsDedekindDomain.HeightOneSpectrum.completionIdeal K v = IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

theorem IsDedekindDomain.HeightOneSpectrum.mem_completionIdeal_iff {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) (x : ↥(adicCompletionIntegers K v)) : x ∈ completionIdeal K v ↔ Valued.v ↑x < 1

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_completionIntegers {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) (x : A) : ↑((algebraMap A ↥(adicCompletionIntegers K v)) x) = (algebraMap A (adicCompletion K v)) x

instance IsDedekindDomain.HeightOneSpectrum.instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : (completionIdeal K v).LiesOver v.asIdeal

noncomputable def IsDedekindDomain.HeightOneSpectrum.ResidueFieldToCompletionResidueField {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : A ⧸ v.asIdeal →+* IsLocalRing.ResidueField ↥(adicCompletionIntegers K v)

The canonical ring homomorphism from A / v to 𝓞ᵥ / v, where 𝓞ᵥ is the integers of the completion Kᵥ of the field of fractions of A.

Equations

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

noncomputable def IsDedekindDomain.HeightOneSpectrum.ResidueFieldEquivCompletionResidueField {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : A ⧸ v.asIdeal ≃+* IsLocalRing.ResidueField ↥(adicCompletionIntegers K v)

The canonical isomorphism from A / v to 𝓞ᵥ / v, where 𝓞ᵥ is the integers of the completion Kᵥ of the field of fractions K of A.

Equations

• IsDedekindDomain.HeightOneSpectrum.ResidueFieldEquivCompletionResidueField K v = RingEquiv.ofBijective (IsDedekindDomain.HeightOneSpectrum.ResidueFieldToCompletionResidueField K v) ⋯

theorem IsDedekindDomain.HeightOneSpectrum.inertiaDeg_asIdeal_completionIdeal {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : v.asIdeal.inertiaDeg (completionIdeal K v) = 1

theorem IsDedekindDomain.HeightOneSpectrum.exists_forall_adicValued_sub_lt {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {ι : Type u_3} (s : Finset ι) (e : ι → (WithZero (Multiplicative ℤ))ˣ) (valuation : ι → HeightOneSpectrum A) (injective : Function.Injective valuation) (x : (i : ι) → ↥(adicCompletionIntegers K (valuation i))) : ∃ (a : A), ∀ i ∈ s, Valued.v (↑((algebraMap A K) a) - ↑(x i)) < ↑(e i)

An element of ∏_{v ∈ s} 𝒪_v, with s finite, can be approximated by an element of A.

theorem IsDedekindDomain.HeightOneSpectrum.closureAlgebraMapIntegers_eq_prodIntegers {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {ι : Type u_3} (valuation : ι → HeightOneSpectrum A) (injective : Function.Injective valuation) : closure ↑(algebraMap A ((i : ι) → adicCompletion K (valuation i))).range = Set.univ.pi fun (i : ι) => (adicCompletionIntegers K (valuation i)).carrier

The closure of A in ∏_{v ∈ s} K_v is ∏_{v ∈ s} 𝒪_v. s may be infinite.

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.eq_mul_nonZeroDivisor_inv_adicCompletionIntegers {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) (x : adicCompletion K v) : ∃ a ∈ nonZeroDivisors A, ∃ b ∈ adicCompletionIntegers K v, x = ((algebraMap A K) a)⁻¹ • b

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.eq_mul_pi_adicCompletionIntegers {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {ι : Type u_3} [Fintype ι] (valuation : ι → HeightOneSpectrum A) (x : (i : ι) → adicCompletion K (valuation i)) : ∃ (k : K), ∃ y ∈ Set.univ.pi fun (i : ι) => (adicCompletionIntegers K (valuation i)).carrier, x = k • y

theorem IsDedekindDomain.HeightOneSpectrum.denseRange_of_prodAlgebraMap {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {ι : Type u_3} [Fintype ι] {valuation : ι → HeightOneSpectrum A} (injective : Function.Injective valuation) : DenseRange ⇑(algebraMap K ((i : ι) → adicCompletion K (valuation i)))

If s is finite then K in dense in ∏_{v ∈ s} K_v.

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.exists_uniformizer {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : ∃ (π : ↥(adicCompletionIntegers K v)), Valued.v ↑π = ↑(Multiplicative.ofAdd (-1))

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.uniformizer_ne_zero {A : Type u_1} {K : Type u_2} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {v : HeightOneSpectrum A} {π : ↥(adicCompletionIntegers K v)} (hπ : Valued.v ↑π = ↑(Multiplicative.ofAdd (-1))) : π ≠ 0

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.uniformizer_not_isUnit {A : Type u_1} {K : Type u_2} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) {π : ↥(adicCompletionIntegers K v)} (hπ : Valued.v ↑π = ↑(Multiplicative.ofAdd (-1))) : ¬IsUnit π

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.eq_pow_uniformizer_mul_unit {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) {x : ↥(adicCompletionIntegers K v)} (hx : x ≠ 0) {π : ↥(adicCompletionIntegers K v)} (hπ : Valued.v ↑π = ↑(Multiplicative.ofAdd (-1))) : ∃ (n : ℕ) (u : (↥(adicCompletionIntegers K v))ˣ), x = π ^ n * ↑u

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.maximalIdeal_eq_span_uniformizer {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) {π : ↥(adicCompletionIntegers K v)} (hπ : Valued.v ↑π = ↑(Multiplicative.ofAdd (-1))) : IsLocalRing.maximalIdeal ↥(adicCompletionIntegers K v) = Ideal.span {π}

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instDimensionLEOneSubtypeMemValuationSubringAdicCompletionIntegers_fLT {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : Ring.DimensionLEOne ↥(adicCompletionIntegers K v)

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsPrincipalIdealRingSubtypeMemValuationSubringAdicCompletionIntegers_fLT {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : IsPrincipalIdealRing ↥(adicCompletionIntegers K v)

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsDiscreteValuationRingSubtypeMemValuationSubringAdicCompletionIntegers_fLT {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : IsDiscreteValuationRing ↥(adicCompletionIntegers K v)

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeInt_fLT {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : IsDiscreteValuationRing ↥(Valued.integer (adicCompletion K v))

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.mem_completionIdeal_pow {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) {n : ℕ} (x : ↥(adicCompletionIntegers K v)) : x ∈ completionIdeal K v ^ n ↔ Valued.v ↑x ≤ ↑(Multiplicative.ofAdd (-↑n))

theorem IsDedekindDomain.HeightOneSpectrum.mem_completionIdeal_iff' {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) (x : ↥(adicCompletionIntegers K v)) : x ∈ completionIdeal K v ↔ Valued.v ↑x ≤ ↑(Multiplicative.ofAdd (-1))

theorem IsDedekindDomain.HeightOneSpectrum.completionIdeal_ne_bot {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : completionIdeal K v ≠ ⊥