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.instAlgebra {R : Type u_1} {Γ₀ : Type u_2} {S : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] [CommSemiring S] [CommRing R] [Algebra S R] (v : Valuation R Γ₀) : Algebra S (WithVal v)

instance WithVal.instIsFractionRing {R : Type u_1} {Γ₀ : Type u_2} {S : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] [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} {S : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] [SMul S R] (v : Valuation R Γ₀) : SMul S (WithVal v)

instance WithVal.instIsScalarTower {R : Type u_1} {Γ₀ : Type u_2} {P : Type u_3} {S : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] [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.

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

@[simp]

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

@[simp]

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

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

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✝