valuation API

[kbuzzard]

We have made a lot of recent progress on the valuation API; I've worked on this for a couple of days but now need to get back to other things, so here's a quick summary of where we are.

Given a valuation v : R -> Gamma union {0}, let $$K$$ be the field of fractions of $$R/supp(v)$$, extend the valuation to $$K$$, and let $$A^\times\subseteq K^\times$$ be the things of valuation 1. We have checked that $$K^\times/A^\times$$ is a totally ordered group and it's called canonical_ordered_group v. The valuation $$v$$ factors through a valuation taking values in this group, and this valuation is called canonical_valuation v. The lemma canonical_valuation.map says that the canonical valuation composed with the natural map canonical_ordered_group.toΓ v from canonical_ordered_group v to Gamma recovers v. I am not wedded to these names by the way! It's just how I was thinking of them.

Here are the things still to be done for the valuation API to be complete:

1) I proved that canonical_ordered_group.toΓ v is a group hom, but we need to show it preserves <=.

2) Prove that the inequality corresponding to canonical_valuation v is the inequality corresponding to valuation v, i.e. prove that v is equivalent to canonical_valuation v. I think that this trivially follows from 1 and canonical_valuation.map.

3) Make a quotient API for Spv. Define lift by evaluating on the canonical valuation. Prove the computation rule from the fact that v is equivalent to its canonical valuation.

4) We need to understand exactly how much of Wedhorn 1.27 we now need. Our goal here is to prove that continuity is constant across equivalence classes. My proposed new definition of the value group is just canonical_ordered_group v -- it is isomorphic to the value group. The proof that equivalent (in our sense) valuations have isomorphic value groups now becomes the statement that equivalent valuations have the same K and the same $$A^*$$, which I think Johan must have done. That means that equivalent valuations have isomorphic canonical_valuations, so one is continuous iff the other is.

All this is easily within sight now, as far as I can see.

It might be easiest to just comment out all the minimal_valuation stuff right now because we should never have to use it -- the canonical valuation replaces this stuff; the canonical valuation has all the properties that the minimal valuation had, and more.

[jcommelin]

I've pushed (1) and (2).

[kbuzzard]

This is all now done.