Ostrowski theorems formalized in Lean 3

Stream: maths

[Filippo A. E. Nuccio]

I was trying to play a bit with @Adam Topaz ' definition and I have a basic question about comm_group_with_zero: it seems to me that the "extended integers" $\mathbb{Z}\cup\{\infty\}$ are a comm_group_with_zero when declaring $\infty \cdot a=a\cdot \infty=\infty$ for every $a : \mathbb{Z}$. Then why can't we define the $p$-adic valuation as taking values here rather than in $\mathbb{Z}$ with the declaration $v(0)=0$ (as it is now in https://leanprover-community.github.io/mathlib_docs/number_theory/padics/padic_numbers.html#padic.valuation )?

[Adam Topaz]

That would break the fact that the units of the valuation are the elements with valuation zero (if you're using the additive notation for the value group).

[Yakov Pechersky]

It's not a comm_group_with_zero because what happens to 0? It doesn't have an inverse.

[Yakov Pechersky]

Unless you mean that 0 is the zero and the inverse of infty is infty

[Adam Topaz]

I think he means linear_ordered_add_comm_group_with_infinity

[Adam Topaz]

Which might not exist?

[Yakov Pechersky]

It's with_top

[Yakov Pechersky]

There's docs#linear_ordered_add_comm_monoid_with_top, docs#linear_ordered_add_comm_group_with_top

[Filippo A. E. Nuccio]

Yes, I mean a lin_ord_ab_group_with_inf, and I might have a look at that with_top instead.

[Filippo A. E. Nuccio]

Adam Topaz said:

That would break the fact that the units of the valuation are the elements with valuation zero (if you're using the additive notation for the value group).

I am sorry, but I don't understand why.

[Adam Topaz]

Because zero is not a unit?

[Adam Topaz]

Maybe I misunderstood the question?

[Filippo A. E. Nuccio]

Ok, I try to explain myself better: if we add to the additive group $\mathbb{Z}$ the element $\infty$ and we call it zero (so the one of the group is 0 : int and the zero of the group is $\infty$), don't we get a comm_group_with_zero when declaring that $\infty$ absorbs everything (additively)?

[Filippo A. E. Nuccio]

Now $\mathbb{Q}_p\rightarrow\bar{\mathbb{Z}}$ and I don't see problems with $0 : \mathbb{Q}_p$ which is the only guy sent to $\infty$.

[Adam Topaz]

Oh, but that's already what's been done... So what's the issue?

[Adam Topaz]

Just that it's not defeq to Z?

[Adam Topaz]

I'll move this thread to the maths stream where it belongs...

[Filippo A. E. Nuccio]

No, well, my "issue" is that here https://leanprover-community.github.io/mathlib_docs/number_theory/padics/padic_numbers.html#padic.valuation the p-adic valuations sends $0$ to $0$, not to $\infty$.

[Yakov Pechersky]

It's not a comm_group_with_zero because there are no multiplicative inverses. Do you mean add_comm_group...?

[Filippo A. E. Nuccio]

Ah, sure, thanks.

[Yakov Pechersky]

And there is no add_comm_group_with_* because add_comm_group already has zero, and no one has made the with_blah version for it.

[Filippo A. E. Nuccio]

Great, I see. I though the difference was just a matter of notation.

[Adam Topaz]

Adam Topaz said:

I'll move this thread to the maths stream where it belongs...

I can't seem to move the messages... how does this work again?

[Patrick Massot]

You simply wait for someone else to do it.

[Filippo A. E. Nuccio]

@Adam Topaz At any rate, I was just trying to add another possible definition to your file, and I got stuck when trying to prove that in my definition the p-adic integers are a valuation ring. Should I push to your branch or create another one?

[Adam Topaz]

Johan Commelin said:

That definition (assuming you are talking about (2) above) and the corresponding valuation $v \colon \mathcal O \to \Gamma$ are already in the perfectoid project. Not sure how much of this "canonical valuation" has made it to mathlib.

@Johan Commelin IIRC the perfectoid project doesn't have a definition of a valuation ring...

[Adam Topaz]

@Filippo A. E. Nuccio feel free to push to my branch, but I think the better way to approach this is to prove that $\mathbb{Z}_p$ is a DVR, and prove that DVRs (in the sense of mathlib) are valuation rings.

[Adam Topaz]

Presumably the fact that $\mathbb{Z}_p$ is a DVR is already in mathlib?

[Filippo A. E. Nuccio]

OK, I will need to go but I'll push, at any rate. We might discuss this further, perhaps, if you want.

[Adam Topaz]

@Filippo A. E. Nuccio what's happenning with this code you pushed?

class valuation_ring' (R : Type u) {K: Type u} [integral_domain R] [field K] [algebra R K]
  [is_fraction_ring R K] (v : valuation K Γ₀) : Prop :=
(int_cond : R = {x : K | v x ≥ 0})

[Adam Topaz]

Does this even compile?

[Filippo A. E. Nuccio]

It does

[Johan Commelin]

@Adam Topaz Right, the pftd project defines $\Gamma$ and the canonical valuation for an arbitrary starting valuation. But still I think a lot of stuff can be reused. Building the quotient $\mathcal O/\mathcal O^*$ and the canonical valuation will still be the same.

[Adam Topaz]

How? R is a type and { x : K | ... } is a set.

[Filippo A. E. Nuccio]

Yes, this looked very strange to me.

[Adam Topaz]

(One more note: the mathlib valuations are written multiplicatively so it should really be {x : K | v x \le 1 }.)

[Filippo A. E. Nuccio]

Oh, this is certainly correct

[Filippo A. E. Nuccio]

At any rate I will modify it tomorrow, also trying to understand how it possibly compiles.

[Filippo A. E. Nuccio]

My point was that when playing with extending valuations for ramified extensions, a bit of flexibility might have been useful rather than having "the canonical one", that's all.

[Adam Topaz]

@Johan Commelin I think the main issue that won't be covered by the code from the perfectoid project is the order on the value group. It seems that you start with a valuation, and construct the order on the "canonical" value group by embedding it in the original value group, using the ordering from the value group of the given valuation. In this case, we don't start with a valuation so we have to construct the order from scratch using the axioms of a valuation ring.

[Adam Topaz]

(By the way, the reason @Filippo A. E. Nuccio 's code above compiles is because lean coerces the set to a type, then asks for an equality of types, so this is not a good definition)

[Adam Topaz]

Perhaps what we should do is define a gadget consisting of the following data: A commutative ring $A$, a prime ideal $\mathfrak{p}$, and a valuation ring $R$ which is a localization of $A/\mathfrak{p}$. This way you can associate such a gadget to any valuation, and conversely associate a valuation to any gadget.

[Filippo A. E. Nuccio]

At any rate I wanted to improve that part of code, so it will certainly be changed. But thanks for the check!