additive discrete valuation

Stream: maths

[Kevin Buzzard]

@Ashvni Narayanan raised the topic of discrete valuation fields, and "the best way to do them". A discrete valuation field is a field equipped with a non-trivial discrete valuation which almost universally in the literature is an additive valuation to with_top int. This issue is also holding me up with valuations on DVRs because the valuation we already have (multiplicity on the semiring of ideals) is valued in enat and I need to get to multiplicative (with_top int) somehow.

I wonder whether a reasonable stopping point here is an API for additive discrete valuations, which can be defined to explicitly go from a ring R to with_top int, and follow the usual additive convention. There can be a coercion or function from additive discrete valuations to Lean's (hyper-general multiplicative) valuations, and conversely a predicate is_discrete on Lean's valuations, together with a proof that the two math-definitions ((1) : image discrete in non-zero part of tot ord gp with 0, (2) in the image of the additive discrete valuations) coincide.

Now I can hear Johan worrying that fixing int instead of using something with a universal property might be a disaster -- but I'm thinking that all the general manipulation of valuations can happen using the multiplicative language, and the additive language would nick some of the API and also of course add more coming from the API of int. For example when we start thinking about extensions of valuations we change from $\mathbb{Z}$ to $\frac{1}{n}\mathbb{Z}$ -- but this is the sort of calculation that should be going on using the multiplicative language perhaps.

If the idea of making a new additive_discrete_valuation class does not appeal, then I could make a new type alias for multiplicative (with_top int) (and would need advice on the name) and use this, or I could just get abstract and try proving things directly using an is_discrete predicate on valuations, although in practice I would imagine I would run into situations where I would far rather be in with_top int.

The structure which somehow doesn't care about whether the valuation is additive or multiplicative is the subset of $R^2$ associated to the valuation, defined as $\{(x,y):v(x)\leq v(y)\}$. Maybe one should pay more attention to this subset?

Will to_additive get us from with_top A to group_with_zero?

[Johan Commelin]

/me :worried:

[Adam Topaz]

The valuation ring itself is an mult/add independent way of speaking about the valuation :grinning_face_with_smiling_eyes:

[Adam Topaz]

There is one place where I would argue that one needs to fix the value group as something concrete like Z, and that's the product formula.

[Kevin Buzzard]

OK so Johan, what do you think about an API for discrete additive valuations taking values in with_top int?

[Kevin Buzzard]

This is all taking so long to get right. Another question is whether with_top X should be redefined as an inductive type, or perhaps made irreducible.

[Kevin Buzzard]

You have stuff like v(pi)=1, and 0<v(x) implies 1 <= v(x), so a little more API: DVRs is the story of with_top nat and DVFs the story of with_top int.

[Johan Commelin]

Kevin Buzzard said:

This is all taking so long to get right. Another question is whether with_top X should be redefined as an inductive type, or perhaps made irreducible.

It's a wrapper around an inductive type, right?

[Johan Commelin]

Kevin Buzzard said:

OK so Johan, what do you think about an API for discrete additive valuations taking values in with_top int?

I think we can't really get around it. So it will be important to have all the norm_cast lemmas that help when moving from enat to with_top int.

[Johan Commelin]

Also, before embarking on anything, I guess the api for enat / multiplicity should be fleshed out.

[Kevin Buzzard]

Are you imagining fleshing out this API for enat/multiplicity specifically within the context of DVRs or generally? For DVR's I was just going to make the API for the composition of multiplicity with the map to with_top int.

[Johan Commelin]

I would make a dedicated map enat -> with_top int and prove bunch of lemmas about it.

[Johan Commelin]

But enats generally seem to be a pain to use.

[Johan Commelin]

So I think the coe : nat -> enat is also missing some API

[Kevin Buzzard]

OK I can certainly start with this, I know what I'm doing here. What is the name of the map enat -> with_top int?

[Johan Commelin]

Also, the API seems to be that you write k \in n for k : nat and n : enat. I'm sure that computers like this. But for humans it is a very weird notation.

[Johan Commelin]

Kevin Buzzard said:

OK I can certainly start with this, I know what I'm doing here. What is the name of the map enat -> with_top int?

Maybe coe?

[Kevin Buzzard]

docs#multiplicity

[Aaron Anderson]

I have a proposal for additive valuations: branch#add_valuation2

[Aaron Anderson]

Basically, I think (but am not completely committed to the idea) that we should have an add_valuation be a separate structure, satisfying the axioms as you might find them in the literature, but then we can have an add_valuation.to_valuation function that turns it into a default multiplicative valuation on a value group made with type tags.

[Aaron Anderson]

We'd still need to duplicate the API, but hopefully the proofs would all just reference the existing lemmas for v.to_valuation, and perhaps we could teach to_additive or a similar tactic to generate the statements too.

[Adam Topaz]

Hmmm.... shouldn't you use linear_ordered_add_comm_group?

[Aaron Anderson]

Do I not?

[Adam Topaz]

Oh, never mind... I was looking at the top of the file where you have linear_ordered_comm_group, but I missed the fact that you have a separate section later on with linear_ordered_add_comm_group.

[Aaron Anderson]

Yes, all the new stuff is at the bottom of the file.

[Kevin Buzzard]

Johan tried this for valuations but eventually decided that it was better to make group_with_zero

[Kevin Buzzard]

You won't be able to do valuations to enat this way

[Eric Wieser]

with_zero (multiplicative (order_dual Γ)) sounds like a pleasure to work with. /s

[Aaron Anderson]

Eric Wieser said:

with_zero (multiplicative (order_dual Γ)) sounds like a pleasure to work with. /s

This is why I don't want to define an add_valuation as literally a valuation to that group...

[Kevin Buzzard]

For two reasons -- it's not with_top of anything and it's a monoid not a group

[Kevin Buzzard]

Valuations need refactoring so they go to monoids with 0. I set everything up but then teaching hit and I never finished the job

[Kevin Buzzard]

The valuation on a DVR goes to with_top nat

[Kevin Buzzard]

Valuations need refactoring so they go to monoids with 0. I set everything up but then teaching hit and I never finished the job

[Aaron Anderson]

Kevin Buzzard said:

Valuations need refactoring so they go to monoids with 0. I set everything up but then teaching hit and I never finished the job

#6500

[Aaron Anderson]

As far as the additive case for monoids, my current formulation has a problem that we don't even have linear_ordered_add_comm_monoid, but we do have linear_ordered_cancel_add_comm_monoid. Other than that, #6500 should be enough to switch to monoids.

[Aaron Anderson]

As far as enat not being with_top of anything, I see two options:

[Aaron Anderson]

• define linear_ordered_add_comm_monoid_with_top

[Aaron Anderson]

• refactor enat to be with_top nat

[Aaron Anderson]

I'm probably actually in favor of both

[Kevin Buzzard]

In my use case for valuations we really want non-cancellative ones by the way. I want to have a valuation on Z/p^nZ whose target is a eg quotient of [0,1] where you collapse [0,e) to zero for some appropriate e

[Aaron Anderson]

Ok, I defer to the mystery of option vs. roption, I've defined linear_ordered_add_comm_monoid_with_top at branch#linear_ordered_comm_monoid

[Aaron Anderson]

And I've placed an instance on multiplicative (order_dual a) which should allow us to get definitional equality when translating between multiplicative and additive valuations.

[Eric Wieser]

Two quick comments about that branch: it's likely to conflict with #6489; attr#ancestor should match the order in the extends clause

[Kevin Buzzard]

I do think this is the right way of doing it. Thanks for putting in this effort!

[Eric Wieser]

I assume you can put an instance in the reverse direction on additive (order_dual a) too?

[Damiano Testa]

In case this is of help to someone else, Mario explained to me the difference between option and roption here (and around the conversation in the following link):

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/discrete_topology/near/218941558

[Aaron Anderson]

Eric Wieser said:

I assume you can put an instance in the reverse direction on additive (order_dual a) too?

I just checked - yes.

[Aaron Anderson]

#6520 has the required changes to the ordered algebra hierarchy, and branch#add_valuation3 implements additive valuations using it.

[Aaron Anderson]

I'm thinking currently the best strategy is to define add_valuation R G to be valuation R (multiplicative (order_dual G)), copy the API (largely done), and then probably also create a new constructor add_valuation.of that will take more reasonably stated (but definitionally equivalent) proofs as input.

[Kevin Buzzard]

Oh that's a nice idea!

[Aaron Anderson]

Actual proof of concept at branch#add_valuation3: multiplicity of a prime in an integral domain as an add_valuation

[Aaron Anderson]

That should subsume the DVR case at least, and may be useful somewhere in the p-adic library

[Aaron Anderson]

#6559

[Kevin Buzzard]

Thanks so much for taking this on

[Kevin Buzzard]

A related question I always had was whether there should be special notation or a definition for multiplicative int (the infinite cyclic group) and with_zero (multiplicative int) (the target of a discrete valuation)

[Aaron Anderson]

#6660 builds the DVR valuation

[Aaron Anderson]

I'd like to move on directly to the p-adics, but there are a lot of choices to be made there

[Aaron Anderson]

@Kevin Buzzard , what other API/examples do you want for valuations now?

[Kevin Buzzard]

If we have a mono morphism of ordered monoids with 0 then this induces a map from the valuations taking values in the first monoid to valuations taking values in the second monoid

[Kevin Buzzard]

I want that if R is a comm ring with a valuation and p is in R then R/pR gets a valuation to some kind of quotient monoid. This was precisely what couldn't be done with ordered groups with 0

[Kevin Buzzard]

I want to collapse 0<=x<=v(p) to zero. I think you can do that with totally ordered monoids

[Aaron Anderson]

Do you have a source I can read about this kind of quotient?

[Adam Topaz]

Deligne's paper on truncated DVRs is the only one I know of

[Adam Topaz]

But Deligne's notion of a truncated DVR involves more data