Examples of perfectoid spaces

[kbuzzard]

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.

[kbuzzard]

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]

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:

1. Allow the valuation to take values in arbitrary Gamma. (See also Definition of nondiscrete valuations #63)
2. Use injective functions instead of subrings.

(Edit: Oops, in the sketch above I forgot to demand compatibility between the topology on K and the valuation topology.)

[kbuzzard]

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]

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]

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:

• 1) Prove that the field K above is a perfectoid field (in the sense of

  lean-perfectoid-spaces/src/perfectoid_field.lean

  Line 35 in e9c4618

  class is_perfectoid_field (K : Type) [nondiscrete_valued_field K] (p : primes) : Prop :=

  )

Now let L be an arbitrary perfectoid field in the above sense.

• 2) Prove that L is a Huber ring and (L,L^o) is a Huber pair
• 3) Prove that Spa(L,L^o) is an adic space
• 4) Prove that Spa(L,L^o) is a perfectoid space.

[kbuzzard]

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,v_e) -> (K0,v_{e^p}).

(this should just be a straightforward calculation given what we have done above)

• Prove that all these valuations give isomorphic uniform space structures on K0

(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: K0_e -> K0_{e^p} induces an isomorphism K_e -> 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:

• prove that x mapsto x^p is a surjection on {x : K | v(x)<=1} (easy) and also on the quotient of this ring by the zero ideal :-/ (mathematically trivial)

[kbuzzard]

Corners that can be cut: instead of dealing with all e, we could just prove for example that v_e and v_{e^p} give isomorphic uniform space structures.

[kbuzzard]

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.

• Formalise the definition of a rank one valued field; prove that K is a rank one valued field.

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.)

• Deduce that F^o is {x : v(x) <= 1}

(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).

• Prove that F^o is adic (J=(pi) will work)

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}.

• Prove that F is a Huber ring.

Indeed F^o is an open adic subring.

• Prove that (F,F^o) is a Huber pair.

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+c_2x^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]

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.

Part 1

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.

• There must be some x in F with w(x) not equal to 1 or 0.

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.

• Hence there exists some x in F with w(x) > 1

Take the previous x and use its reciprocal if necessary.

• The pre-image of {g in {0} union Gamma | g <= 1} under w is a subring of F containing F^o

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).

• The only subrings of F containing F^o are F and 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.

• Hence the pre-image of {g in {0} union Gamma | g <= 1} under w must be F^o.

It can't be F because of x.

• Spa(F,F^o) has one point.

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).

Part 2

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).

• If v is in 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.

• If v is not in 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.

• All rat_open_data_completion.restrictions are surjections.

They're either F-hat -> F-hat or F-hat -> 0

• The value of the presheaf on {v} is isomorphic to the completion of F.

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.

• The value of the presheaf on {} is isomorphic to the zero topological ring.

All the rat_open_data_completions are zero.

• The stalk at v is F-hat, the valuation is the valuation on F-hat, the kernel is 0 which is a maximal ideal.

This by now is surely obvious.

• All values of the presheaf are complete rings

Case by case check.

• The presheaf is a sheaf.

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]

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.

• L is complete and Hausdorff

Completeness is an assumption and Hausdorffness should follow easily from the fact that there's a valuation.

• L is uniform

We showed above that the power-bounded elements of L were {x : v(x)<=1} which is bounded.

• There's a pseudouniformiser whose p'th power divides p

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.