This needs more than I thought. To construct the sections we need an API for complete rings as discussed in https://github.com/kbuzzard/lean-perfectoid-spaces/issues/24 . This is enough to construct the sections. But to define the restriction morphisms we need a bunch of general topological ring theory.
To construct the restriction morphisms we need at least (1) of Proposition 8.2 which needs the more geometric universal property Lemma 8.1, which need the usual universal property of completions and Prop 7.52 (and hence 7.18 whose proof is not in Wedhorn but is in Huber's "continuous valuations" (but doesn't look too bad), and the hard part of 7.49 too, which needs some of 7.44). Everything needs ideals everywhere. But nothing needs modules.
This needs more than I thought. To construct the sections we need an API for complete rings as discussed in https://github.com/kbuzzard/lean-perfectoid-spaces/issues/24 . This is enough to construct the sections. But to define the restriction morphisms we need a bunch of general topological ring theory.
To construct the restriction morphisms we need at least (1) of Proposition 8.2 which needs the more geometric universal property Lemma 8.1, which need the usual universal property of completions and Prop 7.52 (and hence 7.18 whose proof is not in Wedhorn but is in Huber's "continuous valuations" (but doesn't look too bad), and the hard part of 7.49 too, which needs some of 7.44). Everything needs ideals everywhere. But nothing needs modules.