idiomatic Lean

Stream: general

[Kevin Buzzard]

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]

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]

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

[Johan Commelin]

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

[Chris Hughes]

It's probably not that major.

[Johan Commelin]

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]

The longer you leave it the worse it will get.

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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)