feat(topology/category/Compactum): Compact Hausdorff spaces (#4555)

This PR provides the equivalence between the category of compact Hausdorff topological spaces and the category of algebras for the ultrafilter monad.

## Notation
1. `Compactum` is the category of algebras for the ultrafilter monad. It's a wrapper around `monad.algebra (of_type_functor $ ultrafilter)`.
2. `CompHaus` is the full subcategory of `Top` consisting of topological spaces which are compact and Hausdorff.

Author: adamtopaz

src/data/set/constructions.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2020 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Topaz
+-/
+
+import tactic
+import data.finset.basic
+
+/-!
+# Constructions involving sets of sets.
+
+## Finite Intersections
+
+We define a structure `has_finite_inter` which asserts that a set `S` of subsets of `α` is
+closed under finite intersections.
+
+We define `finite_inter_closure` which, given a set `S` of subsets of `α`, is the smallest
+set of subsets of `α` which is closed under finite intersections.
+
+`finite_inter_closure S` is endowed with a term of type `has_finite_inter` using
+`finite_inter_closure_has_finite_inter`.
+
+-/
+
+variables {α : Type*} (S : set (set α))
+
+/-- A structure encapsulating the fact that a set of sets is closed under finite intersection. -/
+structure has_finite_inter :=
+(univ_mem : set.univ ∈ S)
+(inter_mem {s t} : s ∈ S → t ∈ S → s ∩ t ∈ S)
+
+namespace has_finite_inter
+
+-- Satisfying the inhabited linter...
+instance : inhabited (has_finite_inter ({set.univ} : set (set α))) :=
+⟨⟨by tauto, λ _ _ h1 h2, by finish⟩⟩
+
+/-- The smallest set of sets containing `S` which is closed under finite intersections. -/
+inductive finite_inter_closure : set (set α)
+| basic {s} : s ∈ S → finite_inter_closure s
+| univ : finite_inter_closure set.univ
+| inter {s t} : finite_inter_closure s → finite_inter_closure t → finite_inter_closure (s ∩ t)
+
+/-- Defines `has_finite_inter` for `finite_inter_closure S`. -/
+def finite_inter_closure_has_finite_inter : has_finite_inter (finite_inter_closure S) :=
+{ univ_mem := finite_inter_closure.univ,
+  inter_mem := λ _ _, finite_inter_closure.inter }
+
+variable {S}
+lemma finite_inter_mem (cond : has_finite_inter S) (F : finset (set α)) :
+  ↑F ⊆ S → ⋂₀ (↑F : set (set α)) ∈ S :=
+begin
+  classical,
+  refine finset.induction_on F (λ _, _) _,
+  { simp [cond.univ_mem] },
+  { intros a s h1 h2 h3,
+    suffices : a ∩ ⋂₀ ↑s ∈ S, by simpa,
+    exact cond.inter_mem (h3 (finset.mem_insert_self a s))
+                         (h2 $ λ x hx, h3 $ finset.mem_insert_of_mem hx) }
+end
+
+lemma finite_inter_closure_insert {A : set α} (cond : has_finite_inter S)
+  (P ∈ finite_inter_closure (insert A S)) : P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q :=
+begin
+  induction H with S h T1 T2 _ _ h1 h2,
+  { cases h,
+    { exact or.inr ⟨set.univ, cond.univ_mem, by simpa⟩ },
+    { exact or.inl h } },
+  { exact or.inl cond.univ_mem },
+  { rcases h1 with (h | ⟨Q, hQ, rfl⟩); rcases h2 with (i | ⟨R, hR, rfl⟩),
+    { exact or.inl (cond.inter_mem h i) },
+    { exact or.inr ⟨T1 ∩ R, cond.inter_mem h hR, by finish⟩ },
+    { exact or.inr ⟨Q ∩ T2, cond.inter_mem hQ i, by finish⟩ },
+    { exact or.inr ⟨Q ∩ R, cond.inter_mem hQ hR , by tidy⟩ } }
+end
+
+end has_finite_inter

src/order/filter/ultrafilter.lean

@@ -59,6 +59,26 @@ lemma ultrafilter_iff_compl_mem_iff_not_mem :
         have s ∩ sᶜ ∈ g, from inter_mem_sets hs (g_le this),
         by simp only [empty_in_sets_eq_bot, hg, inter_compl_self] at this; contradiction⟩⟩
 
+/-- A variant of `ultrafilter_iff_compl_mem_iff_not_mem`. -/
+lemma ultrafilter_iff_compl_mem_iff_not_mem' :
+  is_ultrafilter f ↔ (∀ s, s ∈ f ↔ sᶜ ∉ f) :=
+begin
+  rw ultrafilter_iff_compl_mem_iff_not_mem,
+  split,
+  { intros h s, conv_lhs {rw (show s = sᶜᶜ, by simp)}, exact h _, },
+  { intros h s, conv_rhs {rw (show s = sᶜᶜ, by simp)}, exact h _, }
+end
+
+lemma ne_empty_of_mem_ultrafilter (s : set α) : is_ultrafilter f → s ∈ f → s ≠ ∅ :=
+begin
+  rintros h hs rfl,
+  replace h := ((ultrafilter_iff_compl_mem_iff_not_mem'.mp h) ∅).mp hs,
+  finish [f.univ_sets],
+end
+
+lemma nonempty_of_mem_ultrafilter (s : set α) : is_ultrafilter f → s ∈ f → s.nonempty :=
+λ hf hs, ne_empty_iff_nonempty.mp (ne_empty_of_mem_ultrafilter _ hf hs)
+
 lemma mem_or_compl_mem_of_ultrafilter (hf : is_ultrafilter f) (s : set α) :
   s ∈ f ∨ sᶜ ∈ f :=
 or_iff_not_imp_left.2 (ultrafilter_iff_compl_mem_iff_not_mem.mp hf s).mpr

src/topology/basic.lean

@@ -816,6 +816,18 @@ section lim
 /-- If `f` is a filter, then `Lim f` is a limit of the filter, if it exists. -/
 noncomputable def Lim [nonempty α] (f : filter α) : α := epsilon $ λa, f ≤ 𝓝 a
 
+/--
+If `f` is a filter satisfying `ne_bot f`, then `Lim' f` is a limit of the filter, if it exists.
+-/
+def Lim' (f : filter α) [ne_bot f] : α := @Lim _ _ (nonempty_of_ne_bot f) f
+
+-- Note: `ultrafilter` is inside the `filter` namespace.
+/--
+If `F` is an ultrafilter, then `filter.ultrafilter.Lim F` is a limit of the filter, if it exists.
+Note that dot notation `F.Lim` can be used for `F : ultrafilter α`.
+-/
+def filter.ultrafilter.Lim : ultrafilter α → α := λ F, Lim' F.1
+
 /-- If `f` is a filter in `β` and `g : β → α` is a function, then `lim f` is a limit of `g` at `f`,
 if it exists. -/
 noncomputable def lim [nonempty α] (f : filter β) (g : β → α) : α :=

src/topology/category/CompHaus.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2020 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Topaz
+-/
+
+import topology.category.Top
+
+/-!
+
+# The category of Compact Hausdorff Spaces
+
+We construct the category of compact Hausdorff spaces.
+The type of compact Hausdorff spaces is denoted `CompHaus`, and it is endowed with a category
+instance making it a full subcategory of `Top`.
+The fully faithful functor `CompHaus ⥤ Top` is denoted `CompHaus_to_Top`.
+
+**Note:** The file `topology/category/Compactum.lean` provides the equivalence between `Compactum`,
+which is defined as the category of algebras for the ultrafilter monad, and `CompHaus`.
+`Compactum_to_CompHaus` is the functor from `Compactum` to `CompHaus` which is proven to be an
+equivalence of categories in `Compactum_to_CompHaus.is_equivalence`.
+See `topology/category/Compactum.lean` for a more detailed discussion where these definitions are
+introduced.
+
+-/
+
+open category_theory
+
+/-- The type of Compact Hausdorff topological spaces. -/
+structure CompHaus :=
+(to_Top : Top)
+[is_compact : compact_space to_Top]
+[is_hausdorff : t2_space to_Top]
+
+namespace CompHaus
+
+instance : inhabited CompHaus := ⟨{to_Top := { α := pempty }}⟩
+
+instance : has_coe_to_sort CompHaus := ⟨Type*, λ X, X.to_Top⟩
+instance {X : CompHaus} : compact_space X := X.is_compact
+instance {X : CompHaus} : t2_space X := X.is_hausdorff
+
+instance category : category CompHaus := induced_category.category to_Top
+
+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