Completions of Dedekind domains with respect to adic valuations

Given a Dedekind domain R with field of fractions K and a maximal ideal v of R, we define the completion of K with respect to its v-adic valuation, denoted v.adicCompletion, and its ring of integers, denoted v.adicCompletionIntegers.

Main definitions

• IsDedekindDomain.HeightOneSpectrum.adicCompletion v is the completion of K with respect to its v-adic valuation.
• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers v is the ring of integers of v.adicCompletion.

Tags

dedekind domain, dedekind ring, adic valuation, completion

@[instance_reducible]

noncomputable def IsDedekindDomain.HeightOneSpectrum.adicValued {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Valued K (WithZero (Multiplicative ℤ))

K as a valued field with the v-adic valuation.

Equations

• v.adicValued = Valued.mk' (IsDedekindDomain.HeightOneSpectrum.valuation K v)

theorem IsDedekindDomain.HeightOneSpectrum.adicValued_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {x : K} : Valued.v x = (valuation K v) x

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

The completion of K with respect to its v-adic valuation, defined as a one-field structure wrapping the uniform-space completion (v.valuation K).Completion.

• ofCompletion :: (
• toCompletion : (HeightOneSpectrum.valuation K v).Completion

  The underlying element of the completion (v.valuation K).Completion.

• )

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.delabOfCompletion : Lean.PrettyPrinter.Delaborator.Delab

Prevents ofCompletion v x being printed as { toCompletion := x } by delabStructureInstance.

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.delabOfCompletion = Lean.PrettyPrinter.Delaborator.delabApp

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : adicCompletion K v ≃ (HeightOneSpectrum.valuation K v).Completion

adicCompletion.toCompletion and adicCompletion.ofCompletion as an equivalence.

Equations

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion_symm_apply_toCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (toCompletion : (HeightOneSpectrum.valuation K v).Completion) : ((equivCompletion K v).symm toCompletion).toCompletion = toCompletion

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (self : adicCompletion K v) : (equivCompletion K v) self = self.toCompletion

@[instance_reducible]

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

Equations

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

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : adicCompletion K v ≃+* (HeightOneSpectrum.valuation K v).Completion

adicCompletion.toCompletion as a ring isomorphism onto the underlying completion.

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv K v = { toEquiv := IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion K v, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (self : adicCompletion K v) : (equiv K v) self = self.toCompletion

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_ofCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : (HeightOneSpectrum.valuation K v).Completion) : (ofCompletion x).toCompletion = x

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_toCompletion {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) : ofCompletion x.toCompletion = x

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : toCompletion 0 = 0

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : toCompletion 1 = 1

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_add {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x y : adicCompletion K v) : (x + y).toCompletion = x.toCompletion + y.toCompletion

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_mul {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x y : adicCompletion K v) : (x * y).toCompletion = x.toCompletion * y.toCompletion

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Function.Surjective toCompletion

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Function.Surjective ofCompletion

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instUniformSpace {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : UniformSpace (adicCompletion K v)

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.instUniformSpace K v = UniformSpace.comap IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion inferInstance

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

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsUniformAddGroup {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : IsUniformAddGroup (adicCompletion K v)

noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))

The v-adic valuation on adicCompletion K v, transported from the completion along equiv.

Equations

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuationExtension_toCompletion {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) : (WithVal.valuation (HeightOneSpectrum.valuation K v)).extension x.toCompletion = (valuation K v) x

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation_ofCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (y : (HeightOneSpectrum.valuation K v).Completion) : (valuation K v) (ofCompletion y) = (WithVal.valuation (HeightOneSpectrum.valuation K v)).extension y

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroup_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : (↑(valuation K v)).valueGroup = (↑(WithVal.valuation (HeightOneSpectrum.valuation K v)).extension).valueGroup

noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupMulEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : ↥(↑(valuation K v)).valueGroup ≃* ↥(↑(WithVal.valuation (HeightOneSpectrum.valuation K v)).extension).valueGroup

The value group (valuation K v).valueGroup of the canonical valuation on v.adicCompletion K is equivalent multiplicatively to the value group of the valuation of K extended to v.adicCompletion K.

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupMulEquiv K v = { toEquiv := Set.equivOfEq ⋯, map_mul' := ⋯ }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupMulEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : ↥(↑(valuation K v)).valueGroup) : ↑((valueGroupMulEquiv K v) a) = ↑a

noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : (↑(valuation K v)).ValueGroup₀ ≃*o (↑(WithVal.valuation (HeightOneSpectrum.valuation K v)).extension).ValueGroup₀

The value group with zero (valuation K v).ValueGrou₀ of the canonical valuation on v.adicCompletion K is multiplicatively order isomorphic to the value group with zero of the valuation of K extended to v.adicCompletion K.

Equations

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_coe {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : ↥(↑(valuation K v)).valueGroup) : (valueGroupOrderMonoidIso K v) ↑a = ↑((valueGroupMulEquiv K v) a)

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderMonoidIso {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (g : (↑(valuation K v)).ValueGroup₀) : MonoidWithZeroHom.ValueGroup₀.embedding ((valueGroupOrderMonoidIso K v) g) = MonoidWithZeroHom.ValueGroup₀.embedding g

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_restrict {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) : (valueGroupOrderMonoidIso K v) ((valuation K v).restrict x) = (WithVal.valuation (HeightOneSpectrum.valuation K v)).extension.restrict x.toCompletion

@[deprecated IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupMulEquiv (since := "2026-09-28")]

noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : ↥(↑(valuation K v)).valueGroup ≃* ↥(↑(WithVal.valuation (HeightOneSpectrum.valuation K v)).extension).valueGroup

Alias of IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupMulEquiv.

---

The value group (valuation K v).valueGroup of the canonical valuation on v.adicCompletion K is equivalent multiplicatively to the value group of the valuation of K extended to v.adicCompletion K.

Equations

• @IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv = @IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupMulEquiv

@[deprecated IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupMulEquiv (since := "2026-09-28")]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : ↥(↑(valuation K v)).valueGroup) : ↑((valueGroupMulEquiv K v) a) = ↑a

Alias of IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupMulEquiv.

@[deprecated IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso (since := "2026-09-28")]

noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : (↑(valuation K v)).ValueGroup₀ ≃*o (↑(WithVal.valuation (HeightOneSpectrum.valuation K v)).extension).ValueGroup₀

Alias of IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso.

---

The value group with zero (valuation K v).ValueGrou₀ of the canonical valuation on v.adicCompletion K is multiplicatively order isomorphic to the value group with zero of the valuation of K extended to v.adicCompletion K.

Equations

• @IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso = @IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso

@[deprecated IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_coe (since := "2026-09-28")]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupOrderIso_coe {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : ↥(↑(valuation K v)).valueGroup) : (valueGroupOrderMonoidIso K v) ↑a = ↑((valueGroupMulEquiv K v) a)

Alias of IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_coe.

@[deprecated IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderMonoidIso (since := "2026-09-28")]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderIso {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (g : (↑(valuation K v)).ValueGroup₀) : MonoidWithZeroHom.ValueGroup₀.embedding ((valueGroupOrderMonoidIso K v) g) = MonoidWithZeroHom.ValueGroup₀.embedding g

Alias of IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderMonoidIso.

@[deprecated IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_restrict (since := "2026-09-28")]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso_restrict {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) : (valueGroupOrderMonoidIso K v) ((valuation K v).restrict x) = (WithVal.valuation (HeightOneSpectrum.valuation K v)).extension.restrict x.toCompletion

Alias of IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_restrict.

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instValuativeRel {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : ValuativeRel (adicCompletion K v)

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.instValuativeRel K v = ValuativeRel.ofValuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation K v)

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCompatibleWithZeroMultiplicativeIntValuation {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : (valuation K v).Compatible

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsValuativeTopology {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : IsValuativeTopology (adicCompletion K v)

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instValuedWithZeroMultiplicativeInt {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Valued (adicCompletion K v) (WithZero (Multiplicative ℤ))

Equations

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

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCompleteSpace {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : CompleteSpace (adicCompletion K v)

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCoeWithValWithZeroMultiplicativeIntValuation {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Coe (WithVal (HeightOneSpectrum.valuation K v)) (adicCompletion K v)

Coercion of an element of WithVal (v.valuation K) into the adic completion.

Equations

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

@[instance_reducible, instance 99]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCoe {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Coe K (adicCompletion K v)

Coercion of an element of K into the adic completion.

Equations

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_toCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (k : K) : (ofCompletion ↑(WithVal.toVal (HeightOneSpectrum.valuation K v) k)).toCompletion = ↑(WithVal.toVal (HeightOneSpectrum.valuation K v) k)

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.extension_apply_eq_valued {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (y : (HeightOneSpectrum.valuation K v).Completion) : (WithVal.valuation (HeightOneSpectrum.valuation K v)).extension y = Valued.v y

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_apply {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} : Valued.v x = Valued.extensionValuation x.toCompletion

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion_apply {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) : Valued.v x.toCompletion = Valued.v x

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (y : (HeightOneSpectrum.valuation K v).Completion) : Valued.v (ofCompletion y) = Valued.v y

@[deprecated IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_apply (since := "2026-09-28")]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_def {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} : Valued.v x = Valued.extensionValuation x.toCompletion

Alias of IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_apply.

@[deprecated IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion_apply (since := "2026-09-28")]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion {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) : Valued.v x.toCompletion = Valued.v x

Alias of IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion_apply.

@[deprecated IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion_apply (since := "2026-09-28")]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (y : (HeightOneSpectrum.valuation K v).Completion) : Valued.v (ofCompletion y) = Valued.v y

Alias of IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion_apply.

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_coe {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (k : K) : Valued.v (ofCompletion ↑(WithVal.toVal (HeightOneSpectrum.valuation K v) k)) = (HeightOneSpectrum.valuation K v) k

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {x y : adicCompletion K v} (h : x.toCompletion = y.toCompletion) : x = y

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext_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 y : adicCompletion K v} : x = y ↔ x.toCompletion = y.toCompletion

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : ofCompletion ↑(WithVal.toVal (HeightOneSpectrum.valuation K v) 0) = 0

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : ofCompletion ↑(WithVal.toVal (HeightOneSpectrum.valuation K v) 1) = 1

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_add {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x y : K) : ofCompletion ↑(WithVal.toVal (HeightOneSpectrum.valuation K v) (x + y)) = ofCompletion ↑(WithVal.toVal (HeightOneSpectrum.valuation K v) x) + ofCompletion ↑(WithVal.toVal (HeightOneSpectrum.valuation K v) y)

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_mul {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x y : K) : ofCompletion ↑(WithVal.toVal (HeightOneSpectrum.valuation K v) (x * y)) = ofCompletion ↑(WithVal.toVal (HeightOneSpectrum.valuation K v) x) * ofCompletion ↑(WithVal.toVal (HeightOneSpectrum.valuation K v) y)

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.uniformEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : adicCompletion K v ≃ᵤ (HeightOneSpectrum.valuation K v).Completion

toCompletion as a uniform-space isomorphism onto the underlying completion.

Equations

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

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

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

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instT0Space {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : T0Space (adicCompletion K v)

theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Function.Surjective ⇑Valued.v

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : (↑Valued.v).valueGroup = (↑(valuation K v)).valueGroup

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

The ring of integers of adicCompletion.

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v = Valued.v.valuationSubring

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.instInhabitedSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Inhabited ↥(adicCompletionIntegers K v)

Equations

• IsDedekindDomain.HeightOneSpectrum.instInhabitedSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers K v = { default := 0 }

theorem IsDedekindDomain.HeightOneSpectrum.mem_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} : x ∈ adicCompletionIntegers K v ↔ Valued.v x ≤ 1

theorem IsDedekindDomain.HeightOneSpectrum.notMem_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} : x ∉ adicCompletionIntegers K v ↔ 1 < Valued.v x

@[instance 100]

instance IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul' (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : UniformContinuousConstSMul R (WithVal (valuation K v))

instance IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] : UniformContinuousConstSMul S (WithVal (valuation K v))

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.instAlgebraCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] : Algebra S (valuation K v).Completion

The S-algebra structure on the underlying completion.

Equations

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

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] : Algebra S (adicCompletion K v)

Equations

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

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion_toCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] (r : S) : ((algebraMap S (adicCompletion K v)) r).toCompletion = (algebraMap S (valuation K v).Completion) r

instance IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerCompletionWithZeroMultiplicativeIntValuation (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] {S₀ : Type u_4} [CommSemiring S₀] [Algebra S₀ S] [Algebra S₀ K] [IsScalarTower S₀ S K] : IsScalarTower S₀ S (valuation K v).Completion

instance IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerAdicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] {S₀ : Type u_4} [CommSemiring S₀] [Algebra S₀ S] [Algebra S₀ K] [IsScalarTower S₀ S K] : IsScalarTower S₀ S (adicCompletion K v)

theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] (r : S) (x : WithVal (valuation K v)) : adicCompletion.ofCompletion ↑(r • x) = r • adicCompletion.ofCompletion ↑x

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] : ⇑(algebraMap S (adicCompletion K v)) = (fun (x : K) => adicCompletion.ofCompletion ↑(WithVal.toVal (valuation K v) x)) ∘ ⇑(algebraMap S K)

theorem IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : DenseRange ⇑(algebraMap K (adicCompletion K v))

theorem IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem (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) : adicCompletion.ofCompletion ↑(WithVal.toVal (valuation K v) ((algebraMap R K) r)) ∈ adicCompletionIntegers K v

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.instAlgebraSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Algebra R ↥(adicCompletionIntegers K v)

Equations

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply (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) : ↑((algebraMap R ↥(adicCompletionIntegers K v)) r) = adicCompletion.ofCompletion ↑(WithVal.toVal (valuation K v) ((algebraMap R K) r))

instance IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [FaithfulSMul R K] : FaithfulSMul R ↥(adicCompletionIntegers K v)

theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation {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) : Valued.v ↑r = (valuation K v) ↑r

The valuation on the completion agrees with the global valuation on elements of the integer ring.

theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation' {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (k : K) : Valued.v (adicCompletion.ofCompletion ↑(WithVal.toVal (valuation K v) k)) = (valuation K v) k

The valuation on the completion agrees with the global valuation on elements of the field.

theorem IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers {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) : ↑r ∈ adicCompletionIntegers K v

A global integer is in the local integers.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers (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) (x : ↥(adicCompletionIntegers K v)) : ↑(r • x) = r • ↑x

instance IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Module.IsTorsionFree R ↥(adicCompletionIntegers K v)

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower' (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : IsScalarTower R (↥(adicCompletionIntegers K v)) (adicCompletion K v)

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : adicCompletion K v) : ∃ b ∈ nonZeroDivisors R, a * ↑b ∈ adicCompletionIntegers K v

instance IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_1 {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : FaithfulSMul (↥(adicCompletionIntegers K v)) (adicCompletion K v)

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

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : HeightOneSpectrum R} {a : ↥(adicCompletionIntegers K v)} : IsUnit a ↔ Valued.v ↑a = 1

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : HeightOneSpectrum R} {a : (adicCompletion K v)ˣ} : a ∈ (adicCompletionIntegers K v).units ↔ Valued.v ↑a = 1