refactor(topology/category/Profinite): define Profinite as a subcategory of CompHaus (#8314)

This adjusts the definition of Profinite to explicitly be a subcategory of CompHaus rather than a subcategory of Top which embeds into CompHaus. Essentially this means it's easier to construct an element of Profinite from an element of CompHaus.

Author: b-mehta

src/topology/category/Profinite/cofiltered_limit.lean

@@ -43,8 +43,8 @@ begin
   -- First, we have the topological basis of the cofiltered limit obtained by pulling back
   -- clopen sets from the factors in the limit. By continuity, all such sets are again clopen.
   have hB := Top.is_topological_basis_cofiltered_limit
-    (F ⋙ Profinite_to_Top)
-    (Profinite_to_Top.map_cone C)
+    (F ⋙ Profinite.to_Top)
+    (Profinite.to_Top.map_cone C)
     (is_limit_of_preserves _ hC)
     (λ j, {W | is_clopen W})
     _ (λ i, is_clopen_univ) (λ i U1 U2 hU1 hU2, hU1.inter hU2) _,
@@ -225,16 +225,16 @@ begin
     rw ← not_forall,
     intros h,
     apply hα,
-    haveI : ∀ j : J, nonempty ((F ⋙ Profinite_to_Top).obj j) := h,
-    haveI : ∀ j : J, t2_space ((F ⋙ Profinite_to_Top).obj j) := λ j,
+    haveI : ∀ j : J, nonempty ((F ⋙ Profinite.to_Top).obj j) := h,
+    haveI : ∀ j : J, t2_space ((F ⋙ Profinite.to_Top).obj j) := λ j,
       (infer_instance : t2_space (F.obj j)),
-    haveI : ∀ j : J, compact_space ((F ⋙ Profinite_to_Top).obj j) := λ j,
+    haveI : ∀ j : J, compact_space ((F ⋙ Profinite.to_Top).obj j) := λ j,
       (infer_instance : compact_space (F.obj j)),
     have cond := Top.nonempty_limit_cone_of_compact_t2_cofiltered_system
-      (F ⋙ Profinite_to_Top),
+      (F ⋙ Profinite.to_Top),
     suffices : nonempty C.X, by exact nonempty.map S.proj this,
-    let D := Profinite_to_Top.map_cone C,
-    have hD : is_limit D := is_limit_of_preserves Profinite_to_Top hC,
+    let D := Profinite.to_Top.map_cone C,
+    have hD : is_limit D := is_limit_of_preserves Profinite.to_Top hC,
     have CD := (hD.cone_point_unique_up_to_iso (Top.limit_cone_is_limit _)).inv,
     exact cond.map CD }
 end

src/topology/category/Profinite/default.lean

@@ -45,10 +45,8 @@ 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]
+(to_CompHaus : CompHaus)
+[is_totally_disconnected : totally_disconnected_space to_CompHaus]
 
 namespace Profinite
 
@@ -57,21 +55,23 @@ Construct a term of `Profinite` from a type endowed with the structure of a
 compact, Hausdorff and totally disconnected topological space.
 -/
 def of (X : Type*) [topological_space X] [compact_space X] [t2_space X]
-  [totally_disconnected_space X] : Profinite := ⟨⟨X⟩⟩
+  [totally_disconnected_space X] : Profinite := ⟨⟨⟨X⟩⟩⟩
 
 instance : inhabited Profinite := ⟨Profinite.of pempty⟩
 
-instance category : category Profinite := induced_category.category to_Top
+instance category : category Profinite := induced_category.category to_CompHaus
 instance concrete_category : concrete_category Profinite := induced_category.concrete_category _
 instance has_forget₂ : has_forget₂ Profinite Top := induced_category.has_forget₂ _
 
-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 : has_coe_to_sort Profinite := ⟨Type*, λ X, X.to_CompHaus⟩
 instance {X : Profinite} : totally_disconnected_space X := X.is_totally_disconnected
 
+-- We check that we automatically infer that Profinite sets are compact and Hausdorff.
+example {X : Profinite} : compact_space X := infer_instance
+example {X : Profinite} : t2_space X := infer_instance
+
 @[simp]
-lemma coe_to_Top {X : Profinite} : (X.to_Top : Type*) = X :=
+lemma coe_to_CompHaus {X : Profinite} : (X.to_CompHaus : Type*) = X :=
 rfl
 
 @[simp] lemma coe_id (X : Profinite) : (𝟙 X : X → X) = id := rfl
@@ -80,20 +80,17 @@ rfl
 
 end Profinite
 
-/-- The fully faithful embedding of `Profinite` in `Top`. -/
-@[simps, derive [full, faithful]]
-def Profinite_to_Top : Profinite ⥤ Top := forget₂ _ _
-
 /-- The fully faithful embedding of `Profinite` in `CompHaus`. -/
-@[simps] def Profinite.to_CompHaus : Profinite ⥤ CompHaus :=
-{ obj := λ X, { to_Top := X.to_Top },
-  map := λ _ _ f, f }
+@[simps, derive [full, faithful]]
+def Profinite_to_CompHaus : Profinite ⥤ CompHaus := induced_functor _
 
-instance : full Profinite.to_CompHaus := { preimage := λ _ _ f, f }
-instance : faithful Profinite.to_CompHaus := {}
+/-- The fully faithful embedding of `Profinite` in `Top`. This is definitionally the same as the
+obvious composite. -/
+@[simps, derive [full, faithful]]
+def Profinite.to_Top : Profinite ⥤ Top := forget₂ _ _
 
 @[simp] lemma Profinite.to_CompHaus_to_Top :
-  Profinite.to_CompHaus ⋙ CompHaus_to_Top = Profinite_to_Top :=
+  Profinite_to_CompHaus ⋙ CompHaus_to_Top = Profinite.to_Top :=
 rfl
 
 section Profinite
@@ -107,17 +104,18 @@ See: https://stacks.math.columbia.edu/tag/0900
 -- Without explicit universe annotations here, Lean introduces two universe variables and
 -- unhelpfully defines a function `CompHaus.{max u₁ u₂} → Profinite.{max u₁ u₂}`.
 def CompHaus.to_Profinite_obj (X : CompHaus.{u}) : Profinite.{u} :=
-{ to_Top := { α := connected_components X.to_Top.α },
-  is_compact := quotient.compact_space,
-  is_t2 := connected_components.t2,
+{ to_CompHaus :=
+  { to_Top := Top.of (connected_components X),
+    is_compact := quotient.compact_space,
+    is_hausdorff := connected_components.t2 },
   is_totally_disconnected := connected_components.totally_disconnected_space }
 
 /--
 (Implementation) The bijection of homsets to establish the reflective adjunction of Profinite
 spaces in compact Hausdorff spaces.
 -/
 def Profinite.to_CompHaus_equivalence (X : CompHaus.{u}) (Y : Profinite.{u}) :
-  (CompHaus.to_Profinite_obj X ⟶ Y) ≃ (X ⟶ Profinite.to_CompHaus.obj Y) :=
+  (CompHaus.to_Profinite_obj X ⟶ Y) ≃ (X ⟶ Profinite_to_CompHaus.obj Y) :=
 { to_fun := λ f,
   { to_fun := f.1 ∘ quotient.mk,
     continuous_to_fun := continuous.comp f.2 (continuous_quotient_mk) },
@@ -135,7 +133,7 @@ def CompHaus.to_Profinite : CompHaus ⥤ Profinite :=
 adjunction.left_adjoint_of_equiv Profinite.to_CompHaus_equivalence (λ _ _ _ _ _, rfl)
 
 lemma CompHaus.to_Profinite_obj' (X : CompHaus) :
-  ↥(CompHaus.to_Profinite.obj X) = connected_components X.to_Top.α := rfl
+  ↥(CompHaus.to_Profinite.obj X) = connected_components X := rfl
 
 /-- Finite types are given the discrete topology. -/
 def Fintype.discrete_topology (A : Fintype) : topological_space A := ⊥
@@ -161,63 +159,63 @@ namespace Profinite
 def limit_cone {J : Type u} [small_category J] (F : J ⥤ Profinite.{u}) :
   limits.cone F :=
 { X :=
-  { to_Top := CompHaus_to_Top.obj (CompHaus.limit_cone (F ⋙ Profinite.to_CompHaus)).X,
-    is_compact := by { dsimp [CompHaus_to_Top], apply_instance },
-    is_t2 := by { dsimp [CompHaus_to_Top], apply_instance },
-    is_totally_disconnected := by {
-      dsimp [CompHaus_to_Top, CompHaus.limit_cone, Profinite.to_CompHaus, Top.limit_cone],
-      apply_instance } },
-  π := { app := λ j, (CompHaus.limit_cone (F ⋙ Profinite.to_CompHaus)).π.app j } }
+  { to_CompHaus := (CompHaus.limit_cone (F ⋙ Profinite_to_CompHaus)).X,
+    is_totally_disconnected :=
+    begin
+      change totally_disconnected_space ↥{u : Π (j : J), (F.obj j) | _},
+      exact subtype.totally_disconnected_space,
+    end },
+  π := { app := (CompHaus.limit_cone (F ⋙ Profinite_to_CompHaus)).π.app } }
 
 /-- The limit cone `Profinite.limit_cone F` is indeed a limit cone. -/
 def limit_cone_is_limit {J : Type u} [small_category J] (F : J ⥤ Profinite.{u}) :
   limits.is_limit (limit_cone F) :=
-{ lift := λ S, (CompHaus.limit_cone_is_limit (F ⋙ Profinite.to_CompHaus)).lift
-    (Profinite.to_CompHaus.map_cone S),
+{ lift := λ S, (CompHaus.limit_cone_is_limit (F ⋙ Profinite_to_CompHaus)).lift
+    (Profinite_to_CompHaus.map_cone S),
   uniq' := λ S m h,
-    (CompHaus.limit_cone_is_limit _).uniq (Profinite.to_CompHaus.map_cone S) _ h }
+    (CompHaus.limit_cone_is_limit _).uniq (Profinite_to_CompHaus.map_cone S) _ h }
 
 /-- The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus -/
-def to_Profinite_adj_to_CompHaus : CompHaus.to_Profinite ⊣ Profinite.to_CompHaus :=
+def to_Profinite_adj_to_CompHaus : CompHaus.to_Profinite ⊣ Profinite_to_CompHaus :=
 adjunction.adjunction_of_equiv_left _ _
 
 /-- The category of profinite sets is reflective in the category of compact hausdroff spaces -/
-instance to_CompHaus.reflective : reflective Profinite.to_CompHaus :=
+instance to_CompHaus.reflective : reflective Profinite_to_CompHaus :=
 { to_is_right_adjoint := ⟨CompHaus.to_Profinite, Profinite.to_Profinite_adj_to_CompHaus⟩ }
 
 noncomputable
-instance to_CompHaus.creates_limits : creates_limits Profinite.to_CompHaus :=
+instance to_CompHaus.creates_limits : creates_limits Profinite_to_CompHaus :=
 monadic_creates_limits _
 
 noncomputable
-instance to_Top.reflective : reflective (Profinite_to_Top : Profinite ⥤ Top) :=
-reflective.comp Profinite.to_CompHaus CompHaus_to_Top
+instance to_Top.reflective : reflective Profinite.to_Top :=
+reflective.comp Profinite_to_CompHaus CompHaus_to_Top
 
 noncomputable
-instance to_Top.creates_limits : creates_limits Profinite_to_Top :=
+instance to_Top.creates_limits : creates_limits Profinite.to_Top :=
 monadic_creates_limits _
 
 instance has_limits : limits.has_limits Profinite :=
-has_limits_of_has_limits_creates_limits Profinite_to_Top
+has_limits_of_has_limits_creates_limits Profinite.to_Top
 
 instance has_colimits : limits.has_colimits Profinite :=
-has_colimits_of_reflective to_CompHaus
+has_colimits_of_reflective Profinite_to_CompHaus
 
 noncomputable
 instance forget_preserves_limits : limits.preserves_limits (forget Profinite) :=
-by apply limits.comp_preserves_limits Profinite_to_Top (forget _)
+by apply limits.comp_preserves_limits Profinite.to_Top (forget Top)
 
 variables {X Y : Profinite.{u}} (f : X ⟶ Y)
 
 /-- Any morphism of profinite spaces is a closed map. -/
 lemma is_closed_map : is_closed_map f :=
-show is_closed_map (Profinite.to_CompHaus.map f), from CompHaus.is_closed_map _
+CompHaus.is_closed_map _
 
 /-- Any continuous bijection of profinite spaces induces an isomorphism. -/
 lemma is_iso_of_bijective (bij : function.bijective f) : is_iso f :=
 begin
-  haveI := CompHaus.is_iso_of_bijective (Profinite.to_CompHaus.map f) bij,
-  exact is_iso_of_fully_faithful Profinite.to_CompHaus _
+  haveI := CompHaus.is_iso_of_bijective (Profinite_to_CompHaus.map f) bij,
+  exact is_iso_of_fully_faithful Profinite_to_CompHaus _
 end
 
 /-- Any continuous bijection of profinite spaces induces an isomorphism. -/