We have already built perfectoid rings, so building perfectoid spaces is the same as building adic spaces, which is hence the main work in this issue.
An adic space is just a pre-adic space plus an extra axiom (the structure presheaf is a sheaf) so the main work is to build a structure in Lean corresponding to a pre-adic space.
For this we first need the objects of the category Wedhorn calls V^pre on p76. These objects do not seem hard to define.
The main work is the assumption that the space is locally affinoid; so we need the notion of an isomorphism in V^pre (which should not be hard; is it less hard than defining general morphisms in that category?), the fact that an open subset of a space in V^pre gets an induced structure of an object in V^pre, and we need that Spa A is in V^pre, so we certainly need the structure presheaf on Spa A (https://github.com/kbuzzard/lean-perfectoid-spaces/issues/25) and we also need Wedhorn 8.6 to "do it properly" but in theory I could imagine circumventing this (and it doesn't look too hard).
We have already built perfectoid rings, so building perfectoid spaces is the same as building adic spaces, which is hence the main work in this issue.
An adic space is just a pre-adic space plus an extra axiom (the structure presheaf is a sheaf) so the main work is to build a structure in Lean corresponding to a pre-adic space.
For this we first need the objects of the category Wedhorn calls V^pre on p76. These objects do not seem hard to define.
The main work is the assumption that the space is locally affinoid; so we need the notion of an isomorphism in V^pre (which should not be hard; is it less hard than defining general morphisms in that category?), the fact that an open subset of a space in V^pre gets an induced structure of an object in V^pre, and we need that
Spa Ais in V^pre, so we certainly need the structure presheaf onSpa A(https://github.com/kbuzzard/lean-perfectoid-spaces/issues/25) and we also need Wedhorn 8.6 to "do it properly" but in theory I could imagine circumventing this (and it doesn't look too hard).