From ff05193346807153c34891c789e8807045765e32 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 27 Aug 2022 17:30:32 +0100 Subject: [PATCH] comment profinite example --- src/examples/profinite.lean | 75 +++++++++++++++++++++++++++++-------- 1 file changed, 60 insertions(+), 15 deletions(-) diff --git a/src/examples/profinite.lean b/src/examples/profinite.lean index 8e5e891c..5c571f61 100644 --- a/src/examples/profinite.lean +++ b/src/examples/profinite.lean @@ -1,23 +1,37 @@ -import challenge +import challenge -- imports the entire proof of the Liquid Tensor Experiment. /-! +# Profinite sets + This file explains the structure of profinite sets. +Lean uses type theory, so strictly speaking we are setting up the theory +of profinite types. But for mathematics of this nature, sets and types +are to all intents and purposes the same thing, and it makes no difference +to the underlying mathematics. + -/ -open category_theory opposite -open_locale liquid_tensor_experiment +open category_theory opposite -- so we can write `grothendieck_topology` instead +-- of `category_theory.grothendieck_topology` and `op` instead of `opposite.op` +open_locale liquid_tensor_experiment -- This introduces a coercion from +-- functors to functions, used once below. +attribute [instance] functor_coe_to_fun /- -`Profinite.{0}` denotes the type of profinite sets whose underlying type -lives in `Type = Type 0`. +Set-theoretically one can think of `Profinite.{0}` as the collection of profinite sets. +Type-theoretically it's the class of profinite spaces whose underlying type +lives in `Type = Type 0`. The type of `Profinite.{0}` is `Type 1`, which is the type-theoretic +version of the set-theoretic concept of an object being a class (so possibly too big to be a set). -/ -example : Type 1 := Profinite.{0} -example (X : Profinite.{0}) : Type := X - +example : Type 1 := Profinite.{0} -- Set-theoretic translation: `Profinite.{0}` is a collection of + -- objects, possibly too big to be a set. +example (X : Profinite.{0}) : Type := X -- Set-theoretic translation: The objects of `Profinite.{0}` + -- can be thought of as sets. /- Any profinite set is a compact, Hausdorff, totally disconnected topological space. +It's the job of Lean's type class inference system to prove these facts automatically. -/ example (X : Profinite.{0}) : topological_space X := infer_instance example (X : Profinite.{0}) : compact_space X := infer_instance @@ -34,16 +48,21 @@ example (X : Type) [t2_space X] [totally_disconnected_space X] : Profinite.{0} := -Profinite.of X +Profinite.of X -- `Profinite.of` is the function which makes the object in the category from the + -- topological space. Lean is pedantic about the difference. /- -The morphisms in the category of profinite sets are just continuous maps. +`C(X,Y)` is the type of continuous maps from `X` to `Y`. The longer +arrow `X ⟶ Y` denotes the type of morphisms from `X` to `Y` in the category `Profinite.{0}`. +The next example shows that, by definition, the morphisms in the category +are the continuous maps. -/ example (X Y : Profinite.{0}) : (X ⟶ Y : Type) = C(X,Y) := rfl /- -The `proetale_topology` is the Grothendieck topology on `Profinite.{0}` which is used in -condensed mathematics. +The term `proetale_topology` is the name of a Grothendieck topology on `Profinite.{0}` +which is used in condensed mathematics. In the next example we'll see that the definition +of this topology is what you would expect. -/ example : grothendieck_topology Profinite.{0} := proetale_topology @@ -51,7 +70,7 @@ example : grothendieck_topology Profinite.{0} := proetale_topology This example shows that the sheaf condition with respect to this Grothendieck topology, for a presheaf of abelian groups on `Profinite.{0}`, is equivalent to the usual definition. -/ -example (F : Profinite.{0}ᵒᵖ ⥤ Ab.{1}) : +example (F : Profinite.{0}ᵒᵖ ⥤ Ab.{1}) : -- Let `F` be a presheaf of ab groups on `Profinite.{0}` presheaf.is_sheaf proetale_topology F -- `F` is a sheaf for `proetale_topology` if and only if... ↔ ∀ (α : Fintype.{0}) -- For any finite indexing type `α`, @@ -67,18 +86,44 @@ example (F : Profinite.{0}ᵒᵖ ⥤ Ab.{1}) : ∀ i, F.map (π i).op s = x i -- which restricts to `x i` over `X i` for all `i`. := begin + -- it suffices to check the underlying sheaf of types is a presheaf rw presheaf.is_sheaf_iff_is_sheaf_forget proetale_topology F (forget _), + -- this is equivalent to the data above in a slightly re-arranged form rw [is_sheaf_iff_is_sheaf_of_type, (F ⋙ forget Ab).is_proetale_sheaf_of_types_tfae.out 0 2], + -- now prove each direction by slightly rearranging the data split, { intros H α, exact H _ }, { introsI H α _, exact H ⟨α⟩ } end -/- The objects of `Condensed.{0} Ab.{1}` are indeed just sheaves in `proetale_topology`. -/ +/-! + +## Condensed abelian groups. + +To give a condensed abelian group in Lean is to give a pair of pieces of data: firstly +a presheaf of abelian groups on the category of profinite sets, and secondly a proof +that this presheaf is a sheaf for the proetale topology. + +We write "$F$ is a condensed abelian group" as `F : Condensed.{0} Ab.{1}` in Lean. +-/ + +/- The objects of `Condensed.{0} Ab.{1}` are indeed just sheaves in `proetale_topology`. +The two components of a condensed abelian group `F`, the presheaf and the proof, +are called `F.1` and `F.2`. + -/ example (F : Condensed.{0} Ab.{1}) : Profinite.{0}ᵒᵖ ⥤ Ab.{1} := F.1 example (F : Condensed.{0} Ab.{1}) : presheaf.is_sheaf proetale_topology F.1 := F.2 +/- +Conversely, given a presheaf `F` and a proof `hF` that it's a sheaf for the proetale +topology, we can make a condensed abelian group using the `⟨F, hF⟩` syntax. +-/ example (F : Profinite.{0}ᵒᵖ ⥤ Ab.{1}) (hF : presheaf.is_sheaf proetale_topology F) : - Condensed.{0} Ab.{1} := ⟨F,hF⟩ + Condensed.{0} Ab.{1} := ⟨F, hF⟩ +/- +This is a proof that the objects in the category of condensed abelian groups +are by definition sheaves of abelian groups for the topology `proetale_topology` +on the category of profinite types (or sets). +-/ example : Condensed.{0} Ab.{1} = Sheaf proetale_topology.{0} Ab.{1} := rfl