Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(topology/category/Profinite): add category of profinite top. spa…
…ces (#5147)
- Loading branch information
Showing
2 changed files
with
84 additions
and
10 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |