From e42af8dae8959e89ed4c53b7b97be816d9460b19 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Thu, 15 Jul 2021 05:43:19 +0000 Subject: [PATCH] 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. --- .../category/Profinite/cofiltered_limit.lean | 16 ++-- src/topology/category/Profinite/default.lean | 92 +++++++++---------- 2 files changed, 53 insertions(+), 55 deletions(-) diff --git a/src/topology/category/Profinite/cofiltered_limit.lean b/src/topology/category/Profinite/cofiltered_limit.lean index 0f25b99f732ca..fa3df9c0f5b93 100644 --- a/src/topology/category/Profinite/cofiltered_limit.lean +++ b/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 diff --git a/src/topology/category/Profinite/default.lean b/src/topology/category/Profinite/default.lean index dffbcfcaa7973..a4b584a78e1f6 100644 --- a/src/topology/category/Profinite/default.lean +++ b/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,9 +104,10 @@ 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 } /-- @@ -117,7 +115,7 @@ def CompHaus.to_Profinite_obj (X : CompHaus.{u}) : Profinite.{u} := 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. -/