Open kbuzzard opened 5 years ago
kbuzzard
commented
5 years ago In fact things are murky well before point 7. To define the valuation on Q_p-bar we will need to define a valuation on finite extensions of Q_p, so we need to be able to extend valuations to finite extensions. This already needs some thought.
jcommelin
commented
5 years ago https://github.com/leanprover-community/lean-perfectoid-spaces/blob/perf-fld/src/examples/char_p.lean#L192 contains a rought proposal for the definition of a perfectoid field:
class perfectoid_field : Type 1 :=
[fld : discrete_field K]
[top : uniform_space K]
[top_fld : topological_division_ring K]
[complete : complete_space K]
[sep : separated K]
(v : valuation K nnreal)
(non_discrete : ∀ ε : nnreal, 0 < ε → ∃ x : K, 1 < v x ∧ v x < 1 + ε)
(Frobenius : surjective (Frob v.le_one_subring ∕p))We might want to tweak this to:
(Edit: Oops, in the sketch above I forgot to demand compatibility between the topology on K and the valuation topology.)
kbuzzard
commented
5 years ago The definition in Scholze's original paper is that a perfectoid is a field + non-discrete real-valued valuation (i.e. image of K^* is a non-discrete subgroup of the positive reals and hence a dense subgroup) with two conditions: first, if we equip K with the valuation topology then it's a complete topological field, and second: the map x \mapsto x^p (Frobenius) is surjective on K^0 / p.
kbuzzard
commented
5 years ago There are other equivalent definitions, and some of the equivalences need the open mapping theorem (for p-adic Banach spaces -- the usual proof (by which I mean "the one I know") goes through in the p-adic case too).
kbuzzard
commented
5 years ago OK so I will attempt to write down our path to a non-empty perfectoid space. It's not hard to check that if we want a non-empty perfectoid space we need a perfectoid ring. One route to a perfectoid ring is to make a perfectoid field (which perhaps counterintuitively is a slightly simpler object and is also of independent interest). Indeed, being able to tell people "we have an example of a perfectoid field" will, I feel, already indicate some kind of progress in this area.
We already have (in the perf-fld branch) the field K, the completion of the perfection of $$k((t))$$ with $$k$$ a finite field of characteristic $$p$$. So a route to a perfectoid space is:
Now let L be an arbitrary perfectoid field in the above sense.
kbuzzard
commented
5 years ago Now let me try and break down what needs to be done in these four check boxes.
Let k be a perfect field of characteristic p (e.g. a finite field of char p e.g. Z/pZ). Let K0 be the perfection of k((t)). Let K be its completion.
To prove that the field K=\widehat{Z/pZ((t^{1/p^infty}))} above is a perfectoid field, we need to do several things but I know my coauthors have done some of them already. Rather than plough through the repo again I will just write a bunch of stuff knowing we have already done some of it.
[ ] Prove that the absolute Frobenius x \mapsto x^p is an isomorphism of fields K0 -> K0.
[ ] Define a family of (non-negative real)-valued valuations v_e on K0 sending t to e. Here e can be any real with 0<e<1.
(mathematical paranthetical remark -- if k is a finite field of size q then there is a natural choice of e, namely e=1/q; this choice has something to do with relating additive and multiplicative Haar measures and is important if you're going on to do arithmetic, which we're not. If k is a random perfect field then there is no natural choice for e)
[ ] Prove that all of these are valuations.
[ ] Prove that Frobenius is an isomorphism of valued fields (K0,ve) -> (K0,v{e^p}).
(this should just be a straightforward calculation given what we have done above)
(the topology on K0 induced by v_e comes from a metric d_e(x,y)=v_e(x-y) and given e and e' with 0<e,e'<1, then for all epsilon, there exists a delta such that d_e'(x,y) < delta implies d_e(x,y) < epsilon; this is because one can prove that v_e'(x) = v_e(x)^{log e' / log e})
[ ] Define K_e to be the completion of the field K0 with the uniform space structure coming from v_e.
[ ] Extend the valuation on K_e and prove it's a field.
[ ] Prove that x\mapsto x^p: K0e -> K0{e^p} induces an isomorphism Ke -> K{e^p}.
[ ] Prove that this isomorphism is also x\mapsto x^p (because both maps are continuous and they agree on the dense subset K0)
[ ] Extend v_e to a valuation (also called v_e) on K.
[ ] Prove K is a field.
[ ] Prove that the valuation v_e on K is nondiscrete
(this is some lemma saying that if you have r>1 a real and you keep taking its p'th root then eventually you'll be less than 1+epsilon, this just follows from the fact that (1+epsilon)^p>=1+p*epsilon which can be proved by induction on p)
Now we have all the ingredients for showing that K is a perfectoid field in the sense of the definition above. Oh -- we just need one more thing actually:
kbuzzard
commented
5 years ago Corners that can be cut: instead of dealing with all e, we could just prove for example that ve and v{e^p} give isomorphic uniform space structures.
kbuzzard
commented
5 years ago OK. Now imagine that we have a perfectoid field L in the sense above. How do we prove it relates to all this Huber ring / Huber pair stuff? In the perf-fld branch we already have the le_one_subring function giving us a ring from a field. So we'd better start by proving that L^o = L.le_one_subring. I guess the correct thing to do from the point of formalisation is to do this properly, and develop some of the theory of Tate rings. Tate rings are easier to manage than general Huber rings, a Tate ring has a topologically nilpotent unit which enables us to "scale" problems. In fact I think we need a basic theory of nonarchimedean fields in the sense of nonarchimedean analysis. Wait -- we don't even need completeness here. We need a basic theory of fields equipped with a valuation v to the non-negative reals, and with the assumption that the image of v is strictly larger than {0,1}. This is even simpler than the theory of nonarchimedean fields, which are fields equipped with such a valuation and with the extra property that the field is complete wrt the induced metric.
Definition: a rank one valued field is a field equipped with a valuation v to the non-negative reals such that there exists an element pi of the field whose valuation v(pi) satisfies 0<v(pi)<1. Johan -- do you know a better name? My suggestion is a bit clunky but it is mathematically sensible because the rank of a valuation is the height of the image in Gamma, and a subgroup of the positive reals has height 1 iff it's non-trivial. I think my formalisation of the non-triviality of v here (asking for something with valuation between 0 and 1) will be useful because in practice I know that pi with 0<v(pi)<1 is precisely the useful thing you need to do stuff -- it's a pseudouniformiser.
Now let F be a rank 1 valued field, because all the below works in this generality.
[ ] Prove that F is a valued field and hence a topological ring
[ ] Prove that a subset of F is a neighbourhood of 0 iff it contains a subset of the form {x : v(x)<epsilon}
[ ] Prove that a subset of F is bounded iff it's contained in a closed ball {x : v(x)<=N}
(this should follow from the previous point relatively straightforwardly; note that we already know a subset of a bounded thing is bounded.)
(if v(x) <= 1 then powers of it are contained in closed unit disc; if v>1 then powers are not contained in any closed disc).
The issue here is to prove that the topology coming from the valuation is equal to the topology coming from (pi). We know v(pi)<1. Note that J={x : v(x)<=v(pi)} and more generally J^n=(pi^n)={x : v(x)<=pi^n}; certainly an F^o-multiple of pi^n has valuation <= v(pi)^n because F^o={x : v(x)<=1}; conversely if v(x)<=v(pi)^n then v(x/pi^n)<=1 in F and hence x/pi^n is in F^o. Now it's easy to prove that the neighbourhoods of zero are the same. I assume the topology on F is defined coming from the metric d(x,y)=v(x-y). Then every neighbourhood of zero contains {x : v(x)<epsilon} for some epsilon>0 and if we choose N such that v(pi)^N<epsilon then J^N is contained in this neighbourhood; conversely J^N contains {x : v(x)<v(pi)^n}.
Indeed F^o is an open adic subring.
I think the only thing not already done is to prove that F^o is integrally closed in F. So say x is in F and x is a root of a monic polynomial with coefficients in F^o. The maths proof here is not so hard, but this might be a pain to formalise. We want to prove v(x)<=1. By contradiction. If v(x)>1 and q(X)=X^n+... is the monic polynomial then x^n=c_0+c_1x+c2x^2+...+c{n-1}x^{n-1}, but everything on the RHS has valuation <= v(x)^{n-1}, so the sum has valuation <= v(x)^{n-1} too, whereas the LHS has valuation v(x)^n>v(x)^{n-1} if v(x)>1, a contradiction.
kbuzzard
commented
5 years ago Spa(L,L^o) is an adic space: again this will work for any rank one valued field. So again let F be a rank one valued field with valuation v. Let Fhat be its completion.
it's clear that every point of Spa(F,F^o) is contained in some Spa(R,R^+) for (R,R^+) a Huber pair, because we just showed that (F,F^o) is a Huber pair, so the work here is in giving Spa(F,F^o) the structure of a CLVRS. It's already a topological space. The proposal here is kind of atrocious -- we should really be proving that Spa(R,R^+) has lots of nice properties for a more general class of R, but unfortunately some nice properties (like the presheaf being a sheaf) really are not true for a general (R,R^+). The strategy comes in two parts:
Part 1: Spa(F,F^o) has only one point. Part 2 : Spa(F,F^o) is a CLVRS.
We need to prove that if w is a continuous valuation (valued in {0} union Gamma) on F with w(x)<=1 for all x in F^o (i.e. if w is in Spa(F,F^o), then w is equivalent to v.
If w only took the values 1 and 0 then by continuity the support of w would be an open proper ideal of F, but the only proper ideal of a field is {0} and {0} is not open.
Take the previous x and use its reciprocal if necessary.
It's a subring (this must be a general result for all valuations) and it contains F^o by definition of Spa(F,F^o).
Let R be such a subring. Then R is a sub-F^o-module of F. If it's strictly bigger than F^o then choose some element f with v(f)>1 (v the rank 1 valuation on F); then for every element y of F choose some natural N with v(f)^N>v(y) and then observe that y/f^N is in F^o and hence in R, so y is in R too, but y was arbitrary.
It can't be F because of x.
We just showed that for w an arbitrary valuation, w(s)<=1 iff v(s)<=1, where v is our fixed valuation on F. This means that w(s)<=w(t) iff v(s)<=v(t) (consider s/t).
Now we need to show that if Spa(F,F^o) can be beefed up from a PreValuedRingedSpace to a CLVRS. We have a space, a topology, a presheaf and a valuation. We want a the presheaf to be a sheaf, but we also want that all global sections are complete rings, we want that the stalk is local (there's only one), and we want that the support of the valuation on the stalk is maximal.
Everything comes back to this "rational open data" stuff. We think of rational open data as an element s of F and a finite subset T of F generating an open ideal. This is just the same as "having at least one non-zero element". Let v denote the unique element of Spa(F,F^o). The key intermediate step we need is this. Let r : rational_open_data (F,F^o).
r.open_set then rat_open_data_completion r is a topological ring equipped with a map from F and this is isomorphic to the completion of F.The maths proof goes like this. rat_open_data_completion ris the completion of F(T/s):=F[1/s] with respect to some topology depending on T. Now v is in r.open_set so s isn't 0 so F(T/s)=F as a field and F -> F(T/s) is continuous. The universal property of F(T/s) (Wedhorn 5.51) implies that there's a continuous F-algebra map F(T/s)->F extending the identity on F, and this shows that the inverse of F->F(T/s) is continuous. Hence F is topologically isomorphic to F(T/s), and thus F<T/s>is just the completion of F.
r.open_set then rat_open_data_completion r is the zero topological ring.If s=0 then F(T/s)=F[1/s]=0 and so its completion is 0. If s isn't 0 then there's some t such that v(t/s)>1, and this element is in the subring D of Wedhorn 5.51 proof, meaning that the fundamental system of neighbourhoods of zero defining the topology on F(T/s) are all equal to F. Hence F(T/s) has the indiscrete topology (only two open sets) and its completion is then zero.
rat_open_data_completion.restrictions are surjections.They're either F-hat -> F-hat or F-hat -> 0
The rational_open_data with T={1} and s=1 give us a rational_open_data involved in the definition of the presheaf, and projection gives us a map from the presheaf on {v} to the rat_open_data_completion at this data. Because all restriction maps are surjections we get a map the other way too; composition in both directions is clearly the identity.
All the rat_open_data_completions are zero.
This by now is surely obvious.
Case by case check.
Its value on the empty set is the zero ring and that's enough, a brute force proof will work.
Note: this looks like many hours of work to me, even though I think we have all the preliminaries.
kbuzzard
commented
5 years ago Spa(L,L^o) is a perfectoid space for L a perfectoid field: it suffices to prove that L is a perfectoid ring. Because "perfectoid field" has a completely different definition to "perfectoid ring" this still needs some argument, but it's trivial given what we have.
Completeness is an assumption and Hausdorffness should follow easily from the fact that there's a valuation.
We showed above that the power-bounded elements of L were {x : v(x)<=1} which is bounded.
Choose any x with 0<v(x)<1 (enough for char p) and v(p)/p<x (needed in char 0). Check p/x^p has valuation at most 1.
Frobenius being surjective on L^o/p is part of the assumption of a perfectoid field.
Other than the empty space we currently have no examples of perfectoid spaces. The most natural class of examples would be to prove that if K is a perfectoid field then Spa(K) is a perfectoid space, and then to give examples of perfectoid fields. I guess the natural example is the completion of an algebraic closure of the p-adic numbers.
Route to examples of perfectoid spaces (needs fleshing out):
1) Get algebraic closures of char 0 fields. 2) Define the valuation on Q_p-bar. 3) Put the valuation topology on Q_p-bar and complete. The valuation extends (we have this). 4) The completion is a field (we might well have this as well). 5) Let C be the completion and let R be its valuation ring. Prove C is a Huber ring and (C,R) is a Huber pair. 6) If v in Spa(C) then by definition v<=1 on R, so the valuation ring of v is either R or some bigger ring; but any subring of C containing R and an element with norm bigger than 1 must be all of C. Moreover, the trivial valuation is not continuous. Hence Spa(C)={obvious valuation}. 7) Now things get a bit murky. The definition of the structure sheaf on an open is a projective limit. We do not yet know that the structure sheaf evaluated at a rational open corresponding to (T,s) is C<T/s>, but all we need to do is to prove the sheaf axiom for a one point set so we can just do it directly.