feat(topology/category/*): Add alternative explicit limit cones for Top, etc. and shows X : Profinite is a limit of finite sets. (#7448)

This PR redefines `Top.limit_cone`, and defines similar explicit limit cones for `CompHaus` and `Profinite`.
Using the definition with the subspace topology makes the proofs that the limit is compact, t2 and/or totally disconnected much easier.

This also expresses any `X : Profinite` as a limit of its discrete quotients, which are all finite.



Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>

Author: adamtopaz

src/topology/category/CompHaus.lean

@@ -159,3 +159,39 @@ has_limits_of_has_limits_creates_limits CompHaus_to_Top
 
 instance CompHaus.has_colimits : limits.has_colimits CompHaus :=
 has_colimits_of_reflective CompHaus_to_Top
+
+namespace CompHaus
+
+/-- An explicit limit cone for a functor `F : J ⥤ CompHaus`, defined in terms of
+`Top.limit_cone`. -/
+def limit_cone {J : Type u} [small_category J] (F : J ⥤ CompHaus.{u}) :
+  limits.cone F :=
+{ X :=
+  { to_Top := (Top.limit_cone (F ⋙ CompHaus_to_Top)).X,
+    is_compact := begin
+      dsimp [Top.limit_cone],
+      rw ← compact_iff_compact_space,
+      apply is_closed.compact,
+      have : {u : Π j, F.obj j | ∀ {i j : J} (f : i ⟶ j), F.map f (u i) = u j} =
+        ⋂ (i j : J) (f : i ⟶ j), {u | F.map f (u i) = u j}, by tidy,
+      rw this,
+      apply is_closed_Inter, intros i,
+      apply is_closed_Inter, intros j,
+      apply is_closed_Inter, intros f,
+      apply is_closed_eq;
+      continuity,
+    end,
+    is_hausdorff := by { dsimp [Top.limit_cone], apply_instance } },
+  π :=
+  { app := λ j, (Top.limit_cone (F ⋙ CompHaus_to_Top)).π.app j,
+    -- tidy needs a little help in the `naturality'` field to avoid deterministic timeouts.
+    naturality' := by { intros _ _ _, ext, tidy } } }
+
+/-- The limit cone `CompHaus.limit_cone F` is indeed a limit cone. -/
+def limit_cone_is_limit {J : Type u} [small_category J] (F : J ⥤ CompHaus.{u}) :
+  limits.is_limit (limit_cone F) :=
+{ lift := λ S,
+    (Top.limit_cone_is_limit (F ⋙ CompHaus_to_Top)).lift (CompHaus_to_Top.map_cone S),
+  uniq' := λ S m h, (Top.limit_cone_is_limit _).uniq (CompHaus_to_Top.map_cone S) _ h }
+
+end CompHaus

src/topology/category/Profinite/as_limit.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2021 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Calle Sönne, Adam Topaz
+-/
+import topology.category.Profinite
+import topology.discrete_quotient
+
+/-!
+# Profinite sets as limits of finite sets.
+
+We show that any profinite set is isomorphic to the limit of its
+discrete (hence finite) quotients.
+
+## Definitions
+
+There are a handful of definitions in this file, given `X : Profinite`:
+1. `X.fintype_diagram` is the functor `discret_quotient X ⥤ Fintype` whose limit
+  is isomorphic to `X` (the limit taking place in `Profinite` via `Fintype_to_Profinite`, see 2).
+2. `X.diagram` is an abbreviation for `X.fintype_diagram ⋙ Fintype_to_Profinite`.
+3. `X.as_limit_cone` is the cone over `X.diagram` whose cone point is `X`.
+4. `X.iso_as_limit_cone_lift` is the isomorphism `X ≅ (Profinite.limit_cone X.diagram).X` induced
+  by lifting `X.as_limit_cone`.
+5. `X.as_limit_cone_iso` is the isomorphism `X.as_limit_cone ≅ (Profinite.limit_cone X.diagram)`
+  induced by `X.iso_as_limit_cone_lift`.
+6. `X.as_limit` is a term of type `is_limit X.as_limit_cone`.
+7. `X.lim : category_theory.limits.limit_cone X.as_limit_cone` is a bundled combination of 3 and 6.
+
+-/
+
+noncomputable theory
+
+open category_theory
+
+namespace Profinite
+
+universe u
+
+variables (X : Profinite.{u})
+
+/-- The functor `discrete_quotient X ⥤ Fintype` whose limit is isomorphic to `X`. -/
+def fintype_diagram : discrete_quotient X ⥤ Fintype :=
+{ obj := λ S, Fintype.of S,
+  map := λ S T f, discrete_quotient.of_le $ le_of_hom f }
+
+/-- An abbreviation for `X.fintype_diagram ⋙ Fintype_to_Profinite`. -/
+abbreviation diagram : discrete_quotient X ⥤ Profinite :=
+X.fintype_diagram ⋙ Fintype.to_Profinite
+
+/-- A cone over `X.diagram` whose cone point is `X`. -/
+def as_limit_cone : category_theory.limits.cone X.diagram :=
+{ X := X,
+  π := { app := λ S, ⟨S.proj, S.proj_is_locally_constant.continuous⟩ } }
+
+instance is_iso_as_limit_cone_lift :
+  is_iso ((limit_cone_is_limit X.diagram).lift X.as_limit_cone) :=
+is_iso_of_bijective _
+begin
+  refine ⟨λ a b, _, λ a, _⟩,
+  { intro h,
+    refine discrete_quotient.eq_of_proj_eq (λ S, _),
+    apply_fun (λ f : (limit_cone X.diagram).X, f.val S) at h,
+    exact h },
+  { obtain ⟨b, hb⟩ := discrete_quotient.exists_of_compat
+      (λ S, a.val S) (λ _ _ h, a.prop (hom_of_le h)),
+    refine ⟨b, _⟩,
+    ext S : 3,
+    apply hb },
+end
+
+/--
+The isomorphism between `X` and the explicit limit of `X.diagram`,
+induced by lifting `X.as_limit_cone`.
+-/
+def iso_as_limit_cone_lift : X ≅ (limit_cone X.diagram).X :=
+as_iso $ (limit_cone_is_limit _).lift X.as_limit_cone
+
+/--
+The isomorphism of cones `X.as_limit_cone` and `Profinite.limit_cone X.diagram`.
+The underlying isomorphism is defeq to `X.iso_as_limit_cone_lift`.
+-/
+def as_limit_cone_iso : X.as_limit_cone ≅ limit_cone _ :=
+limits.cones.ext (iso_as_limit_cone_lift _) (λ _, rfl)
+
+/-- `X.as_limit_cone` is indeed a limit cone. -/
+def as_limit : category_theory.limits.is_limit X.as_limit_cone :=
+limits.is_limit.of_iso_limit (limit_cone_is_limit _) X.as_limit_cone_iso.symm
+
+/-- A bundled version of `X.as_limit_cone` and `X.as_limit`. -/
+def lim : limits.limit_cone X.diagram := ⟨X.as_limit_cone, X.as_limit⟩
+
+end Profinite

src/topology/category/Profinite.lean renamed to src/topology/category/Profinite/default.lean

@@ -137,7 +137,7 @@ adjunction.left_adjoint_of_equiv Profinite.to_CompHaus_equivalence (λ _ _ _ _ _
 lemma CompHaus.to_Profinite_obj' (X : CompHaus) :
   ↥(CompHaus.to_Profinite.obj X) = connected_components X.to_Top.α := rfl
 
- /-- Finite types are given the discrete topology. -/
+/-- Finite types are given the discrete topology. -/
 def Fintype.discrete_topology (A : Fintype) : topological_space A := ⊥
 
 section discrete_topology
@@ -159,6 +159,31 @@ end Profinite
 
 namespace Profinite
 
+universe u
+
+/--
+An explicit limit cone for a functor `F : J ⥤ Profinite`, defined in terms of
+`Top.limit_cone`.
+-/
+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 } }
+
+/-- 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),
+  uniq' := λ S m h,
+    (CompHaus.limit_cone_is_limit _).uniq (Profinite.to_CompHaus.map_cone S) _ h }
+
 /--
 The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus
 -/

src/topology/category/Top/limits.lean

@@ -35,24 +35,21 @@ Generally you should just use `limit.cone F`, unless you need the actual definit
 (which is in terms of `types.limit_cone`).
 -/
 def limit_cone (F : J ⥤ Top.{u}) : cone F :=
-{ X := ⟨(types.limit_cone (F ⋙ forget)).X, ⨅j,
-        (F.obj j).str.induced ((types.limit_cone (F ⋙ forget)).π.app j)⟩,
+{ X := Top.of {u : Π j : J, F.obj j | ∀ {i j : J} (f : i ⟶ j), F.map f (u i) = u j},
   π :=
-  { app := λ j, ⟨(types.limit_cone (F ⋙ forget)).π.app j,
-                 continuous_iff_le_induced.mpr (infi_le _ _)⟩,
-    naturality' := λ j j' f,
-                   continuous_map.coe_inj ((types.limit_cone (F ⋙ forget)).π.naturality f) } }
+  { app := λ j,
+    { to_fun := λ u, u.val j,
+      continuous_to_fun := show continuous ((λ u : Π j : J, F.obj j, u j) ∘ subtype.val),
+        by continuity } } }
 
 /--
 The chosen cone `Top.limit_cone F` for a functor `F : J ⥤ Top` is a limit cone.
 Generally you should just use `limit.is_limit F`, unless you need the actual definition
 (which is in terms of `types.limit_cone_is_limit`).
 -/
 def limit_cone_is_limit (F : J ⥤ Top.{u}) : is_limit (limit_cone F) :=
-by { refine is_limit.of_faithful forget (types.limit_cone_is_limit _) (λ s, ⟨_, _⟩) (λ s, rfl),
-     exact continuous_iff_coinduced_le.mpr (le_infi $ λ j,
-       coinduced_le_iff_le_induced.mp $ (continuous_iff_coinduced_le.mp (s.π.app j).continuous :
-         _) ) }
+{ lift := λ S, { to_fun := λ x, ⟨λ j, S.π.app _ x, λ i j f, by { dsimp, erw ← S.w f, refl }⟩ },
+  uniq' := λ S m h, by { ext : 3, simpa [← h] } }
 
 instance Top_has_limits : has_limits.{u} Top.{u} :=
 { has_limits_of_shape := λ J 𝒥, by exactI