Theorem: to give a term of type perfectoid space X is to give a perfectoid space (in the sense used in the mathematical literature).
Proof: Looking at the definition of perfectoid space in our repository, and comparing it with the definition in the literature, one sees that there are two instances where we do not follow the definition in the literature, but instead do something equivalent. Here is the justification that what we do is equivalent.
1) Theorem: if A is a Huber pair, then the topology on Spa(A) generated by the basic open sets is the same as the topology on Spa(A) generated by the rational open sets.
Traditionally in the literature the topology on Spa(A) is defined to be the one generated by basic open sets, but in our repository we used the one generated by rational open sets. A reference in the informal literature for the fact that these topologies coincide is Theorem 3.5(ii) of "Continuous Valuations", by R. Huber (Math Z 212, 455--477, 1993).
Once this theorem is formalised in Lean, we can change our definition of the topology to be the one generated by the basic opens and thus conform more closely to the literature.
2) The presheaf on Spa(A) on a general open set U as defined in the literature (a projective limit over all rational open subsets) is isomorphic to the presheaf on Spa(A) as defined in our repository.
A reference for the definition of the presheaf on Spa(A) in the informal literature is the definition just after the end of the proof of Lemma 1.5 in "A generalization of formal schemes and rigid analytic varieties", by R. Huber (Math Z 217, 513--551, 1994). The reason we do not use this definition is that we have not yet formalised the proof of Lemma 1.5(i) of Loc Cit, a geometric universal property of rational open subsets. As a consequence we cannot define all of the morphisms between rings involved in Huber's projective limit. Instead we use a trick. If U and V are rational subsets of Spa(A) and V is a subset of U, then we can define restriction maps from O_X(U) and O_X(V) to an auxiliary ring R, and use these two maps instead of the map O_X(U)->O_X(V) in our projective limit. R is constructed using the proof that the intersection of two rational opens is a rational open, applied to U intersect V. Because U intersect V equals V, R is isomorphic to O_X(V), but a formal proof of this needs a formal proof of Lemma 1.5(i), which we have not yet completed.
We summarise the situation as follows. Two theorems in the informal literature imply that our definition of perfectoid space is the same as the definition in the informal literature. However we have not yet formalised the proofs of these theorems in Lean.
For those more familiar with Wedhorn's "Adic Spaces" notes (never published, but extremely helpful), the two results we have not formalised are Theorem 7.35(2) and Proposition 8.2(1). To give some idea of what is involved here, 8.2(1) relies on 7.18, whose proof involves setting up some of the theory of primary and secondary specialisations of valuations, and Theorem 7.35(2) relies on the theory of the sets Spv(A,I) and the subgroup c\Gamma_v of the value group. All of this is possible in Lean, it simply takes time.
Theorem: to give a term of type
perfectoid space Xis to give a perfectoid space (in the sense used in the mathematical literature).Proof: Looking at the definition of perfectoid space in our repository, and comparing it with the definition in the literature, one sees that there are two instances where we do not follow the definition in the literature, but instead do something equivalent. Here is the justification that what we do is equivalent.
1) Theorem: if A is a Huber pair, then the topology on Spa(A) generated by the basic open sets is the same as the topology on Spa(A) generated by the rational open sets.
Traditionally in the literature the topology on Spa(A) is defined to be the one generated by basic open sets, but in our repository we used the one generated by rational open sets. A reference in the informal literature for the fact that these topologies coincide is Theorem 3.5(ii) of "Continuous Valuations", by R. Huber (Math Z 212, 455--477, 1993).
Once this theorem is formalised in Lean, we can change our definition of the topology to be the one generated by the basic opens and thus conform more closely to the literature.
2) The presheaf on Spa(A) on a general open set U as defined in the literature (a projective limit over all rational open subsets) is isomorphic to the presheaf on Spa(A) as defined in our repository.
A reference for the definition of the presheaf on Spa(A) in the informal literature is the definition just after the end of the proof of Lemma 1.5 in "A generalization of formal schemes and rigid analytic varieties", by R. Huber (Math Z 217, 513--551, 1994). The reason we do not use this definition is that we have not yet formalised the proof of Lemma 1.5(i) of Loc Cit, a geometric universal property of rational open subsets. As a consequence we cannot define all of the morphisms between rings involved in Huber's projective limit. Instead we use a trick. If U and V are rational subsets of Spa(A) and V is a subset of U, then we can define restriction maps from O_X(U) and O_X(V) to an auxiliary ring R, and use these two maps instead of the map O_X(U)->O_X(V) in our projective limit. R is constructed using the proof that the intersection of two rational opens is a rational open, applied to U intersect V. Because U intersect V equals V, R is isomorphic to O_X(V), but a formal proof of this needs a formal proof of Lemma 1.5(i), which we have not yet completed.
We summarise the situation as follows. Two theorems in the informal literature imply that our definition of perfectoid space is the same as the definition in the informal literature. However we have not yet formalised the proofs of these theorems in Lean.
For those more familiar with Wedhorn's "Adic Spaces" notes (never published, but extremely helpful), the two results we have not formalised are Theorem 7.35(2) and Proposition 8.2(1). To give some idea of what is involved here, 8.2(1) relies on 7.18, whose proof involves setting up some of the theory of primary and secondary specialisations of valuations, and Theorem 7.35(2) relies on the theory of the sets Spv(A,I) and the subgroup c\Gamma_v of the value group. All of this is possible in Lean, it simply takes time.