feat(topology/category/limits): Topological bases in cofiltered limits (

#7820)

This PR proves a theorem which provides a simple characterization of certain topological bases in a cofiltered limit of topological spaces.

Eventually I will specialize this assertion to the case where the topological spaces are profinite, and the `T i` are the topological bases given by clopen sets.

This generalizes a lemma from LTE.



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

src/topology/category/Top/basic.lean

@@ -58,4 +58,24 @@ def trivial : Type u ⥤ Top.{u} :=
 { obj := λ X, ⟨X, ⊤⟩,
   map := λ X Y f, { to_fun := f, continuous_to_fun := continuous_top } }
 
+/-- Any homeomorphisms induces an isomorphism in `Top`. -/
+@[simps] def iso_of_homeo {X Y : Top.{u}} (f : X ≃ₜ Y) : X ≅ Y :=
+{ hom := ⟨f⟩,
+  inv := ⟨f.symm⟩ }
+
+/-- Any isomorphism in `Top` induces a homeomorphism. -/
+@[simps] def homeo_of_iso {X Y : Top.{u}} (f : X ≅ Y) : X ≃ₜ Y :=
+{ to_fun := f.hom,
+  inv_fun := f.inv,
+  left_inv := λ x, by simp,
+  right_inv := λ x, by simp,
+  continuous_to_fun := f.hom.continuous,
+  continuous_inv_fun := f.inv.continuous }
+
+@[simp] lemma of_iso_of_homeo {X Y : Top.{u}} (f : X ≃ₜ Y) : homeo_of_iso (iso_of_homeo f) = f :=
+by { ext, refl }
+
+@[simp] lemma of_homeo_of_iso {X Y : Top.{u}} (f : X ≅ Y) : iso_of_homeo (homeo_of_iso f) = f :=
+by { ext, refl }
+
 end Top

src/topology/category/Top/limits.lean

@@ -42,6 +42,21 @@ def limit_cone (F : J ⥤ Top.{u}) : cone F :=
       continuous_to_fun := show continuous ((λ u : Π j : J, F.obj j, u j) ∘ subtype.val),
         by continuity } } }
 
+/--
+A choice of limit cone for a functor `F : J ⥤ Top` whose topology is defined as an
+infimum of topologies infimum.
+Generally you should just use `limit.cone F`, unless you need the actual definition
+(which is in terms of `types.limit_cone`).
+-/
+def limit_cone_infi (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)⟩,
+  π :=
+  { 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) } }
+
 /--
 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
@@ -51,6 +66,17 @@ def limit_cone_is_limit (F : J ⥤ Top.{u}) : is_limit (limit_cone F) :=
 { 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] } }
 
+/--
+The chosen cone `Top.limit_cone_infi 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_infi_is_limit (F : J ⥤ Top.{u}) : is_limit (limit_cone_infi 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 :
+         _) ) }
+
 instance Top_has_limits : has_limits.{u} Top.{u} :=
 { has_limits_of_shape := λ J 𝒥, by exactI
   { has_limit := λ F, has_limit.mk { cone := limit_cone F, is_limit := limit_cone_is_limit F } } }
@@ -102,6 +128,101 @@ end Top
 
 namespace Top
 
+section cofiltered_limit
+
+variables {J : Type u} [small_category J] [is_cofiltered J] (F : J ⥤ Top.{u})
+  (C : cone F) (hC : is_limit C)
+
+include hC
+
+/--
+Given a *compatible* collection of topological bases for the factors in a cofiltered limit
+which contain `set.univ` and are closed under intersections, the induced *naive* collection
+of sets in the limit is, in fact, a topological basis.
+-/
+theorem is_topological_basis_cofiltered_limit
+  (T : Π j, set (set (F.obj j))) (hT : ∀ j, is_topological_basis (T j))
+  (univ : ∀ (i : J), set.univ ∈ T i)
+  (inter : ∀ i (U1 U2 : set (F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i)
+  (compat : ∀ (i j : J) (f : i ⟶ j) (V : set (F.obj j)) (hV : V ∈ T j), (F.map f) ⁻¹' V ∈ T i) :
+  is_topological_basis { U : set C.X | ∃ j (V : set (F.obj j)), V ∈ T j ∧ U = C.π.app j ⁻¹' V } :=
+begin
+  classical,
+  -- The limit cone for `F` whose topology is defined as an infimum.
+  let D := limit_cone_infi F,
+  -- The isomorphism between the cone point of `C` and the cone point of `D`.
+  let E : C.X ≅ D.X := hC.cone_point_unique_up_to_iso (limit_cone_infi_is_limit _),
+  have hE : inducing E.hom := (Top.homeo_of_iso E).inducing,
+  -- Reduce to the assertion of the theorem with `D` instead of `C`.
+  suffices : is_topological_basis
+    { U : set D.X | ∃ j (V : set (F.obj j)), V ∈ T j ∧ U = D.π.app j ⁻¹' V },
+  { convert this.inducing hE,
+    ext U0,
+    split,
+    { rintro ⟨j, V, hV, rfl⟩,
+      refine ⟨D.π.app j ⁻¹' V, ⟨j, V, hV, rfl⟩, rfl⟩ },
+    { rintro ⟨W, ⟨j, V, hV, rfl⟩, rfl⟩,
+      refine ⟨j, V, hV, rfl⟩ } },
+  -- Using `D`, we can apply the characterization of the topological basis of a
+  -- topology defined as an infimum...
+  convert is_topological_basis_infi hT (λ j (x : D.X), D.π.app j x),
+  ext U0,
+  split,
+  { rintros  ⟨j, V, hV, rfl⟩,
+    let U : Π i, set (F.obj i) := λ i, if h : i = j then (by {rw h, exact V}) else set.univ,
+    refine ⟨U,{j},_,_⟩,
+    { rintro i h,
+      rw finset.mem_singleton at h,
+      dsimp [U],
+      rw dif_pos h,
+      subst h,
+      exact hV },
+    { dsimp [U],
+      simp } },
+  { rintros ⟨U, G, h1, h2⟩,
+    obtain ⟨j, hj⟩ := is_cofiltered.inf_objs_exists G,
+    let g : ∀ e (he : e ∈ G), j ⟶ e := λ _ he, (hj he).some,
+    let Vs : J → set (F.obj j) := λ e, if h : e ∈ G then F.map (g e h) ⁻¹' (U e) else set.univ,
+    let V : set (F.obj j) := ⋂ (e : J) (he : e ∈ G), Vs e,
+    refine ⟨j, V, _, _⟩,
+    { -- An intermediate claim used to apply induction along `G : finset J` later on.
+      have : ∀ (S : set (set (F.obj j))) (E : finset J) (P : J → set (F.obj j))
+        (univ : set.univ ∈ S)
+        (inter : ∀ A B : set (F.obj j), A ∈ S → B ∈ S → A ∩ B ∈ S)
+        (cond : ∀ (e : J) (he : e ∈ E), P e ∈ S), (⋂ e (he : e ∈ E), P e) ∈ S,
+      { intros S E,
+        apply E.induction_on,
+        { intros P he hh,
+          simpa },
+        { intros a E ha hh1 hh2 hh3 hh4 hh5,
+          rw finset.set_bInter_insert,
+          refine hh4 _ _ (hh5 _ (finset.mem_insert_self _ _)) (hh1 _ hh3 hh4 _),
+          intros e he,
+          exact hh5 e (finset.mem_insert_of_mem he) } },
+      -- use the intermediate claim to finish off the goal using `univ` and `inter`.
+      refine this _ _ _ (univ _) (inter _) _,
+      intros e he,
+      dsimp [Vs],
+      rw dif_pos he,
+      exact compat j e (g e he) (U e) (h1 e he), },
+    { -- conclude...
+      rw h2,
+      dsimp [V],
+      rw set.preimage_Inter,
+      congr' 1,
+      ext1 e,
+      rw set.preimage_Inter,
+      congr' 1,
+      ext1 he,
+      dsimp [Vs],
+      rw [dif_pos he, ← set.preimage_comp],
+      congr' 1,
+      change _ = ⇑(D.π.app j ≫ F.map (g e he)),
+      rw D.w } }
+end
+
+end cofiltered_limit
+
 section topological_konig
 
 /-!