From d416ad697f6a4add211cdce18ae299efb95f40ed Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Thu, 3 Dec 2020 19:30:23 +0000
Subject: [PATCH] feat(topology/category/Profinite): add category of profinite
 top. spaces (#5147)

---
 src/topology/category/CompHaus.lean  | 16 +++---
 src/topology/category/Profinite.lean | 78 ++++++++++++++++++++++++++++
 2 files changed, 84 insertions(+), 10 deletions(-)
 create mode 100644 src/topology/category/Profinite.lean

diff --git a/src/topology/category/CompHaus.lean b/src/topology/category/CompHaus.lean
index 990f1c3ac687d..6d04455128983 100644
--- a/src/topology/category/CompHaus.lean
+++ b/src/topology/category/CompHaus.lean
@@ -42,16 +42,12 @@ instance {X : CompHaus} : t2_space X := X.is_hausdorff
 
 instance category : category CompHaus := induced_category.category to_Top
 
+@[simp]
+lemma coe_to_Top {X : CompHaus} : (X.to_Top : Type*) = X :=
+rfl
+
 end  CompHaus
 
 /-- The fully faithful embedding of `CompHaus` in `Top`. -/
-def CompHaus_to_Top : CompHaus ⥤ Top :=
-{ obj := λ X, { α := X },
-  map := λ _ _ f, f }
-
-namespace CompHaus_to_Top
-
-instance : full CompHaus_to_Top := { preimage := λ _ _ f, f }
-instance : faithful CompHaus_to_Top := {}
-
-end CompHaus_to_Top
+@[simps {rhs_md := semireducible}, derive [full, faithful]]
+def CompHaus_to_Top : CompHaus ⥤ Top := induced_functor _
diff --git a/src/topology/category/Profinite.lean b/src/topology/category/Profinite.lean
new file mode 100644
index 0000000000000..662903f47c7f6
--- /dev/null
+++ b/src/topology/category/Profinite.lean
@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2020 Kevin Buzzard. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Buzzard
+-/
+
+import topology.category.CompHaus
+
+/-!
+# The category of Profinite Types
+
+We construct the category of profinite topological spaces,
+often called profinite sets -- perhaps they could be called
+profinite types in Lean.
+
+The type of profinite topological spaces is called `Profinite`. It has a category
+instance and is a fully faithful subcategory of `Top`. The fully faithful functor
+is called `Profinite_to_Top`.
+
+## Implementation notes
+
+A profinite type is defined to be a topological space which is
+compact, Hausdorff and totally disconnected.
+
+## TODO
+
+0. Link to category of projective limits of finite discrete sets.
+1. existence of products, limits(?), finite coproducts
+2. `Profinite_to_Top` creates limits?
+3. Clausen/Scholze topology on the category `Profinite`.
+
+## Tags
+
+profinite
+
+-/
+
+open category_theory
+
+/-- The type of profinite topological spaces. -/
+structure Profinite :=
+(to_Top : Top)
+[is_compact : compact_space to_Top]
+[is_t2 : t2_space to_Top]
+[is_totally_disconnected : totally_disconnected_space to_Top]
+
+namespace Profinite
+
+instance : inhabited Profinite := ⟨{to_Top := { α := pempty }}⟩
+
+instance : has_coe_to_sort Profinite := ⟨Type*, λ X, X.to_Top⟩
+instance {X : Profinite} : compact_space X := X.is_compact
+instance {X : Profinite} : t2_space X := X.is_t2
+instance {X : Profinite} : totally_disconnected_space X := X.is_totally_disconnected
+
+instance category : category Profinite := induced_category.category to_Top
+
+@[simp]
+lemma coe_to_Top {X : Profinite} : (X.to_Top : Type*) = X :=
+rfl
+
+end Profinite
+
+/-- The fully faithful embedding of `Profinite` in `Top`. -/
+@[simps {rhs_md := semireducible}, derive [full, faithful]]
+def Profinite_to_Top : Profinite ⥤ Top := induced_functor _
+
+/-- The fully faithful embedding of `Profinite` in `Top`. -/
+@[simps] def Profinite_to_CompHaus : Profinite ⥤ CompHaus :=
+{ obj := λ X, { to_Top := X.to_Top },
+  map := λ _ _ f, f }
+
+instance : full Profinite_to_CompHaus := { preimage := λ _ _ f, f }
+instance : faithful Profinite_to_CompHaus := {}
+
+@[simp] lemma Profinite_to_CompHaus_to_Top :
+  Profinite_to_CompHaus ⋙ CompHaus_to_Top = Profinite_to_Top :=
+rfl