feat(topology/category/Profinite): Profinite_to_Top creates limits. (#…

…7070)

This PR adds a proof that `Profinite` has limits by showing that the forgetful functor to `Top` creates limits.

src/topology/category/CompHaus.lean

@@ -7,6 +7,7 @@ Authors: Adam Topaz, Bhavik Mehta
 import category_theory.adjunction.reflective
 import topology.category.Top
 import topology.stone_cech
+import category_theory.monad.limits
 
 /-!
 
@@ -26,6 +27,8 @@ introduced.
 
 -/
 
+universe u
+
 open category_theory
 
 /-- The type of Compact Hausdorff topological spaces. -/
@@ -64,7 +67,7 @@ end CompHaus
 
 /-- The fully faithful embedding of `CompHaus` in `Top`. -/
 @[simps {rhs_md := semireducible}, derive [full, faithful]]
-def CompHaus_to_Top : CompHaus ⥤ Top := induced_functor _
+def CompHaus_to_Top : CompHaus.{u} ⥤ Top.{u} := induced_functor _
 
 /--
 (Implementation) The object part of the compactification functor from topological spaces to
@@ -105,8 +108,8 @@ noncomputable def stone_cech_equivalence (X : Top) (Y : CompHaus) :
 The Stone-Cech compactification functor from topological spaces to compact Hausdorff spaces,
 left adjoint to the inclusion functor.
 -/
-noncomputable def Top_to_CompHaus : Top ⥤ CompHaus :=
-adjunction.left_adjoint_of_equiv stone_cech_equivalence (λ _ _ _ _ _, rfl)
+noncomputable def Top_to_CompHaus : Top.{u} ⥤ CompHaus.{u} :=
+adjunction.left_adjoint_of_equiv stone_cech_equivalence.{u u} (λ _ _ _ _ _, rfl)
 
 lemma Top_to_CompHaus_obj (X : Top) : ↥(Top_to_CompHaus.obj X) = stone_cech X :=
 rfl
@@ -116,3 +119,6 @@ The category of compact Hausdorff spaces is reflective in the category of topolo
 -/
 noncomputable instance CompHaus_to_Top.reflective : reflective CompHaus_to_Top :=
 { to_is_right_adjoint := ⟨Top_to_CompHaus, adjunction.adjunction_of_equiv_left _ _⟩ }
+
+noncomputable instance CompHaus_to_Top.creates_limits : creates_limits CompHaus_to_Top :=
+monadic_creates_limits _

src/topology/category/Profinite.lean

@@ -8,6 +8,7 @@ import topology.category.CompHaus
 import topology.connected
 import topology.subset_properties
 import category_theory.adjunction.reflective
+import category_theory.monad.limits
 
 /-!
 # The category of Profinite Types
@@ -28,9 +29,8 @@ 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`.
+1. finite coproducts
+2. Clausen/Scholze topology on the category `Profinite`.
 
 ## Tags
 
@@ -133,4 +133,19 @@ lemma CompHaus.to_Profinite_obj' (X : CompHaus) :
 instance Profinite.to_CompHaus.reflective : reflective Profinite.to_CompHaus :=
 { to_is_right_adjoint := ⟨CompHaus.to_Profinite, Profinite.to_Profinite_adj_to_CompHaus⟩ }
 
+noncomputable
+instance Profinite.to_CompHaus.creates_limits : creates_limits Profinite.to_CompHaus :=
+monadic_creates_limits _
+
+noncomputable
+instance Profinite.to_Top.reflective : reflective (Profinite_to_Top : Profinite ⥤ Top) :=
+reflective.comp Profinite.to_CompHaus CompHaus_to_Top
+
+noncomputable
+instance Profinite.to_Top.creates_limits : creates_limits Profinite_to_Top :=
+monadic_creates_limits _
+
+instance Profinite.has_limits : limits.has_limits Profinite :=
+has_limits_of_has_limits_creates_limits Profinite_to_Top
+
 end Profinite