Leading term of valuation

Stream: maths

[Violeta Hernández]

In #29687 I prove that if the real numbers embed into a ring K, then for any two elements x y : K with equal docs#ArchimedeanClass, there's a unique real number r such that ArchimedeanClass.mk y < ArchimedeanClass.mk (x - r * y).

@Weiyi Wang suggested that this result might generalize. Specifically, for any (additive) valuation v, and two elements x y : K with the same valuation, there should exist a unique r in the residue field (?) such that v y < v (x - r * y). My questions are:

• Is this result true?
• Does this value r have a name?
• Does this exist in Mathlib?

[Aaron Liu]

"remainder"?

[Weiyi Wang]

I guess it needs a condition "the residue field can be embedded back to K in a nice way "

[Violeta Hernández]

I think "nice way" here should mean v (f x) = 0 for x ≠ 0

[Aaron Liu]

sometimes it's an embedding but it doesn't respect the ring operations

[Violeta Hernández]

Well in the PR I made I specifically needed f : R ->+* K + strictly monotone

[Violeta Hernández]

Though it might be possible to relax strictly monotone to injective

[Aaron Liu]

so we also want it to be a RingHomClass?

[Aaron Liu]

the embedding, I mean

[Violeta Hernández]

I believe so

[Weiyi Wang]

actually, how about thinking "how do we calculate r". For now let's suppose K is a field, then x/y has multiplicative valuation 1 (or, x/y is in Valuation.valuationSubring if you relax the hypothesis like in your PR), and then IsLocalRing.residue outputs r

[Violeta Hernández]

docs#IsLocalRing.residue

[Violeta Hernández]

You're saying this is the value I want?

[Violeta Hernández]

in the surreal case, I think this gives the "omnific numbers mod w" map

[Weiyi Wang]

It is not exactly yet because it is not In \R. The next step would be: the residue field of ArchimedeanClass.addValuation is Archimedean, hence a subfield of \R

[Weiyi Wang]

(I have that "is a subfield of R" PR opened somewhere...)

[Weiyi Wang]

(deleted)

[Violeta Hernández]

Wait, but what's the local field in this context?

[Violeta Hernández]

Would it be the subfield of elements with nonnegative valuation?

[Aaron Liu]

Weiyi Wang said:

(I have that "is a subfield of R" PR opened somewhere...)

isn't that just docs#LinearOrderedField.inducedOrderRingHom

[Weiyi Wang]

Oh right, my PR was to show that the map for group and map for ring coincide :sweat_smile:but that's likely unnecessary.

[Violeta Hernández]

Or perhaps docs#Archimedean.embedReal ?

[Violeta Hernández]

oh that one's weaker

[Aaron Liu]

not a ring hom :(

[Weiyi Wang]

yeah that's the group hom. You can upgrade it to ring hom

[Violeta Hernández]

Feels weird that we have these two ways of embedding a field into the reals and that they read so differently

[Weiyi Wang]

That's probably my bad. I didn't find the existing one when writing Archimedean.embedReal

[Violeta Hernández]

Wait

[Violeta Hernández]

Isnt the property that I want to prove basically that valuations give an Euclidean domain structure?

[Weiyi Wang]

From https://en.wikipedia.org/wiki/Euclidean_domain
"Examples"

• Any discrete valuation ring....

[Violeta Hernández]

A valuation ring with a value group isomorphic to the integers? That doesn't seem right.

[Weiyi Wang]

This one translates to requiring discrete ArchimedeanClass, though. There is likely something junky when ArchimedeanClass is not discrete

[Weiyi Wang]

Yeah it only applies to discrete case

[Weiyi Wang]

(In mathlib it is Valuation.valuationSubring_isDiscreteValuationRing)

[Weiyi Wang]

This might be where ArchimedeanClass is special among arbitrary valuations. Its valuationSubring probably can be an Euclidean domain with weaker conditions

[Violeta Hernández]

Valuation.valuationSubring: the valuation subring associated to a valuation

wow thanks for nothing docstring

[Weiyi Wang]

Mathlib doesn't have IsDiscreteValuationRing -> EuclideanDomain.. is it missing or wrong?

[Violeta Hernández]

Weiyi Wang said:

This might be where ArchimedeanClass is special among arbitrary valuations. Its valuationSubring probably can be an Euclidean domain with weaker conditions

Wait, is this really the case? wouldn't it require ArchimedeanClass to be well-ordered?

[Weiyi Wang]

Does it? Could you elaborate?

[Violeta Hernández]

Well, the Euclidean function in an Euclidean domain needs a well-founded codomain

[Violeta Hernández]

I'm not sure if we necessarily have that

[Kenny Lau]

Weiyi Wang said:

Mathlib doesn't have IsDiscreteValuationRing -> EuclideanDomain.. is it missing or wrong?

well all the data involved there are highly noncanonical... maybe people just thought it wasn't a good idea

[Kenny Lau]

but I personally am not opposed to see a def (not instance)

[Weiyi Wang]

Violeta Hernández said:

Well, the Euclidean function in an Euclidean domain needs a well-founded codomain

Ah, I think you are right. I forgot the "A well-founded relation on R, satisfying r (a % b) b. This ensures that the GCD algorithm always terminates." part. So what we want is just a "possibly non-terminating Euclidean domain"

[Weiyi Wang]

Anyway, if we follow docs#EuclideanDomain, r would be quotient, and x - r * y would be remainder, and when FiniteArchimedeanClass is, say, isomorphic to integers, then these concepts coincide

[Kenny Lau]

import Mathlib

noncomputable section

namespace IsDiscreteValuationRing

variable {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]

def quotient (x y : R) : R :=
  open Classical in if y = 0 then 0 else if h : y ∣ x then h.choose else 0

def remainder (x y : R) : R :=
  x - y * quotient x y

def toWithBotNat (x : R) : WithBot ℕ :=
  addVal R x

@[simp] lemma toWithBotNat_zero : toWithBotNat (R := R) 0 = ⊥ :=
  addVal_zero

@[simp] lemma toWithBotNat_eq_bot_iff (x : R) : toWithBotNat x = ⊥ ↔ x = 0 :=
  addVal_eq_top_iff

@[simp] lemma bot_lt_toWithBotNat_iff (x : R) : ⊥ < toWithBotNat x ↔ x ≠ 0 := by
  rw [bot_lt_iff_ne_bot]; simp

lemma toWithBotNat_le_toWithBotNat_iff {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) :
    toWithBotNat x ≤ toWithBotNat y ↔ x ∣ y := by
  unfold toWithBotNat
  generalize hvx : addVal R x = vx
  generalize hvy : addVal R y = vy
  cases' vx with vx
  · rw [addVal_eq_top_iff] at hvx; tauto
  cases' vy with vy
  · rw [addVal_eq_top_iff] at hvy; tauto
  rw [← addVal_le_iff_dvd, hvx, hvy]
  exact WithBot.coe_le_coe.trans WithTop.coe_le_coe.symm

lemma dvd_of_toWithBotNat_le_toWithBotNat (x y : R) (hx : x ≠ 0)
    (hle : toWithBotNat x ≤ toWithBotNat y) : x ∣ y := by
  by_cases hy : y = 0
  · simp [hy, hx] at hle
  exact (toWithBotNat_le_toWithBotNat_iff hx hy).mp hle

variable (R) in
def toEuclideanDomain : EuclideanDomain R where
  quotient := quotient
  remainder := remainder
  r x y := toWithBotNat x < toWithBotNat y
  r_wellFounded := WellFounded.onFun wellFounded_lt
  quotient_zero x := by simp [quotient]
  remainder_lt x y hy := by
    rw [remainder, quotient, if_neg hy]
    split_ifs with hyx
    · rwa [← hyx.choose_spec, sub_self, toWithBotNat_zero, bot_lt_toWithBotNat_iff]
    · rw [mul_zero, sub_zero, lt_iff_not_ge]
      exact mt (dvd_of_toWithBotNat_le_toWithBotNat _ _ hy) hyx
  quotient_mul_add_remainder_eq x y := by
    rw [remainder, quotient]
    split_ifs with h₁ h₂
    · rw [h₁]; ring
    · rw [← h₂.choose_spec]; ring
    · ring
  mul_left_not_lt x y hy := by
    by_cases hx : x = 0
    · simp [hx]
    rw [not_lt, toWithBotNat_le_toWithBotNat_iff hx (mul_ne_zero hx hy)]
    exact dvd_mul_right _ _

end IsDiscreteValuationRing

[Kenny Lau]

#29693

[Scott Carnahan]

Regarding the original question, I would prefer a statement that there exists a unit r in the valuation ring (not the residue field) satisfying your condition. Then you could have a uniqueness statement asserting that any other such element is equivalent mod the maximal ideal.

[Scott Carnahan]

This avoids some of the messiness of lifting from the residue field.

[Weiyi Wang]

Wait... the EuclideanDomain stuff doesn't look right to me

[Weiyi Wang]

This code is basically saying the remainder is either x or 0???

[Aaron Liu]

that's probably not right

[Weiyi Wang]

I think you constructed... a EuclideanDomain, but not the EuclideanDomain I had in mind. Maybe this really just shows how non-canonical it is

[Weiyi Wang]

I'd like to define an EuclideanDomain on formal PowerSeries like example: 3 * x ^ 2 + 5 * x ^ 5 + 2 * x ^ 100 + ... divided by x^2 + x^5 should give quotient 3 and remainder 2 * x^5 + 2 * x ^ 100 + ...
Yours: gives quotient = 3 + 2 * x^3 - 2 * x^6 + 2 * x^9 + ... and remainder = 0

[Violeta Hernández]

I've got new doubts about my original statement. Consider the rationals with the 2-adic valuation. What would the statement even say? There isn't a ring homomorphism from 𝔽₂ → ℚ besides the trivial one.

[Aaron Liu]

Violeta Hernández said:

There isn't a ring homomorphism from 𝔽₂ → ℚ besides the trivial one.

There also isn't a trivial ring homomorphism

[Violeta Hernández]

isn't mapping everything to 0 always a ring homomorphism?

[Aaron Liu]

doesn't preserve 1

[Violeta Hernández]

ah

[Aaron Liu]

if there's a ring homomorphism then the characteristic of the codomain has to divide the characteristic of the domain

[Aaron Liu]

and 0 ∤ 2

[Aaron Liu]

why do we have ∉ but we don't have ∤

[Violeta Hernández]

in other words, I have no idea what the generalization of my standardPart construction even is anymore

[Kenny Lau]

Weiyi Wang said:

Maybe this really just shows how non-canonical it is

yeah...

[Kenny Lau]

Weiyi Wang said:

the remainder is either x or 0???

we're in a valuation ring, so either x|y or y|x, so the GCD can be computed in "1 step"

[Kenny Lau]

i just wrote the most efficient algorithm

[Violeta Hernández]

Question. Coming back to the original topic, do we have any other instances where the valuation theorem I mention is true?

[Violeta Hernández]

Not just that there's an Euclidean division, but that the quotient is given as an element of some ring homomorphism

[Weiyi Wang]

It should be true for PowerSeries / HahnSeries. Not sure if it is stated anywhere. (probably too trivial because it is just chopping off a term)
It is also "true" for p-adic numbers in some sense, but that's not a ring hom

[Yakov Pechersky]

docs#IsLocalRing.residue is a ring hom to a quotient, that I would call more of a "trailing" term rather than leading.

[Violeta Hernández]

Well, this standard part value in a sense is just encoding part of the Hahn embedding theorem

[Yakov Pechersky]

For p adics, embedding that back into the p adics is called docs#PadicInt.zmodRepr

[Yakov Pechersky]

That is the thing that avoids the nastiness of lifting from the residue field, that Scott mentioned.

[Violeta Hernández]

Is there any way to generalize both the standard part and the p-adic constructions, though?

[Violeta Hernández]

Like, from what I understand, my function ArchimedeanClass.standardPart is basically just a quotient, but there isn't really a single way to generalize this construction, and this construction doesn't even lead to something nice like an Euclidean domain in the general case.

[Weiyi Wang]

I think docs#IsLocalRing.residue is the generalization. It is unfortunately in the quotient space because not all valuation has a nicer construction

[Violeta Hernández]

Are the docs down? I can't open that page :frown:

[Weiyi Wang]

It opens for me

[Violeta Hernández]

Oh, it works if I open it on mobile

[Violeta Hernández]

Sorry, but I still don't get what R is in this case.

[Weiyi Wang]

R is docs#Valuation.valuationSubring, where x/y lives

[Violeta Hernández]

Ah!

[Violeta Hernández]

So that's what the v(y) ≤ v(x)condition translates to

[Weiyi Wang]

yep

[Violeta Hernández]

So you're right, what we want to do is show that the residue field is archimedean

[Violeta Hernández]

An archimedean field has a unique embedding into ℝ, right?

[Weiyi Wang]

Right. Pretty sure that uniqueness is stated in mathlib

[Weiyi Wang]

docs#LinearOrderedField.uniqueOrderRingHom

[Violeta Hernández]

I think I understand now

[Violeta Hernández]

I'll remake my standardPart PR using this

[Violeta Hernández]

I think the definition should look something like

def standardPart (x : K) : ℝ :=
  if 0 ≤ ArchimedeanClass.mk x then inducedMap (residue ⟨x, sorry⟩) else 0

[Violeta Hernández]

What's the Mathlib name for "the ring of elements of nonnegative valuation"?

[Violeta Hernández]

Is docs#Valuation.integer what I want? Do I need to turn my AddValuation into a Valuation first?

[Weiyi Wang]

I think so

[Violeta Hernández]

It's weird that we have docs#Valuation.integer and docs#Valuation.Integers

[Violeta Hernández]

Both feel like they go against the Mathlib naming convention

[Violeta Hernández]

At the very least the latter should be Valuation.IsInteger

[Violeta Hernández]

Oh nevermind, I want to use docs#Valuation.valuationSubring rather than docs#Valuation.integer

[Violeta Hernández]

I am also going to complain about these two definitions that are essentially the same having such different names and not linking to each other

[Violeta Hernández]

Wait a second

[Violeta Hernández]

How do we define the ordering on the residue field?

[Weiyi Wang]

:grimacing:by... showing the quotient operation respect the linear order on the original field?

[Violeta Hernández]

That seems untrue

[Violeta Hernández]

For instance, residue ω < residue 1

[Violeta Hernández]

I think what we need to show is that every nonzero element in the residue field has a unique representative with valuation zero

[Weiyi Wang]

I am assuming \omega here represents an infinitely large element, then residue omega isn't really defined? because residue can only be taken on all real elements or infinitesimal elements

[Violeta Hernández]

ah, dammit

[Violeta Hernández]

the inverse ordering on ArchimedeanClass strikes again

[Weiyi Wang]

so the linear order on residue is really saying "linear order is preserved if you quotient away infinitesimal elements"

[Violeta Hernández]

I guess you could define < on the residue field as x < y for all representatives x and y

[Violeta Hernández]

≤ is subtler, since you can have situations like 1 < 1 + ε but residue 1 = residue (1 + ε)

[Violeta Hernández]

I guess ¬ y < x would work to define x ≤ y, but this seems inelegant

[Weiyi Wang]

I went into something very similar when originally defining the linear order on ArchimedeanClass

[Weiyi Wang]

Basically we want to say express "a quotient collapse the linear order on the source type"

[Weiyi Wang]

One bad way to do that is LinearOrder.lift' with Quotient.out, but it's ugly

[Violeta Hernández]

That would work yeah

[Violeta Hernández]

I think the issue is that the order is preserved between different elements, but not within representatives for the same element

[Weiyi Wang]

Right. Perhaps mathlib has this but I don't know the magic spell

[Violeta Hernández]

Actually, what about this?

[Violeta Hernández]

• residue x ≤ residue y when either residue x = residue y or x ≤ y
• residue x < residue y when both residue x ≠ residue y and x < y

[Violeta Hernández]

I think both of these are independent of representative

[Weiyi Wang]

Yeah these can be defined as Quotient.lift₂ on Prop. It leaves you to justify it is a LinearOrder

[Violeta Hernández]

I think this is all related to the following fact: if you take a quotient of a linear order, where every equivalence class is convex, you get another linear order

[Weiyi Wang]

btw, this linear order can be generalized to quotient between any two ArchimedeanClass.addSubgroup, and you can also conclude the ArchimedeanClass on the quotient is isomorphic to the difference between the classes of the two subgroup (after properly dealing with 0). I had it in a very old branch (using the ugly LinearOrder.lift' way)

[Weiyi Wang]

Oh yeah I think what you said is even more general

[Aaron Liu]

Violeta Hernández said:

I think this is all related to the following fact: if you take a quotient of a linear order, where every equivalence class is convex, you get another linear order

convex as in docs#Set.OrdConnected

[Aaron Liu]

you wouldn't know from just the name

[Violeta Hernández]

@loogle LinearOrder, Quotient

[loogle]

:shrug: nothing found

[Violeta Hernández]

Just re-made my PR #29687 using the IsLocalRing.residue approach

[Violeta Hernández]

Still drafted, since it depends on three other PRs, one of which is still being actively discussed

[Violeta Hernández]

I'm still a bit surprised by the fact you can define a real-valued standard part from an arbitrary linearly ordered field without knowing anything about how the reals may or may not embed into it

[Violeta Hernández]

@Weiyi Wang doesn't docs#LinearOrderedField.uniqueOrderRingHom generalize where the domain is an Archimedean field, not necessarily conditionally complete? nevermind, I was thinking of docs#OrderRingHom.subsingleton

[Weiyi Wang]

I found something related to this

Screenshot from 2025-09-24 21-59-17.png

Irving Kaplansky, Maximal Fields with Valuations

(K is a field with valuation V. The fancy "R" is an arbitrary field, not necessarily real numbers)