## Stream: maths

### Topic: additive discrete valuation

#### Kevin Buzzard (Sep 10 2020 at 11:30):

@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?

/me :worried:

#### Adam Topaz (Sep 10 2020 at 12:52):

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

#### Adam Topaz (Sep 10 2020 at 12:56):

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 (Sep 10 2020 at 13:36):

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

#### Kevin Buzzard (Sep 10 2020 at 13:37):

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 (Sep 10 2020 at 13:40):

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 (Sep 10 2020 at 13:47):

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 (Sep 10 2020 at 13:48):

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 (Sep 10 2020 at 13:48):

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

#### Kevin Buzzard (Sep 10 2020 at 13:57):

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 (Sep 10 2020 at 14:01):

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

#### Johan Commelin (Sep 10 2020 at 14:01):

But enats generally seem to be a pain to use.

#### Johan Commelin (Sep 10 2020 at 14:02):

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

#### Kevin Buzzard (Sep 10 2020 at 14:02):

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 (Sep 10 2020 at 14:02):

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 (Sep 10 2020 at 14:03):

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 (Sep 10 2020 at 20:08):

docs#multiplicity

#### Aaron Anderson (Mar 02 2021 at 17:51):

I have a proposal for additive valuations: branch#add_valuation2

#### Aaron Anderson (Mar 02 2021 at 17:55):

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 (Mar 02 2021 at 17:57):

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 (Mar 02 2021 at 18:01):

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

Do I not?

#### Adam Topaz (Mar 02 2021 at 18:09):

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 (Mar 02 2021 at 18:10):

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

#### Kevin Buzzard (Mar 02 2021 at 18:10):

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

#### Kevin Buzzard (Mar 02 2021 at 18:10):

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

#### Eric Wieser (Mar 02 2021 at 18:10):

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

#### Aaron Anderson (Mar 02 2021 at 18:11):

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 (Mar 02 2021 at 18:12):

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

#### Kevin Buzzard (Mar 02 2021 at 18:13):

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 (Mar 02 2021 at 18:13):

The valuation on a DVR goes to with_top nat

#### Kevin Buzzard (Mar 02 2021 at 18:13):

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 (Mar 02 2021 at 18:15):

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 (Mar 02 2021 at 18:40):

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 (Mar 02 2021 at 18:40):

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

#### Aaron Anderson (Mar 02 2021 at 18:40):

• define linear_ordered_add_comm_monoid_with_top

#### Aaron Anderson (Mar 02 2021 at 18:41):

• refactor enat to be with_top nat

#### Aaron Anderson (Mar 02 2021 at 18:41):

I'm probably actually in favor of both

#### Kevin Buzzard (Mar 02 2021 at 18:49):

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 (Mar 03 2021 at 17:32):

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 (Mar 03 2021 at 17:33):

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 (Mar 03 2021 at 17:45):

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 (Mar 03 2021 at 17:50):

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

#### Eric Wieser (Mar 03 2021 at 17:51):

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

#### Damiano Testa (Mar 03 2021 at 18:09):

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 (Mar 03 2021 at 21:11):

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 (Mar 03 2021 at 22:58):

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

#### Aaron Anderson (Mar 03 2021 at 23:01):

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 (Mar 03 2021 at 23:07):

Oh that's a nice idea!

#### Aaron Anderson (Mar 04 2021 at 04:51):

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

#### Aaron Anderson (Mar 04 2021 at 04:54):

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

#6559

#### Kevin Buzzard (Mar 06 2021 at 18:20):

Thanks so much for taking this on

#### Kevin Buzzard (Mar 06 2021 at 18:22):

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 (Mar 12 2021 at 19:51):

#6660 builds the DVR valuation

#### Aaron Anderson (Mar 12 2021 at 19:52):

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

#### Aaron Anderson (Mar 12 2021 at 21:07):

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

#### Kevin Buzzard (Mar 13 2021 at 00:20):

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 (Mar 13 2021 at 00:21):

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 (Mar 13 2021 at 00:22):

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