# 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.

source
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.

Equations

- WithVal x✝ = R

Instances For

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

- WithVal.instRing v = inferInstanceAs (Ring R)

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

- WithVal.instCommRing v = inferInstanceAs (CommRing R)

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

- WithVal.instField v = inferInstanceAs (Field R)

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

- WithVal.instInhabited v = { default := 0 }

source
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)
Equations

- WithVal.instAlgebra v = inferInstanceAs (Algebra S R)

source
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)
source
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)
Equations

- WithVal.instSMul v = inferInstanceAs (SMul S R)

source
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)
source
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
Equations

- WithVal.instAlgebra_1 v = inferInstanceAs (Algebra R S)

source
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)
Equations

- WithVal.instAlgebra_2 w = inferInstanceAs (Algebra R S)

source
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
source
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`.

Equations

- WithVal.equiv v = RingEquiv.refl (WithVal v)

Instances For

source
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.

Equations

- WithVal.valuation v = Valuation.comap (↑(WithVal.equiv v)) v

Instances For

source
@[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
source
instance WithVal.instValued {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) :
Valued (WithVal v) Γ₀
Equations

- WithVal.instValued v = Valued.mk' (WithVal.valuation v)

source
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
source
@[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
source
instance WithVal.instValuativeRel {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [CommRing R] (v : Valuation R Γ₀) :
ValuativeRel (WithVal v)
Equations

- WithVal.instValuativeRel v = ValuativeRel.ofValuation (WithVal.valuation v)

source
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.

source
@[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.

Equations

- v.Completion = UniformSpace.Completion (WithVal v)

Instances For

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

- v.instCoeCompletion = inferInstanceAs (Coe (WithVal v) (UniformSpace.Completion (WithVal v)))

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

- NumberField.RingOfIntegers.instCoeHeadWithVal v = inferInstanceAs (CoeHead (NumberField.RingOfIntegers K) K)

source
instance NumberField.RingOfIntegers.instIsDedekindDomainWithVal {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [Field K] [NumberField K] (v : Valuation K Γ₀) :
IsDedekindDomain (RingOfIntegers (WithVal v))
source
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)
source
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`.

Equations

- NumberField.RingOfIntegers.withValEquiv v R = NumberField.RingOfIntegers.equiv R

Instances For

source
@[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✝
source
@[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✝
source
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 `ℤ`.

Equations

- Rat.ringOfIntegersWithValEquiv v = NumberField.RingOfIntegers.withValEquiv v ℤ

Instances For

source
@[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✝