discrete valuation

Stream: Is there code for X?

[François Sunatori]

Hi, is discrete valuation on a field defined in Mathlib?

[Johan Commelin]

@François Sunatori mathlib has valuations in pretty great generality. There are arbitrary valuations on rings, and also the special case of discrete valuation rings.

[Johan Commelin]

The exact thing that your are looking for might not be there, but there should be sufficient API to quickly get what you want.

[Johan Commelin]

docs#discrete_valuation_ring

[Kevin Buzzard]

The ridiculous hold-up for me when I was thinking about defining these explicitly last summer was that I didn't know whether the value group should be a multiplicative version of the integers or whether it should be a more general thing just isomorphic to this. We have discrete valuation rings IIRC

[François Sunatori]

I did see discrete valuation rings, but I'm wondering if there's explicitly this definition:

A discrete valuation on a field K is a function ν : K× −→ Z that
satisfies the following properties.
(i) ν is surjective.
(ii) ν(xy) = ν(x) + ν(y).
(iii) ν(x + y) ≥ min{ν(x), ν(y)}

or can it be derived from what is already there?

[François Sunatori]

I would like to show that

Let R be a DVR. Then a non-zero element u ∈ R is a unit if and
only if ν(u) = 0

[Johan Commelin]

@François Sunatori nope, I don't think we have exactly that. Specifically, what is missing is (i) v is surjective. I think that your question about DVRs might already be there. You don't need fields to answer that question; you can stay inside R.

[Kevin Buzzard]

With the valuations we have this would be a map from all of $K$ to with_zero (multiplicative ℤ)

[Adam Topaz]

What sort of things would you like to prove for discrete valuations that are not true for general valuations (on a field, say)?

[Kevin Buzzard]

Stuff like ramification index can only be defined for discrete valuations maybe?

[Adam Topaz]

The ramification degree in general is the index of the inclusion of the value groups.

[Adam Topaz]

Although things like the fundamental equality do require some additional assumptions

[Kevin Buzzard]

There is an entire theory of discrete valuation rings and fields, with theorems such as $ef=n$ for an extension (ramification index times degree of residue field extension equals degree of field extension) which I have no reason to believe will be true for general valuation rings (in the sense that I have no idea whether it's true). Things like the definition of a uniformiser only make sense for discrete valuations.

[Adam Topaz]

https://www.ams.org/journals/tran/1958-088-01/S0002-9947-1958-0100589-6/S0002-9947-1958-0100589-6.pdf

[Kevin Buzzard]

The criteria for equality both mention discreteness of the valuation though ;-)

[Adam Topaz]

Yes, but not of rank 1

[Kevin Buzzard]

right

[Kevin Buzzard]

so equality is the sort of thing I'd like to prove for discrete valuations which are not true for general valuations (on a field).

[Adam Topaz]

Fair enough. I would say the first inequality is worth proving as well.

[Kevin Buzzard]

There is a general theory of valuations on fields, but important special cases are rank 1 valuations (where you can build the theory of rigid analytic geometry) and rank 1 discrete valuations (where you can build things like local class field theory). I think we will have to have these special cases at some point, and I do not know how best to formalise them in Lean

[Adam Topaz]

For rank 1, we can use the characterization saying that the value group has an order embedding in the reals.

[Kevin Buzzard]

and for rank 1 discrete we can say that the value group is not 0 but has an order embedding into the integers (or more precisely multiplicative int). The question I'm not sure about is: is that really what we want to say?

[François Sunatori]

ok I see.. I was trying to see if there were some statements missing about discrete valuation rings or Dedekind domains. I guess many statements about discrete valuations are done at the valuation level.

[François Sunatori]

Is there anything (definitions or lemmas) missing to show in dedekind_domain.lean the equivalence between is_dedekind_domain and is_dedekind_domain_dvr?

I saw TODO: Prove that these are actually equivalent definitions.

[Kevin Buzzard]

If you're interested in proving this then give it a try! Cassels Froehlich is a reference I believe

[Anne Baanen]

François Sunatori said:

Is there anything (definitions or lemmas) missing to show in dedekind_domain.lean the equivalence between is_dedekind_domain and is_dedekind_domain_dvr?

I saw TODO: Prove that these are actually equivalent definitions.

There's a branch we're slowly working on getting merged, that proves docs#is_dedekind_domain and docs#is_dedekind_domain_inv are equivalent. I don't think anyone is working on the _dvr equivalence.

[François Sunatori]

thanks @Anne Baanen , I am thinking of working on

lemma is_dedekind_domain_dvr_equiv_is_dedekind_domain_inv :
  is_dedekind_domain_dvr_iff A ↔ is_dedekind_domain_inv_iff A :=
begin
  sorry
end

[François Sunatori]

On which branch is the work on proving docs#is_dedekind_domain and docs#is_dedekind_domain_inv are equivalent being done?

[Anne Baanen]

There is a proof on branch#dedekind-domain-dev

[Anne Baanen]

(That branch is gruesomely, namely 2 months, out-of-date!)

[François Sunatori]

ok thanks! I'll take a look

[François Sunatori]

by the way, I was looking at branches that may have work related to DVRs or Dedekind domains and found this branch https://github.com/leanprover-community/mathlib/compare/dvr-valuation with the statement

noncomputable def valuation (R : Type u) [integral_domain R] [discrete_valuation_ring R] :
  valuation R (with_zero (multiplicative ℤ))

is this definition no longer necessary because it lives in a more general form in mathlib? or is it still missing?

[Kevin Buzzard]

It's probably still missing because I didn't know whether this was the right definition and then got sidetracked into the question of whether there should be notation for multiplicative int, and then I just forgot about it.