General p-adic valuation

Stream: mathlib4

[Daniel Weber]

For any UFD F and a field K such that IsFractionRing F K, for any prime p in F the p-adic valuation is a (noncomputable) AddValuation K (WithTop ℤ). I want to contribute this to Mathlib, but I'm not sure where to place this and how to name it. Any suggestions?

[Johan Commelin]

I guess it could be called adicValuation? Maybe put it in a file Mathlib/RingTheory/Valuation/AdicValuation.lean?

[Kevin Buzzard]

Valuation in lean usually refers to multiplicative valuations though.

[Filippo A. E. Nuccio]

We have docs#IsDedekindDomain.HeightOneSpectrum.valuation for the Adic Valuation attached to every prime in a Dedekind domain. This, as Kevin says, is a multiplicative valuation, and I think it is important that we keep things aligned, somewhat avoiding additive ones altogether. I understand it takes a little bit to switch language, but having two versions of valuations everywhere would lead to either a bunch of useless code or an immense duplication, and without a true mathematical benefit.

[Filippo A. E. Nuccio]

Its definition relies upon docs#IsDedekindDomain.HeightOneSpectrum.intValuationDef and probably the best way to go is to strengthen this definition by removing unnecessary assumptions on the ring.

[Filippo A. E. Nuccio]

On the other hand, UFD and Dedekind domains are not one more/less general than the other one, so we should probably come up with the right assumptions on the ring to allow a nice unified definition and then specialize to the UFD or DD case for specific results.

[Daniel Weber]

My definition actually works with WfDvdMonoid, which is more general than Dedekind domain, but it's stated directly in terms of (p : R) [Fact (Prime p)]

[Filippo A. E. Nuccio]

Can't you make it work using an ideal rather than an element?

[Daniel Weber]

It's using docs#multiplicity.addValuation, so I'm not exactly sure how

[Filippo A. E. Nuccio]

Perhaps playing with docs#count_span_normalizedFactors_eq and its friends?

[Filippo A. E. Nuccio]

I would advocate for avoiding this docs#multiplicity.addValuation altogether. It is additive and moreover takes values in the horrible PartENat.

[Filippo A. E. Nuccio]

It is an old file that somewhat got lost, I believe.

[Filippo A. E. Nuccio]

Working around what we have for the (multiplicative) AdicValuation for DD is more suitable, generalizing it if possible.

[Filippo A. E. Nuccio]

If you have this on a github repo, I'd be happy to have a look.

[Daniel Weber]

What I wanted to add is https://github.com/leanprover-community/mathlib4/blob/83ae564e733541ba769472141d046aa2f75d0669/Mathlib/RingTheory/Valuation/AdicValuation.lean although I now agree that generalizing the multiplicative version would be better

[Adam Topaz]

Filippo A. E. Nuccio said:

On the other hand, UFD and Dedekind domains are not one more/less general than the other one, so we should probably come up with the right assumptions on the ring to allow a nice unified definition and then specialize to the UFD or DD case for specific results.

The general construction would be to associate the discrete valuation to a height one prime in any normal Noetherian ring. (The localization at the prime would be a DVR.)

[Adam Topaz]

Or better, you just need to assume that the localization at the prime is normal.

[Adam Topaz]

cf. DiscreteValuationRing.TFAE

[Filippo A. E. Nuccio]

Actually the localization at this hgt 1 prime would be a local dedekind domain, hence a dvr, no?

[Adam Topaz]

Yup!

[Adam Topaz]

But I assume mathlib doesn't know this yet (except for the TFAE statement above)

[Filippo A. E. Nuccio]

Yes, probably.

[Filippo A. E. Nuccio]

At any rate since there is a lot of API for the AdicValuation in a (local or not) Dedekind domain, I would argue that using this is probably easier than using the valuation attached to it as a DVR. We prove they are equivalent in our project on local fields so it makes little difference. The advantage of using the DedekindDomain.AdicValuation is that all things related to "valuation is positive iff a uniformizer divides" and friends are already in mathlib.

[Johan Commelin]

Yeah it would certainly be good to capitalize on that (-;

[Filippo A. E. Nuccio]

To sum up for @Daniel Weber , I agree with Adam that if you start with any Normal Noetherian domain R and any prime ideal P of hgt 1, then you can define the (multiplicative) valuation as the DedekindDomain.AdicValuation attached to the maximal ideal of the local field obtained localizing R at P. The case of a UFD and an element p follows since UFD's are Noetherian Normal and the ideal generated by p would have hgt 1.

[Filippo A. E. Nuccio]

It would also be very nice to develop more about Krull rings building upon what we currently have for Dedekind D.

[Adam Topaz]

Is the adic valuation for a prime in a Dedekind domain not defined by localizing and looking at the associated DVR?

[Filippo A. E. Nuccio]

Not "defined" by proven equivalent (in mathlib I mean(

[Adam Topaz]

Or is it defined in terms of factorization of principal fractional ideals?

[Filippo A. E. Nuccio]

docs#IsDedekindDomain.HeightOneSpectrum.valuation

[Filippo A. E. Nuccio]

Probably what really matters is docs#IsDedekindDomain.HeightOneSpectrum.intValuationDef

[Adam Topaz]

Oh I see… that seems like the least efficient definition to me! :rofl:

[Adam Topaz]

But that doesn’t matter as long as it works!

[Filippo A. E. Nuccio]

Once we're done with porting our project, you're welcome to refactor it entirely :grinning_face_with_smiling_eyes:

[Filippo A. E. Nuccio]

Jokes aside, I think that since the API built around it is quite well done, the def is no longer very important. And working with this valuation is pretty easy.

[Daniel Weber]

Filippo A. E. Nuccio said:

To sum up for Daniel Weber , I agree with Adam that if you start with any Normal Noetherian domain R and any prime ideal P of hgt 1, then you can define the (multiplicative) valuation as the DedekindDomain.AdicValuation attached to the maximal ideal of the local field obtained localizing R at P. The case of a UFD and an element p follows since UFD's are Noetherian Normal and the ideal generated by p would have hgt 1.

My use case has R as the ring of polynomials over a field, so I think I should be able to just use the existing version for a Dedekind domain. However, I'm not sure how to construct a docs#IsDedekindDomain.HeightOneSpectrum from the span of a prime element. What's the API for that?

[Filippo A. E. Nuccio]

This docs#Polynomial.idealX is the ideal spanned by X and this, for instance, docs#RatFunc.instValuedWithZeroMultiplicativeInt is the associated valuation.

[Filippo A. E. Nuccio]

Which prime polynomial are you considering?

[Daniel Weber]

My argument is that for any prime polynomial the valuation of some value is nonnegative (that's additive, multiplicatively it'd be ≤ 1, right?), so that value must actually be a polynomial, so it has to be general

[Filippo A. E. Nuccio]

Then you can first prove that your polynomial is prime and deduce (say, in lemma1) that the ideal spanned by it is a prime ideal. Then you prove in lemma2 that this is non-zero, and finally you can define

def Danielideal : IsDedekindDomain.HeightOneSpectrum K[X] where
  asIdeal := Ideal.span {p}
  isPrime := by lemma1
  ne_bot  := by lemma2

[Filippo A. E. Nuccio]

Then you can access the valuation attached to it as DanielIdeal.valuation.

[Daniel Weber]

I think you misunderstood, the result I'm using is something along the lines of

example (x : K) (h : ∀ p : F[X], Prime p → p.Monic → 0 ≤ vp p x) :
   IsLocalization.IsInteger F[X] x := sorry

and I'm not sure what to write in place of vp p in h.

[Filippo A. E. Nuccio]

You should take my explanation and let it depend on p. So

def Danielideal (p : F[X]) (hp: Prime p): IsDedekindDomain.HeightOneSpectrum K[X] where
  asIdeal := Ideal.span {p}
  isPrime := lemma1
  ne_bot  := lemma2

[Daniel Weber]

I see, so that's not defined already. Alright, I'll define it. BTW hp0 isn't necessary, it's part of docs#Prime

[Filippo A. E. Nuccio]

In the above code, lemma1 is a proof that under hP the ideal spanned by p is prime; and lemma2 is a proof that under hp0 the ideal spanned by p is non-zero.

[Filippo A. E. Nuccio]

And then in your example you can replace vp p by (DanielIdeal p hp).valuation.

[Daniel Weber]

Alright, thanks. Is IsDedekindDomain.HeightOneSpectrum.primeSpan a good name for this?

[Filippo A. E. Nuccio]

I think so. It can be put somwhere in RingTheory/DedekindDomain/Ideal.lean

[Filippo A. E. Nuccio]

No, actually SpanPrime is better

[Filippo A. E. Nuccio]

Because the general name is Span and in case of the span of a single element we have SpanSingleton, so I would advocate for SpanPrime.

[Daniel Weber]

Alright

[Daniel Weber]

Daniel Weber said:

I think you misunderstood, the result I'm using is something along the lines of

example (x : K) (h : ∀ p : F[X], Prime p → p.Monic → 0 ≤ vp p x) :
   IsLocalization.IsInteger F[X] x := sorry

and I'm not sure what to write in place of vp p in h.

This result is the second TODO in RingTheory.DedekindDomain.SInteger, right? What would be the best way to show this?