Documentation

Mathlib.Topology.Algebra.Valued.WithVal

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.

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

Type u_1

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

toVal :: (

ofVal : R
Converts an element of WithVal v to an element of R.

)

Instances For

def WithVal.delabToVal :

Lean.PrettyPrinter.Delaborator.Delab

This prevents toVal v x being printed as { ofAbs := x } by delabStructureInstance.

Instances For

@[implicit_reducible]

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

Ring (WithVal v)

@[implicit_reducible]

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

Inhabited (WithVal v)

@[implicit_reducible]

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

Preorder (WithVal v)

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

a ≤ b ↔ v a.ofVal ≤ v b.ofVal

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

a < b ↔ v a.ofVal < v b.ofVal

theorem WithVal.ofVal_toVal {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x : R) :

(toVal v x).ofVal = x

@[simp]

theorem WithVal.toVal_ofVal {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x : WithVal v) :

toVal v x.ofVal = x

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

Function.Surjective ofVal

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

Function.Surjective (toVal v)

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

Function.Injective ofVal

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

Function.Injective (toVal v)

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

Function.Bijective ofVal

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

Function.Bijective (toVal v)

@[simp]

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

toVal v 0 = 0

@[simp]

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

ofVal 0 = 0

@[simp]

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

toVal v 1 = 1

@[simp]

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

ofVal 1 = 1

@[simp]

theorem WithVal.toVal_add {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x y : R) :

toVal v (x + y) = toVal v x + toVal v y

@[simp]

theorem WithVal.ofVal_add {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x y : WithVal v) :

(x + y).ofVal = x.ofVal + y.ofVal

@[simp]

theorem WithVal.toVal_sub {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x y : R) :

toVal v (x - y) = toVal v x - toVal v y

@[simp]

theorem WithVal.ofVal_sub {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x y : WithVal v) :

(x - y).ofVal = x.ofVal - y.ofVal

@[simp]

theorem WithVal.toVal_mul {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x y : R) :

toVal v (x * y) = toVal v x * toVal v y

@[simp]

theorem WithVal.ofVal_mul {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x y : WithVal v) :

(x * y).ofVal = x.ofVal * y.ofVal

@[simp]

theorem WithVal.toVal_neg {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x : R) :

toVal v (-x) = -toVal v x

@[simp]

theorem WithVal.ofVal_neg {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x : WithVal v) :

(-x).ofVal = -x.ofVal

@[simp]

theorem WithVal.toVal_pow {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x : R) (n : ℕ) :

toVal v (x ^ n) = toVal v x ^ n

@[simp]

theorem WithVal.ofVal_pow {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x : WithVal v) (n : ℕ) :

(x ^ n).ofVal = x.ofVal ^ n

@[simp]

theorem WithVal.toVal_eq_zero {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x : R) :

toVal v x = 0 ↔ x = 0

@[simp]

theorem WithVal.ofVal_eq_zero {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (x : WithVal v) :

x.ofVal = 0 ↔ x = 0

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

WithVal v ≃+* R

The canonical ring equivalence between WithVal v and R.

Instances For

@[simp]

theorem WithVal.equiv_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (self : WithVal v) :

(equiv v) self = self.ofVal

@[simp]

theorem WithVal.equiv_symm_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (ofVal : R) :

(equiv v).symm ofVal = toVal v ofVal

def WithVal.map {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [Ring S] {Λ₀ : Type u_4} [LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀) (f : R →+* S) :

WithVal v →+* WithVal w

Lift a ring hom to WithVal.

Instances For

@[simp]

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

map v v (RingHom.id R) = RingHom.id (WithVal v)

@[simp]

theorem WithVal.map_comp {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [Ring S] {Λ₀ : Type u_4} [LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀) {T : Type u_5} [Ring T] (u : Valuation T Γ₀) (f : S →+* T) (g : R →+* S) :

map v u (f.comp g) = (map w u f).comp (map v w g)

@[simp]

theorem WithVal.map_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [Ring S] {Λ₀ : Type u_4} [LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀) (f : R →+* S) (x : WithVal v) :

(map v w f) x = toVal w (f x.ofVal)

def WithVal.congr {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [Ring S] {Λ₀ : Type u_4} [LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀) (f : R ≃+* S) :

WithVal v ≃+* WithVal w

Lift a RingEquiv to WithVal.

Instances For

@[simp]

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

congr v v (RingEquiv.refl R) = RingEquiv.refl (WithVal v)

theorem WithVal.congr_symm {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [Ring S] {Λ₀ : Type u_4} [LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀) (f : R ≃+* S) :

(congr v w f).symm = congr w v f.symm

theorem WithVal.congr_trans {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [Ring S] {Λ₀ : Type u_4} [LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀) {T : Type u_5} [Ring T] (u : Valuation T Γ₀) (f : R ≃+* S) (g : S ≃+* T) :

congr v u (f.trans g) = (congr v w f).trans (congr w u g)

@[simp]

theorem WithVal.congr_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [Ring S] {Λ₀ : Type u_4} [LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀) (f : R ≃+* S) (x : WithVal v) :

(congr v w f) x = toVal w (f x.ofVal)

@[simp]

theorem WithVal.congr_symm_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [Ring S] {Λ₀ : Type u_4} [LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀) (f : R ≃+* S) (x : WithVal w) :

(congr v w f).symm x = toVal v (f.symm x.ofVal)

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.

Instances For

@[simp]

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

(valuation v) (toVal v x) = v x

@[implicit_reducible]

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

Valued (WithVal v) Γ₀

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

v r.ofVal = Valued.v r

theorem WithVal.val_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.valued_toVal {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) (r : R) :

Valued.v (toVal v r) = v r

@[deprecated WithVal.apply_ofVal (since := "2026-03-02")]

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

v r.ofVal = Valued.v r

Alias of WithVal.apply_ofVal.

@[deprecated WithVal.valued_toVal (since := "2026-03-02")]

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

Valued.v (toVal v r) = v r

Alias of WithVal.valued_toVal.

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

CharZero (WithVal v)

@[implicit_reducible]

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

CommRing (WithVal v)

@[implicit_reducible]

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

@[implicit_reducible]

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

SMul (WithVal v) S

theorem WithVal.smul_left_def {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [SMul R S] (x : WithVal v) (s : S) :

x • s = x.ofVal • s

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

FaithfulSMul (WithVal v) S

@[implicit_reducible]

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

SMul S (WithVal v)

theorem WithVal.smul_right_def {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [SMul S R] (s : S) (x : WithVal v) :

s • x = toVal v (s • x.ofVal)

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

FaithfulSMul S (WithVal v)

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

IsScalarTower (WithVal v) S P

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

IsScalarTower P R (WithVal v)

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

IsScalarTower P (WithVal v) R

@[implicit_reducible]

instance WithVal.instModule {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [AddCommMonoid S] [Module R S] :

Module (WithVal v) S

instance WithVal.instFinite {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [AddCommMonoid S] [Module R S] [Module.Finite R S] :

Module.Finite (WithVal v) S

@[implicit_reducible]

instance WithVal.instModule_1 {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [Semiring S] [Module S R] :

Module S (WithVal v)

@[simp]

theorem WithVal.toVal_smul {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [SMul S R] (s : S) (r : R) :

toVal v (s • r) = s • toVal v r

@[simp]

theorem WithVal.ofVal_smul {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] (v : Valuation R Γ₀) {S : Type u_3} [SMul S R] (s : S) (x : WithVal v) :

(s • x).ofVal = s • x.ofVal

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

WithVal v ≃ₗ[R] S

The canonical R-linear isomorphism between WithVal v and S, when v : Valuation S Γ₀.

Instances For

@[simp]

theorem WithVal.linearEquiv_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] {S : Type u_3} [Ring S] [Module R S] (v : Valuation S Γ₀) (x : WithVal v) :

(linearEquiv R v) x = x.ofVal

@[simp]

theorem WithVal.linearEquiv_symm_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] {S : Type u_3} [Ring S] [Module R S] (v : Valuation S Γ₀) (x : S) :

(linearEquiv R v).symm x = toVal v x

instance WithVal.instFinite_1 {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Ring R] {S : Type u_3} [Ring S] (v : Valuation S Γ₀) [Module R S] [Module.Finite R S] :

Module.Finite R (WithVal v)

@[implicit_reducible]

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

Algebra (WithVal v) S

theorem WithVal.algebraMap_left_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [CommRing R] (v : Valuation R Γ₀) [Semiring S] [Algebra R S] (s : WithVal v) :

(algebraMap (WithVal v) S) s = (algebraMap R S) s.ofVal

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

IsFractionRing (WithVal v) S

theorem WithVal.algebraMap_left_injective {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [CommRing R] (v : Valuation R Γ₀) [Semiring S] [Algebra R S] (h : Function.Injective ⇑(algebraMap R S)) :

Function.Injective ⇑(algebraMap (WithVal v) S)

@[implicit_reducible]

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

Algebra R (WithVal v)

theorem WithVal.algebraMap_right_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [CommSemiring R] [Ring S] [Algebra R S] (v : Valuation S Γ₀) (r : R) :

(algebraMap R (WithVal v)) r = toVal v ((algebraMap R S) r)

theorem WithVal.algebraMap_right_injective {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [CommSemiring R] [Ring S] [Algebra R S] (v : Valuation S Γ₀) (h : Function.Injective ⇑(algebraMap R S)) :

Function.Injective ⇑(algebraMap R (WithVal v))

def WithVal.algEquiv (R : Type u_1) {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [CommSemiring R] [Ring S] [Algebra R S] (v : Valuation S Γ₀) :

WithVal v ≃ₐ[R] S

The canonical R-algebra isomorphism between WithVal v and S, when v : Valuation S Γ₀.

Instances For

@[simp]

theorem WithVal.algEquiv_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [CommSemiring R] [Ring S] [Algebra R S] (v : Valuation S Γ₀) (x : WithVal v) :

(algEquiv R v) x = x.ofVal

@[simp]

theorem WithVal.algEquiv_symm_apply {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [CommSemiring R] [Ring S] [Algebra R S] (v : Valuation S Γ₀) (x : S) :

(algEquiv R v).symm x = toVal v x

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

IsLocalization M (WithVal v)

@[implicit_reducible]

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

Field (WithVal v)

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

NumberField (WithVal v)

@[simp]

theorem WithVal.toVal_div {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Field R] (v : Valuation R Γ₀) (x y : R) :

toVal v (x / y) = toVal v x / toVal v y

@[simp]

theorem WithVal.ofVal_div {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Field R] (v : Valuation R Γ₀) (x y : WithVal v) :

(x / y).ofVal = x.ofVal / y.ofVal

@[simp]

theorem WithVal.toVal_inv {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Field R] (v : Valuation R Γ₀) (x : R) :

toVal v x⁻¹ = (toVal v x)⁻¹

@[simp]

theorem WithVal.ofVal_inv {R : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Field R] (v : Valuation R Γ₀) (x : WithVal v) :

x⁻¹.ofVal = x.ofVal⁻¹

@[deprecated "Use `WithVal.congr v w (.refl R)` instead" (since := "2026-01-27")]

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.

Instances For

@[deprecated WithVal.congr_symm (since := "2026-01-27")]

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

(congr v w (RingEquiv.refl R)).symm = congr w v (RingEquiv.refl R)

@[deprecated "Use `WithVal.congr_apply` instead" (since := "2026-01-27")]

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} :

(congr v w (RingEquiv.refl R)) x = (equiv w).symm ((equiv v) x)

@[deprecated "Use `WithVal.congr_symm_apply` instead" (since := "2026-01-27")]

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} :

(congr v w (RingEquiv.refl R)).symm x = (equiv v).symm ((equiv w) x)

theorem WithVal.valueGroup_eq {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) :

MonoidWithZeroHom.valueGroup Valued.v = MonoidWithZeroHom.valueGroup v

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

↥(MonoidWithZeroHom.valueGroup Valued.v) ≃* ↥(MonoidWithZeroHom.valueGroup v)

The multiplicative equivalence between the valueGroup of the valuation on WithVal v and the valuation v.

Instances For

@[simp]

theorem WithVal.valueGroupEquiv_symm_apply {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) (b : { b : Γ₀ˣ // (fun (x : Γ₀ˣ) => x ∈ ↑(MonoidWithZeroHom.valueGroup v)) b }) :

(valueGroupEquiv v).symm b = ⟨↑b, ⋯⟩

@[simp]

theorem WithVal.valueGroupEquiv_apply {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) (a : { a : Γ₀ˣ // (fun (x : Γ₀ˣ) => x ∈ ↑(MonoidWithZeroHom.valueGroup Valued.v)) a }) :

(valueGroupEquiv v) a = ⟨↑a, ⋯⟩

theorem WithVal.strictMono_valueGroupEquiv {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) :

StrictMono ⇑(valueGroupEquiv v)

theorem WithVal.strictMono_valueGroupEquiv_symm {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) :

StrictMono ⇑(valueGroupEquiv v).symm

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

MonoidWithZeroHom.ValueGroup₀ Valued.v ≃*o MonoidWithZeroHom.ValueGroup₀ v

The order-preserving, multiplicative equivalence between the ValueGroup₀ of the valuation on WithVal v and the valuation v.

Instances For

@[simp]

theorem WithVal.valueGroupOrderIso₀_apply {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) (a : WithZero ↥(MonoidWithZeroHom.valueGroup Valued.v)) :

(valueGroupOrderIso₀ v) a = (WithZero.map' ↑(valueGroupEquiv v)) a

@[simp]

theorem WithVal.valueGroupOrderIso₀_symm_apply {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) (a : WithZero ↥(MonoidWithZeroHom.valueGroup v)) :

(valueGroupOrderIso₀ v).symm a = (WithZero.map' ↑(valueGroupEquiv v).symm) a

theorem WithVal.valueGroupOrderIso₀_restrict {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) (b : WithVal v) :

(valueGroupOrderIso₀ v) (Valued.v.restrict b) = v.restrict b.ofVal

theorem WithVal.valueGroupOrderIso₀_symm_restrict {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) (b : R) :

(valueGroupOrderIso₀ v).symm (v.restrict b) = Valued.v.restrict (toVal v b)

theorem WithVal.strictMono_valueGroupOrderIso₀ {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) :

StrictMono ⇑(valueGroupOrderIso₀ v)

theorem WithVal.strictMono_valueGroupOrderIso₀_symm {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) :

StrictMono ⇑(valueGroupOrderIso₀ v).symm

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.

Instances For

@[implicit_reducible, instance 99]

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

Instances For

@[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.toVal w x.ofVal

@[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.toVal v x.ofVal

theorem Valuation.IsEquiv.uniformContinuous_equiv {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} [hval : Valued R Γ₀'] (hv : Valued.v = w) (h : v.IsEquiv w) :

UniformContinuous ⇑(WithVal.equiv v)

theorem Valuation.IsEquiv.uniformContinuous_equiv_symm {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} [hval : Valued R Γ₀'] (hv : Valued.v = w) (h : w.IsEquiv v) :

UniformContinuous ⇑(WithVal.equiv v).symm

theorem Valuation.IsEquiv.uniformContinuous {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} (h : v.IsEquiv w) :

UniformContinuous ⇑(RingHom.id R)

theorem Valuation.IsEquiv.uniformContinuous_congr {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} (h : v.IsEquiv w) :

UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))

@[deprecated Valuation.IsEquiv.uniformContinuous_congr (since := "2026-01-27")]

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 Γ₀'} (h : v.IsEquiv w) :

UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))

Alias of Valuation.IsEquiv.uniformContinuous_congr.

def Valuation.IsEquiv.uniformEquiv {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 ≃ᵤ WithVal w

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

Instances For

def WithVal.uniformEquiv {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} [Valued R Γ₀'] (hV : Valued.v = w) (h : v.IsEquiv w) :

WithVal v ≃ᵤ R

Let v : Valuation R Γ₀. If R has Valued R Γ₀' defined via construction through w : Valuation R Γ₀', with v equivalent to w, then WithVal.equiv defines a uniform space isomorphism WithVal v ≃ᵤ R.

Instances For

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.restrict_exists_div_eq {K : Type u_7} [Field K] {Γ₀ : Type u_8} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) (γ : (MonoidWithZeroHom.ValueGroup₀ v)ˣ) :

∃ (r : K) (s : K), 0 < v r ∧ 0 < v s ∧ v.restrict r / v.restrict 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) {x : v.Completion} :

Valued.v x ≤ 1 ↔ Valued.v ((UniformSpace.Completion.mapEquiv h.uniformEquiv) x) ≤ 1

@[implicit_reducible]

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

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

Instances For

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

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

noncomputable 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 ℤ.

Instances For

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