Ring topologised by a valuation

For a given valuation v : Valuation R Γ₀ on a ring R taking values in Γ₀, this file defines the type synonym WithVal v of R. By assigning a Valued (WithVal v) Γ₀ instance, WithVal v represents the ring R equipped with the topology coming from v. The type synonym WithVal v is in isomorphism to R as rings via WithVal.equiv v. This isomorphism should be used to explicitly map terms of WithVal v to terms of R.

The WithVal type synonym is used to define the completion of R with respect to v in Valuation.Completion. An example application of this is IsDedekindDomain.HeightOneSpectrum.adicCompletion, which is the completion of the field of fractions of a Dedekind domain with respect to a height-one prime ideal of the domain.

Main definitions

• WithVal : type synonym for a ring equipped with the topology coming from a valuation.
• WithVal.equiv : the canonical ring equivalence between WithValuation v and R.
• Valuation.Completion : the uniform space completion of a field K according to the uniform structure defined by the specified valuation.

def WithVal {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] : Valuation R Γ₀ → Type u_1

Type synonym for a ring equipped with the topology coming from a valuation.

instance WithVal.instRing {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) : Ring (WithVal v)

instance WithVal.instCommRing {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [CommRing R] (v : Valuation R Γ₀) : CommRing (WithVal v)

instance WithVal.instField {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Field R] (v : Valuation R Γ₀) : Field (WithVal v)

instance WithVal.instInhabited {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) : Inhabited (WithVal v)

instance WithVal.instPreorder {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) : Preorder (WithVal v)

instance WithVal.instAlgebra {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {S : Type u_4} [CommSemiring S] [CommRing R] [Algebra S R] (v : Valuation R Γ₀) : Algebra S (WithVal v)

instance WithVal.instIsFractionRing {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {S : Type u_4} [CommRing S] [CommRing R] [Algebra S R] [IsFractionRing S R] (v : Valuation R Γ₀) : IsFractionRing S (WithVal v)

instance WithVal.instSMul {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {S : Type u_4} [Ring R] [SMul S R] (v : Valuation R Γ₀) : SMul S (WithVal v)

instance WithVal.instIsScalarTower {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {P : Type u_3} {S : Type u_4} [Ring R] [SMul P S] [SMul S R] [SMul P R] [IsScalarTower P S R] (v : Valuation R Γ₀) : IsScalarTower P S (WithVal v)

instance WithVal.instAlgebra_1 {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [CommRing R] (v : Valuation R Γ₀) {S : Type u_5} [Ring S] [Algebra R S] : Algebra (WithVal v) S

instance WithVal.instAlgebra_2 {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [CommRing R] {S : Type u_5} [Ring S] [Algebra R S] (w : Valuation S Γ₀) : Algebra R (WithVal w)

instance WithVal.instIsScalarTower_1 {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [CommRing R] (v : Valuation R Γ₀) {P : Type u_5} {S : Type u_6} [Ring S] [Semiring P] [Module P R] [Module P S] [Algebra R S] [IsScalarTower P R S] : IsScalarTower P (WithVal v) S

def WithVal.equiv {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) : WithVal v ≃+* R

Canonical ring equivalence between WithVal v and R.

def WithVal.valuation {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) : Valuation (WithVal v) Γ₀

Canonical valuation on the WithVal v type synonym.

@[simp]

theorem WithVal.valuation_equiv_symm {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x : R) : (valuation v) ((equiv v).symm x) = v x

def WithVal.equivWithVal {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] {Γ'₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation R Γ₀) (w : Valuation R Γ'₀) : WithVal v ≃+* WithVal w

Canonical ring equivalence between WithVal v and WithVal w.

theorem WithVal.equivWithVal_symm {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] {Γ'₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation R Γ₀) (w : Valuation R Γ'₀) : (equivWithVal v w).symm = equivWithVal w v

@[simp]

theorem WithVal.equivWithVal_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] {Γ'₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation R Γ₀) (w : Valuation R Γ'₀) {x : WithVal v} : (equivWithVal v w) x = (equiv w).symm ((equiv v) x)

@[simp]

theorem WithVal.equivWithVal_symm_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] {Γ'₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation R Γ₀) (w : Valuation R Γ'₀) {x : WithVal w} : (equivWithVal v w).symm x = (equiv v).symm ((equiv w) x)

instance WithVal.instValued {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_4} [Ring R] (v : Valuation R Γ₀) : Valued (WithVal v) Γ₀

theorem WithVal.apply_equiv {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (r : WithVal v) : v ((equiv v) r) = Valued.v r

@[simp]

theorem WithVal.apply_symm_equiv {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (r : R) : Valued.v ((equiv v).symm r) = v r

theorem WithVal.le_def {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] {v : Valuation R Γ₀} {a b : WithVal v} : a ≤ b ↔ v ((equiv v) a) ≤ v ((equiv v) b)

theorem WithVal.lt_def {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] {v : Valuation R Γ₀} {a b : WithVal v} : a < b ↔ v ((equiv v) a) < v ((equiv v) b)

instance WithVal.instValuativeRel {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [CommRing R] (v : Valuation R Γ₀) : ValuativeRel (WithVal v)

instance WithVal.instCompatibleValuation {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [CommRing R] (v : Valuation R Γ₀) : (valuation v).Compatible

The completion of a field with respect to a valuation.

@[reducible, inline]

abbrev Valuation.Completion {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) : Type u_3

The completion of a field with respect to a valuation.

instance Valuation.instCoeCompletion {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) : Coe R v.Completion

The uniform isomorphism between WithVal v and WithVal w when v and w are equivalent.

def Valuation.IsEquiv.orderRingIso {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} (h : v.IsEquiv w) : WithVal v ≃+*o WithVal w

If two valuations v and w are equivalent then WithVal v is order-isomorphic to WithVal w.

@[simp]

theorem Valuation.IsEquiv.orderRingIso_apply {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} (h : v.IsEquiv w) (x : WithVal v) : h.orderRingIso x = (WithVal.equivWithVal v w) x

@[simp]

theorem Valuation.IsEquiv.orderRingIso_symm_apply {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} (h : v.IsEquiv w) (x : WithVal w) : h.orderRingIso.symm x = (WithVal.equivWithVal v w).symm x

theorem Valuation.IsEquiv.uniformContinuous_equivWithVal {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} (hw : ∀ (γ : Γ₀'ˣ), ∃ (r : R) (s : R), 0 < w r ∧ 0 < w s ∧ w r / w s = ↑γ) (h : v.IsEquiv w) : UniformContinuous ⇑(WithVal.equivWithVal v w)

def Valuation.IsEquiv.uniformEquiv {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} (hv : ∀ (γ : Γ₀ˣ), ∃ (r : R) (s : R), 0 < v r ∧ 0 < v s ∧ v r / v s = ↑γ) (hw : ∀ (γ : Γ₀'ˣ), ∃ (r : R) (s : R), 0 < w r ∧ 0 < w s ∧ w r / w s = ↑γ) (h : v.IsEquiv w) : WithVal v ≃ᵤ WithVal w

If two valuations v and w are equivalent then WithVal v and WithVal w are isomorphic as uniform spaces.

theorem Valuation.exists_div_eq_of_surjective {K : Type u_7} [Field K] {Γ₀ : Type u_8} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation K Γ₀} (hv : Function.Surjective ⇑v) (γ : Γ₀ˣ) : ∃ (r : K) (s : K), 0 < v r ∧ 0 < v s ∧ v r / v s = ↑γ

theorem Valuation.IsEquiv.valuedCompletion_le_one_iff {Γ₀ : Type u_5} {Γ₀' : Type u_6} [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀'] {K : Type u_7} [Field K] {v : Valuation K Γ₀} {w : Valuation K Γ₀'} (h : v.IsEquiv w) (hv : Function.Surjective ⇑v) (hw : Function.Surjective ⇑w) {x : v.Completion} : Valued.v x ≤ 1 ↔ Valued.v ((UniformSpace.Completion.mapEquiv (uniformEquiv ⋯ ⋯ h)) x) ≤ 1

instance NumberField.RingOfIntegers.instCoeHeadWithVal {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [Field K] (v : Valuation K Γ₀) : CoeHead (RingOfIntegers (WithVal v)) (WithVal v)

instance NumberField.RingOfIntegers.instIsDedekindDomainWithVal {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [Field K] [NumberField K] (v : Valuation K Γ₀) : IsDedekindDomain (RingOfIntegers (WithVal v))

instance NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [Field K] (v : Valuation K Γ₀) (R : Type u_4) [CommRing R] [Algebra R K] [IsIntegralClosure R ℤ K] : IsIntegralClosure R ℤ (WithVal v)

def NumberField.RingOfIntegers.withValEquiv {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [Field K] (v : Valuation K Γ₀) (R : Type u_4) [CommRing R] [Algebra R K] [IsIntegralClosure R ℤ K] : RingOfIntegers (WithVal v) ≃+* R

The ring equivalence between 𝓞 (WithVal v) and an integral closure of ℤ in K.

@[simp]

theorem NumberField.RingOfIntegers.withValEquiv_symm_apply {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [Field K] (v : Valuation K Γ₀) (R : Type u_4) [CommRing R] [Algebra R K] [IsIntegralClosure R ℤ K] (a✝ : R) : (withValEquiv v R).symm a✝ = (IsIntegralClosure.equiv ℤ R (WithVal v) (RingOfIntegers (WithVal v))) a✝

@[simp]

theorem NumberField.RingOfIntegers.withValEquiv_apply {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [Field K] (v : Valuation K Γ₀) (R : Type u_4) [CommRing R] [Algebra R K] [IsIntegralClosure R ℤ K] (a✝ : RingOfIntegers (WithVal v)) : (withValEquiv v R) a✝ = (↑↑(IsIntegralClosure.equiv ℤ R (WithVal v) (RingOfIntegers (WithVal v)))).symm a✝

def Rat.ringOfIntegersWithValEquiv {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℚ Γ₀) : NumberField.RingOfIntegers (WithVal v) ≃+* ℤ

The ring of integers of WithVal v, when v is a valuation on ℚ, is equivalent to ℤ.

@[simp]

theorem Rat.ringOfIntegersWithValEquiv_apply {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℚ Γ₀) (a✝ : NumberField.RingOfIntegers (WithVal v)) : (ringOfIntegersWithValEquiv v) a✝ = (↑↑(IsIntegralClosure.equiv ℤ ℤ (WithVal v) (NumberField.RingOfIntegers (WithVal v)))).symm a✝