Zulip Chat Archive

Stream: maths

Topic: additive discrete valuation


view this post on Zulip 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 Z\mathbb{Z} to 1nZ\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 R2R^2 associated to the valuation, defined as {(x,y):v(x)v(y)}\{(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?

view this post on Zulip Johan Commelin (Sep 10 2020 at 11:35):

/me :worried:

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 10 2020 at 13:48):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 10 2020 at 14:01):

But enats generally seem to be a pain to use.

view this post on Zulip Johan Commelin (Sep 10 2020 at 14:02):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 20:08):

docs#multiplicity

view this post on Zulip Aaron Anderson (Mar 02 2021 at 17:51):

I have a proposal for additive valuations: branch#add_valuation2

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 02 2021 at 18:01):

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

view this post on Zulip Aaron Anderson (Mar 02 2021 at 18:06):

Do I not?

view this post on Zulip 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.

view this post on Zulip Aaron Anderson (Mar 02 2021 at 18:10):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 18:10):

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

view this post on Zulip Eric Wieser (Mar 02 2021 at 18:10):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 18:13):

The valuation on a DVR goes to with_top nat

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Aaron Anderson (Mar 02 2021 at 18:40):

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

view this post on Zulip Aaron Anderson (Mar 02 2021 at 18:40):

  • define linear_ordered_add_comm_monoid_with_top

view this post on Zulip Aaron Anderson (Mar 02 2021 at 18:41):

  • refactor enat to be with_top nat

view this post on Zulip Aaron Anderson (Mar 02 2021 at 18:41):

I'm probably actually in favor of both

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 03 2021 at 23:07):

Oh that's a nice idea!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Aaron Anderson (Mar 06 2021 at 16:59):

#6559

view this post on Zulip Kevin Buzzard (Mar 06 2021 at 18:20):

Thanks so much for taking this on

view this post on Zulip 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)

view this post on Zulip Aaron Anderson (Mar 12 2021 at 19:51):

#6660 builds the DVR valuation

view this post on Zulip 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

view this post on Zulip Aaron Anderson (Mar 12 2021 at 21:07):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Aaron Anderson (Mar 13 2021 at 17:11):

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

view this post on Zulip Adam Topaz (Mar 13 2021 at 17:26):

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

view this post on Zulip Adam Topaz (Mar 13 2021 at 17:29):

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


Last updated: May 10 2021 at 07:15 UTC