p-adic valuation

Stream: Is there code for X?

[Michael Stoll]

I'm struggling to prove

example (x : ℚ_[2]) : (x^2).valuation = 2*x.valuation

It looks like it should be in the library, but suggest and library_search give me timeouts.

There is docs#add_valuation.map_pow , but it wants an explicit valuation as an argument, whose target is supposed to be a linear_ordered_add_comm_monoid_with_top, which I don't think ℤ is. I would think the corresponding statement should be an API lemma somewhere in the padics folder.

[Kevin Buzzard]

Yeah it looks like you're using padic.valuation which doesn't seem to have any API.

[Kevin Buzzard]

add_valuations are valuations which behave "correctly" on 0; padic.valuation isn't a valuation (it's additive) but it doesn't behave correctly on 0 (v(0)=0) so it's not an add_valuation either.

[Michael Stoll]

So what would be preferable?

1. Write an API for padic.valuation.
2. Change padic.valuation to be a well-behaved valuation (which would entail replacing the target by ℤ ∪ {∞}) and somehow set things up so one can use the general stuff.

[Adam Topaz]

Do we not have the p-adic valuation as a docs#valuation ?

[Michael Stoll]

No: docs#valuation is a multiplicative map; this corresponds to the p-adic norm.
We are talking about the additive valuation here.

[Adam Topaz]

Yeah, I understand, but I seem to vaguely remember @Aaron Anderson constructing the p-adic valuation as a (multiplicative) valuation, and presumably that would have involved a way to go back and forth between the additive and multiplicative version. But I might be misremembering, because I can't seem to find the multiplicative p-adic valuation.

[Michael Stoll]

There is docs#padic.has_norm; this is the multplicative valuation.

[Aaron Anderson]

I don't really remember getting anything closer to this than docs#multiplicity.add_valuation.

[María Inés de Frutos Fernández]

I was just talking about docs#padic.valuation with Kevin yesterday. I think this should renamed to something like padic.int_add_valuation (since as pointed out above it's not a docs#valuation).
I actually defined padic.add_valuation a couple of days ago (as an docs#add_valuation with values in with_top Z). I'll PR it now , and then #12914 could be used to get the corresponding absolute value.

[María Inés de Frutos Fernández]

I opened #12939.

[Michael Stoll]

I would like to keep the version with values in the integers as an alternative, since I imagine trying to work with the condition that the valuation is even (say) is likely to be a bit painful when it is of type with_top ℤ instead of ℤ.

[Eric Wieser]

I'm not at all familiar with the area, but it feels rather messy that the definition of all this stuff around padic norms seems to expand to an if with a special case, rather than letting a with_bot handle the special cases somehow

[Adam Topaz]

As long as with_top \Z has whatever algebraic structure mimics comm_group_with_zero, then it should be natural enough to use without always translating to \Z. I assume we have docs#add_comm_group_with_top ?
Edit: it's docs#linear_ordered_add_comm_group_with_top

[Michael Stoll]

How would even n and odd n be defined for n : with_top ℤ?
I don't see a way around distinguishing cases here.
(Background: I want to formulate (and prove) a statement like "a nonzero p-adic number is a square iff...".)

[Adam Topaz]

If we generalize docs#even and docs#odd slightly, it would be possible.

[Adam Topaz]

import ring_theory.valuation.basic

def even' {α : Type*} [has_one α] [has_zero α] [has_add α] [has_mul α] (a : α) : Prop :=
  ∃ k, a = 2 * k

def odd' {α : Type*} [has_one α] [has_zero α] [has_add α] [has_mul α] (a : α) : Prop :=
  ∃ k, a = 2 * k + 1

example (a : with_top ℤ) : Prop := even' a
example (a : with_top ℤ) : Prop := odd' a

[Adam Topaz]

Of course, $\infty$ would be both even and odd, but :shrug: ...

[Damiano Testa]

Note that there is already a more general proposal for even: #13037.

[Adam Topaz]

@Damiano Testa does your PR also includes a generalization of docs#odd ?

[Adam Topaz]

It seems that the answer is "no". But perhaps if all @Michael Stoll needs is even, then that's okay.

[Michael Stoll]

even is sufficient for what I have in mind for now.

[Reid Barton]

Is there something special about divisibility by 2 in this context?

[María Inés de Frutos Fernández]

Michael Stoll said:

I would like to keep the version with values in the integers as an alternative, since I imagine trying to work with the condition that the valuation is even (say) is likely to be a bit painful when it is of type with_top ℤ instead of ℤ.

I would vote for keeping both versions, with some API relating them (same as for polynomials we have nat_degree with values in ℕ and degree with values in with_bot ℕ).

[Adam Topaz]

@Reid Barton -- I don't know exactly what result Michael has in mind here, but the multiplicative group of $\mathbb{Q}_p$ with $p$ odd has a very explicit description: $\mathbb{Q}_p^\times \cong \mathbb{Z} \times \mathbb{F}_p^\times \times (1 + p \cdot \mathbb{Z}_p)$ where the first component is the valuation, the second is the Teichmuller representative of the first nonzero coefficient in the Teichmuller expansion, and the rest is "the rest". By Hensel's lemma "the rest" consists of squares (since $p$ is odd), so to test whether you have a square in $\mathbb{Q}_p^\times$ you need to do ensure that the valuation is even and that the part in the residue field is a square, which means you need to compute some Legendre symbol. You can generalize this in various ways, but I think the statement for squares is natural enough to be in mathlib.

[Damiano Testa]

Adam, the PR above only deals with even.

There has been a discussion about this in a different thread (General - even/odd, I think, but I'm on mobile now). The conclusion was that even was "more fundamental".

Besides, I am still not sure if I prefer odd to require also the existence of a 1, making the two notions asymmetric, or whether it is better to define odd = ¬even and get the usual 2*n+1 only once you assume more.

[Damiano Testa]

Honestly, regardless of whether it is called odd or not, ¬even is a much better concept than ∃n, x=2*n+1.

[Damiano Testa]

I also thought that introducing is_square at the same time as refactoring even was more than enough for a single PR!

[Damiano Testa]

Regarding using with_top ℤ, I very much like the option of keeping both. One thing that I had not noticed earlier is that you cannot subtract one from a degree, since subtraction is not defined on the type. Nevertheless, it is very useful to be able to talk about subtracting valuations!

[Damiano Testa]

Now at a computer: this is the chat and approximate location of the discussion relevant to what the PR contains.

[Adam Topaz]

María Inés de Frutos Fernández said:

I would vote for keeping both versions, with some API relating them (same as for polynomials we have nat_degree with values in ℕ and degree with values in with_bot ℕ).

I completely agree with this -- we need a good API to go back and forth between the two notions.

But the valuation theory situation in mathlib still bothers me for some reason. We have this docs#padic.valuation as a map from $\mathbb{Q}_p$ to $\mathbb{Z}$ which behaves as expected on nonzero elements and sends $0$ to $0$. But we don't have a version which is a homomorphism $v_p : \mathbb{Q}_p^\times \to \mathbb{Z}$. If we had such a $v_p$, then we could define padic.valuation using if h : x = 0 then 0 else v_p (units.mk0 x h) (cf. docs#units.mk0 ). In general it seems pretty strange to me that we can consider docs#add_valuation on fields taking values in with_top \Z, but we don't have anything that would let us work with a valuation of the form $v : K^\times \to \mathbb{Z}$.

[Kevin Buzzard]

Choosing an orientation for v_p is like deciding whether your canonical Frobenii are going to be arithemetic Frobenii or geometric Frobenii

[Adam Topaz]

Why? $v_p(p) = 1$.

[Kevin Buzzard]

No, it really is not, is it.

[Kevin Buzzard]

Inversion on $K^\times$ doesn't extend to a ring morphism

[Adam Topaz]

The issue with defining valuations as $v : K^\times \to \Gamma$ is that the theory for valuations on rings must involve the top from the very start, since you have have nonzero elements mapping to top. The field case is still an important special case, as one can prove that any valuation on a commutative ring arises from a valuation on the residue field of one of its primes. In this sense, it might be worthwhile to focus more on developing the theory for valued fields where one can have a nice picture using valuations of the form $v : K^\times \to \Gamma$.

[Kevin Buzzard]

Why can't we have a predicate is_isomorphic_to_top_of Gamma?

[Adam Topaz]

Yeah! I think that's a very good idea.

[Kevin Buzzard]

Is it called is_top? What's the corresponding naming convention for localisations? docs#localization

[Adam Topaz]

I assume you want some predicate saying that a linear_ordered_comm_group_with_top is isomorphic to with_top \Gamma?

[Kevin Buzzard]

ha, is_top is taken!

[Yaël Dillies]

I wonder who took it :grinning:

[Kevin Buzzard]

Adam I think you're right. I have learnt a bunch about valuation theory recently. For the perfectoid project there were rings everywhere, we couldn't use this hack. But I remember skipping over a bunch of proofs because we didn't need them for the definition of a perfectoid space but would need to be able to build one jot of API, and valuation theory of fields was in the part which we skipped.

[Kevin Buzzard]

Do you think there should be a field_valuation K \Gamma typeclass? And then a bridge: if I have a ring R with is_field R and a monoid with zero M then you give me a field_valuation R Mˣ and conversely if you give me a field_valuation K \Gamma I'll return a valuation K (with_zero \Gamma)

[Adam Topaz]

Yeah, that might be the way to go (sorry, I can't discuss this more right now, even though I would like to! I have to teach in 25mins.)

[Kevin Buzzard]

Or how about this: make is_field a class and then just make a more fieldy API contructors/eliminators but leave the implementation. Although I guess we don't seem to have an is_group predicate on monoids -- do we? docs#is_group

[Michael Stoll]

Reid Barton said:

Is there something special about divisibility by 2 in this context?

If you are interested in squares (which I am right now because of the relation to quadratic Hilbert symbols), then yes. But of course, if you look at n-th powers more generally, then divisibility by n will be relevant.

[Reid Barton]

I guess a better formulation of my question would have been: are you going to face a similar issue regarding "valuation is divisible by $n$" for $n > 2$, and if so, is it worth giving special attention to the statement for $n = 2$

[Michael Stoll]

In this respect, I'd say no. On the other hand, divisibility by 2 is already given special attention -- we don't have an analogue of even for divisibility by 3, say.