Zulip Chat Archive

Stream: general

Topic: idiomatic Lean


Kevin Buzzard (Jul 08 2019 at 17:06):

I am slowly learning the importance of writing "idiomatic Lean".

I want to develop a theory of rank 1 valuations on fields. I already have a theory of arbitrary valuations on rings:

class valuation.is_valuation [ring R] (v : R  with_zero Γ) : Prop :=
(map_zero : v 0 = 0)
(map_one  : v 1 = 1)
(map_mul  :  x y, v (x * y) = v x * v y)
(map_add  :  x y, v (x + y)  v x  v (x + y)  v y)

/-- Γ-valued valuations on R -/
def valuation (R : Type u₀) [ring R] (Γ : Type u) [linear_ordered_comm_group Γ] :=
{ v : R  with_zero Γ // valuation.is_valuation v }

with more details at

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/valuation/basic.lean#L75

I am now interested in the case where (1) R is a field, (2) Gamma is the group of positive reals and (3) there exists some r in R such that v(r) is neither 0 nor 1, or equivalently the group homomorphism R^* -> Gamma is non-trivial, or equivalently the induced topology on R is not discrete, or any number of other equivalent things.

I would like to formalise this definition "correctly". I am not very good at this. I would imagine there are good and bad ways to do this. For starters, even though with_zero Gamma is the non-negative reals, I can't find the positive reals in mathlib. Are they there and I missed them? There is a big theory of valuations taking values in the non-negative reals, but there is also a theory of valuations taking values in with_zero Gamma which we already set up in the perfectoid project and it's in some sense a shame that I am going to have to make another nnreal as with_zero posreal.

As for the statement that the valuation is non-trivial, this seems a bit artificial however I do it. Aah! In practice the kind of thing people need is a "pseudouniformiser", namely an element of the field whose valuation is strictly between 0 and 1. Maybe I will just assert that a pseudouniformiser exists. Does that sound crazy?

Johan Commelin (Jul 08 2019 at 17:28):

I am also quite interested in suggestions how to bridge the gap between the theory developed for valuations taking values in with_zero Gamma and valuations taking values in nnreal.

Chris Hughes (Jul 08 2019 at 17:56):

I think the way is to define valuations on some class that doesn't exists yet instead of with_zero

Johan Commelin (Jul 08 2019 at 17:58):

O.o... major refactor of the entire perfectoid project...

Chris Hughes (Jul 08 2019 at 18:04):

It's probably not that major.

Johan Commelin (Jul 08 2019 at 18:08):

Well... we have a lot of stuff on manipulating valuations, equivalences of valuations, replacing the value group with another group, extending valuations, defining the canonical valuation, etc... etc...

Chris Hughes (Jul 09 2019 at 09:21):

The longer you leave it the worse it will get.

Kevin Buzzard (Jul 09 2019 at 20:56):

This would involve making a new class I think. Currently our class is with_zero Gamma with Gamma a totally ordered comm_group (group law *) and the group law extended to 0 by 0*x=0 and the order extended by letting 0 be bot. I have convinced myself this evening that we cannot go as general as totally ordered comm_monoids with 0 because then rings will start having extra valuations which we don't want (the adic spectrum of a ring is the equivalence classes of valuations and we definitely don't want that type to change up to anything more than an equiv).

The two natural choices for a new class are (1) totally ordered comm_monoids with 0 and with the property that if you remove 0 then you get a group, or (2) totally ordered comm_monoids with 0 and with the property that if you remove 0 then you get a cancellative monoid (i.e. a submonoid of a group). The notion of equivalence, which we're always working with when it comes to valuations, means that we only really care about the image of the valuation. Two valuations are equivalent if their images in the respective with_zero Gamma's are isomorphic and the isomorphism commutes with the valuations.

Somehow I am now coming to the conclusion that we just want to make a new mathematical object, a totally ordered comm_monoid with a 0 and with the property that everything non-zero cancels.

It's probably not that major.

@Chris Hughes the definition of a valuation is line 1 of the first file we import in the 10000+ line project. Can it really not be major?


Mario Carneiro (Jul 09 2019 at 21:04):

with the property that everything non-zero cancels

This sounds suspiciously similar to the multiplication and division in a division ring or field

Mario Carneiro (Jul 09 2019 at 21:05):

How much do you actually use Gamma itself? Everything of interest seems to be happening in with_zero Gamma in your examples

Mario Carneiro (Jul 09 2019 at 21:06):

Would it work if you just had some Gamma_0 being a typeclass like you said and use units Gamma_0 in place of Gamma?

Kevin Buzzard (Jul 09 2019 at 21:28):

For a valuation on a general commutative ring, the axioms of valuations imply that the stuff sent to zero is a prime ideal, which can reasonably be regarded as the kernel of the valuation; quotienting out by the kernel gives an integral domain A, and the valuation induces a (not necessarily injective) monoid map from A to this with_zero thing. The big difference between a division ring/field is that with_zero Gamma does not have an addition.

Kevin Buzzard (Jul 09 2019 at 21:29):

An example one might keep in mind is {0} union {e^0,e^1,e^2,...} with 0<e<1.

Kevin Buzzard (Jul 09 2019 at 21:29):

e.g. {0,1,1/2,1/4,1/8,...}

Kevin Buzzard (Jul 09 2019 at 21:30):

We don't ever really care about Gamma. I guess one thing that shows up in some of the arguments is the subgroup of Gamma generated by the image of (R - stuff which got sent to zero).

Kevin Buzzard (Jul 09 2019 at 21:31):

In fact given the valuation, to whatever target, one can in some sense reconstruct the correct Gamma by taking the field of fractions K of A the integral domain, and then letting Gamma be units(K)/units(A)


Last updated: Dec 20 2023 at 11:08 UTC