How to read Lean

On this page we explain how to read the file perfectoid_space.lean step by step.

We start the file with some import statements.

-- We import definitions of adic_space, Huber_pair, etc
import Frobenius
import adic_space
import Tate_ring
import power_bounded

These lines import other definitions, theorems, notation, etc… from other files in the library. This import is transitive, so this will automatically import a large part of the library (on algebra, topology, etc, and ultimately basic logic).

The next lines form a so-called module docstring: a piece of documentation describing the file. Such module docstrings can be automatically retrieved by documentation tools.

/-!
# Perfectoid Spaces

by Kevin Buzzard, Johan Commelin, and Patrick Massot

Definitions in this file follow Scholze's paper: Étale cohomology of diamonds,
specifically Definition 3.1 and 3.19

For more information on how to read this file, see
https://leanprover-community.github.io/lean-perfectoid-spaces/how-to-read-lean.html
-/

After these introductory lines, we are almost ready to turn to the subject at hand. But we first need to introduce some notation and terminology.

section
-- notation for the power bounded subring
local postfix `ᵒ` : 66 := power_bounded_subring

We start a section, and then setup notation for the power bounded subring. Because a postfix ᵒ is also useful as notation for other concepts, we choose to make this notation local to this file, instead of global notation for every file that imports this file.

open nat power_bounded_subring topological_space function

This block opens some namespaces. Namespaces exist to avoid naming conflicts. As an example, there are functions nat.add and int.add, that define the addition on natural numbers and integers respectively. Thus we have two functions add, one in the namespace nat, and the other in the namespace int.

By opening a namespace, we don’t have to write down the namespace prefix when referring to a definition or lemma in the namespace. For example, topological_space.opens X is the type of all open subsets of X. But because we open the namespace topological_space, we can simply write opens X later on in the file.

parameter (p : primes)

Once and for all (in this file) we fix a prime number p.

structure perfectoid_ring (R : Type) [Huber_ring R] extends Tate_ring R : Prop :=
(complete  : is_complete_hausdorff R)
(uniform   : is_uniform R)
(ramified  : ∃ ϖ : pseudo_uniformizer R, ϖ^p ∣ p in Rᵒ)
(Frobenius : surjective (Frob Rᵒ∕p))

In this block there are a lot of things going on. This block defines a predicate, because it is of the form structure something : Prop := something. Indeed, Prop is the type of propositions: theorems, lemmas, properties, predicates… The predicate in question is perfectoid_ring, and it is a predicate for Huber rings. (Technically, it defines the predicate for types R endowed with the structure of a Huber ring.) The predicate extends another predicate, namely Tate_ring R, which is defined in one of the files that were imported at the top of this file. In addition to the conditions put forth in the predicate Tate_ring, this predicate imposes four new conditions: * it requires R to be complete and Hausdorff * R should be uniform * it asks for the existence of a pseudo-uniformizer, whose p-th power divides p in the subring Rᵒ * and finally it requires that the p’th power map on the power-bounded subring modulo p is surjective.

Note the (for mathematicians) funny notation in the last two conditions. Because Lean is based on type theory, it uses : in places where a mathematician would usually write ∈. In condition ramified, we ask for the existence of a term ϖ of type pseudo_uniformizer R.

Note also that the notation of the universal and existential quantifier use a , where some mathematicians would write a :. Because the : already has a fundamental meaning, we don’t write ∃ (x : X) : condition_on_x to mean “there exists an x such that condition-on-x” but instead we write ∃ (x : X), condition_on_x.

/-
CLVRS ("complete locally valued ringed space") is a category
whose objects are topological spaces with a sheaf of complete topological rings
and an equivalence class of valuation on each stalk, whose support is the unique
maximal ideal of the stalk; in Wedhorn's notes this category is called 𝒱.
A perfectoid space is an object of CLVRS which is locally isomorphic to Spa(A) with
A a perfectoid ring. Note however that CLVRS is a full subcategory of the category
`PreValuedRingedSpace` of topological spaces equipped with a presheaf of topological
rings and a valuation on each stalk, so the isomorphism can be checked in
PreValuedRingedSpace instead, which is what we do.
-/

This comment explains the symbol CLVRS that is used in the rest of the file. It is a category that is defined in one of the imported files.

/-- Condition for an object of CLVRS to be perfectoid: every point should have an open
neighbourhood isomorphic to Spa(A) for some perfectoid ring A.-/
def is_perfectoid (X : CLVRS) : Prop :=
∀ x : X, ∃ (U : opens X) (A : Huber_pair) [perfectoid_ring A],
(x ∈ U) ∧ (Spa A ≊ U)

We now define a predicate on objects of the category CVLRS. Such an object is perfectoid if every point has an open neighbourhood that is isomorphic to the adic spectrum of a perfectoid ring.

Finally we define the type of perfectoid spaces. It is the type of all objects of CLVRS that satisfy the predicate is_perfectoid.

/-- The category of perfectoid spaces.-/
def PerfectoidSpace := {X : CLVRS // is_perfectoid X}

end