feat(topology/category/*/projective): CompHaus and Profinite have eno…

…ugh projectives (#8613)

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



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

docs/references.bib

@@ -744,6 +744,15 @@ @InProceedings{   mcbride1996
   organization  = {Springer}
 }
 
+@Book{            miraglia2006introduction,
+  title         = {An Introduction to Partially Ordered Structures and Sheaves},
+  author        = {Miraglia, F.},
+  isbn          = {9788876990359},
+  series        = {Contemporary logic},
+  year          = {2006},
+  publisher     = {Polimetrica}
+}
+
 @Book{            MM92,
   title         = {Sheaves in geometry and logic: A first introduction to
                   topos theory},

src/topology/category/CompHaus.lean → src/topology/category/CompHaus/default.lean

@@ -8,6 +8,7 @@ import category_theory.adjunction.reflective
 import topology.category.Top
 import topology.stone_cech
 import category_theory.monad.limits
+import topology.urysohns_lemma
 
 /-!
 
@@ -169,23 +170,27 @@ def limit_cone {J : Type u} [small_category J] (F : J ⥤ CompHaus.{u}) :
 { X :=
   { to_Top := (Top.limit_cone (F ⋙ CompHaus_to_Top)).X,
     is_compact := begin
-      dsimp [Top.limit_cone],
+      show compact_space ↥{u : Π j, (F.obj j) | ∀ {i j : J} (f : i ⟶ j), (F.map f) (u i) = u j},
       rw ← is_compact_iff_compact_space,
       apply is_closed.is_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,
+        ⋂ (i j : J) (f : i ⟶ j), {u | F.map f (u i) = u j},
+      { ext1, simp only [set.mem_Inter, set.mem_set_of_eq], },
       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,
+      apply is_closed_eq,
+      { exact (continuous_map.continuous (F.map f)).comp (continuous_apply i), },
+      { exact continuous_apply j, }
     end,
-    is_hausdorff := by { dsimp [Top.limit_cone], apply_instance } },
+    is_hausdorff :=
+      show t2_space ↥{u : Π j, (F.obj j) | ∀ {i j : J} (f : i ⟶ j), (F.map f) (u i) = u j},
+      from infer_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 } } }
+    naturality' := by { intros _ _ _, ext ⟨x, hx⟩,
+      simp only [comp_apply, functor.const.obj_map, id_apply], exact (hx f).symm, } } }
 
 /-- 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}) :
@@ -194,4 +199,50 @@ def limit_cone_is_limit {J : Type u} [small_category J] (F : J ⥤ CompHaus.{u})
     (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 }
 
+lemma epi_iff_surjective {X Y : CompHaus.{u}} (f : X ⟶ Y) : epi f ↔ function.surjective f :=
+begin
+  split,
+  { contrapose!,
+    rintros ⟨y, hy⟩ hf,
+    let C := set.range f,
+    have hC : is_closed C := (is_compact_range f.continuous).is_closed,
+    let D := {y},
+    have hD : is_closed D := is_closed_singleton,
+    have hCD : disjoint C D,
+    { rw set.disjoint_singleton_right, rintro ⟨y', hy'⟩, exact hy y' hy' },
+    haveI : normal_space ↥(Y.to_Top) := normal_of_compact_t2,
+    obtain ⟨φ, hφ0, hφ1, hφ01⟩ := exists_continuous_zero_one_of_closed hC hD hCD,
+    haveI : compact_space (ulift.{u} $ set.Icc (0:ℝ) 1) := homeomorph.ulift.symm.compact_space,
+    haveI : t2_space (ulift.{u} $ set.Icc (0:ℝ) 1) := homeomorph.ulift.symm.t2_space,
+    let Z := of (ulift.{u} $ set.Icc (0:ℝ) 1),
+    let g : Y ⟶ Z := ⟨λ y', ⟨⟨φ y', hφ01 y'⟩⟩,
+      continuous_ulift_up.comp (continuous_subtype_mk (λ y', hφ01 y') φ.continuous)⟩,
+    let h : Y ⟶ Z := ⟨λ _, ⟨⟨0, set.left_mem_Icc.mpr zero_le_one⟩⟩, continuous_const⟩,
+    have H : h = g,
+    { rw ← cancel_epi f,
+      ext x, dsimp,
+      simp only [comp_apply, continuous_map.coe_mk, subtype.coe_mk, hφ0 (set.mem_range_self x),
+        pi.zero_apply], },
+    apply_fun (λ e, (e y).down) at H,
+    dsimp at H,
+    simp only [subtype.mk_eq_mk, hφ1 (set.mem_singleton y), pi.one_apply] at H,
+    exact zero_ne_one H, },
+  { rw ← category_theory.epi_iff_surjective,
+    apply faithful_reflects_epi (forget CompHaus) },
+end
+
+lemma mono_iff_injective {X Y : CompHaus.{u}} (f : X ⟶ Y) : mono f ↔ function.injective f :=
+begin
+  split,
+  { introsI hf x₁ x₂ h,
+    let g₁ : of punit ⟶ X := ⟨λ _, x₁, continuous_of_discrete_topology⟩,
+    let g₂ : of punit ⟶ X := ⟨λ _, x₂, continuous_of_discrete_topology⟩,
+    have : g₁ ≫ f = g₂ ≫ f, by { ext, exact h },
+    rw cancel_mono at this,
+    apply_fun (λ e, e punit.star) at this,
+    exact this },
+  { rw ← category_theory.mono_iff_injective,
+    apply faithful_reflects_mono (forget CompHaus) }
+end
+
 end CompHaus

src/topology/category/CompHaus/projective.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2021 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import topology.category.CompHaus
+import topology.stone_cech
+import category_theory.preadditive.projective
+
+/-!
+# CompHaus has enough projectives
+
+In this file we show that `CompHaus` has enough projectives.
+
+## Main results
+
+Let `X` be a compact Hausdorff space.
+
+* `CompHaus.projective_ultrafilter`: the space `ultrafilter X` is a projective object
+* `CompHaus.projective_presentation`: the natural map `ultrafilter X → X`
+  is a projective presentation
+
+## Reference
+
+See [miraglia2006introduction] Chapter 21 for a proof that `CompHaus` has enough projectives.
+
+-/
+
+noncomputable theory
+
+open category_theory function
+
+namespace CompHaus
+
+instance projective_ultrafilter (X : Type*) :
+  projective (of $ ultrafilter X) :=
+{ factors := λ Y Z f g hg,
+  begin
+    rw epi_iff_surjective at hg,
+    obtain ⟨g', hg'⟩ := hg.has_right_inverse,
+    let t : X → Y := g' ∘ f ∘ (pure : X → ultrafilter X),
+    let h : ultrafilter X → Y := ultrafilter.extend t,
+    have hh : continuous h := continuous_ultrafilter_extend _,
+    use ⟨h, hh⟩,
+    apply faithful.map_injective (forget CompHaus),
+    simp only [forget_map_eq_coe, continuous_map.coe_mk, coe_comp],
+    convert dense_range_pure.equalizer (g.continuous.comp hh) f.continuous _,
+    rw [comp.assoc, ultrafilter_extend_extends, ← comp.assoc, hg'.comp_eq_id, comp.left_id],
+  end }
+
+/-- For any compact Hausdorff space `X`,
+  the natural map `ultrafilter X → X` is a projective presentation. -/
+def projective_presentation (X : CompHaus) : projective_presentation X :=
+{ P := of $ ultrafilter X,
+  f := ⟨_, continuous_ultrafilter_extend id⟩,
+  projective := CompHaus.projective_ultrafilter X,
+  epi := concrete_category.epi_of_surjective _ $
+    λ x, ⟨(pure x : ultrafilter X), congr_fun (ultrafilter_extend_extends (𝟙 X)) x⟩ }
+
+instance : enough_projectives CompHaus :=
+{ presentation := λ X, ⟨projective_presentation X⟩ }
+
+end CompHaus

src/topology/category/Profinite/default.lean

@@ -7,8 +7,10 @@ Authors: Kevin Buzzard, Calle Sönne
 import topology.category.CompHaus
 import topology.connected
 import topology.subset_properties
+import topology.locally_constant.basic
 import category_theory.adjunction.reflective
 import category_theory.monad.limits
+import category_theory.limits.constructions.epi_mono
 import category_theory.Fintype
 
 /-!
@@ -249,4 +251,47 @@ of topological spaces. -/
   left_inv := λ f, by { ext, refl },
   right_inv := λ f, by { ext, refl } }
 
+lemma epi_iff_surjective {X Y : Profinite.{u}} (f : X ⟶ Y) : epi f ↔ function.surjective f :=
+begin
+  split,
+  { contrapose!,
+    rintros ⟨y, hy⟩ hf,
+    let C := set.range f,
+    have hC : is_closed C := (is_compact_range f.continuous).is_closed,
+    let U := Cᶜ,
+    have hU : is_open U := is_open_compl_iff.mpr hC,
+    have hyU : y ∈ U,
+    { refine set.mem_compl _, rintro ⟨y', hy'⟩, exact hy y' hy' },
+    have hUy : U ∈ nhds y := hU.mem_nhds hyU,
+    obtain ⟨V, hV, hyV, hVU⟩ := is_topological_basis_clopen.mem_nhds_iff.mp hUy,
+    classical,
+    letI : topological_space (ulift.{u} $ fin 2) := ⊥,
+    let Z := of (ulift.{u} $ fin 2),
+    let g : Y ⟶ Z := ⟨(locally_constant.of_clopen hV).map ulift.up, locally_constant.continuous _⟩,
+    let h : Y ⟶ Z := ⟨λ _, ⟨1⟩, continuous_const⟩,
+    have H : h = g,
+    { rw ← cancel_epi f,
+      ext x, dsimp [locally_constant.of_clopen],
+      rw if_neg, { refl },
+      refine mt (λ α, hVU α) _,
+      simp only [set.mem_range_self, not_true, not_false_iff, set.mem_compl_eq], },
+    apply_fun (λ e, (e y).down) at H,
+    dsimp [locally_constant.of_clopen] at H,
+    rw if_pos hyV at H,
+    exact top_ne_bot H },
+  { rw ← category_theory.epi_iff_surjective,
+    apply faithful_reflects_epi (forget Profinite) },
+end
+
+lemma mono_iff_injective {X Y : Profinite.{u}} (f : X ⟶ Y) : mono f ↔ function.injective f :=
+begin
+  split,
+  { intro h,
+    haveI : limits.preserves_limits Profinite_to_CompHaus := infer_instance,
+    haveI : mono (Profinite_to_CompHaus.map f) := infer_instance,
+    rwa ← CompHaus.mono_iff_injective },
+  { rw ← category_theory.mono_iff_injective,
+    apply faithful_reflects_mono (forget Profinite) }
+end
+
 end Profinite

src/topology/category/Profinite/projective.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2021 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import topology.category.Profinite
+import topology.stone_cech
+import category_theory.preadditive.projective
+
+/-!
+# Profinite sets have enough projectives
+
+In this file we show that `Profinite` has enough projectives.
+
+## Main results
+
+Let `X` be a profinite set.
+
+* `Profinite.projective_ultrafilter`: the space `ultrafilter X` is a projective object
+* `Profinite.projective_presentation`: the natural map `ultrafilter X → X`
+  is a projective presentation
+
+-/
+
+noncomputable theory
+
+open category_theory function
+
+namespace Profinite
+
+instance projective_ultrafilter (X : Type*) :
+  projective (of $ ultrafilter X) :=
+{ factors := λ Y Z f g hg,
+  begin
+    rw epi_iff_surjective at hg,
+    obtain ⟨g', hg'⟩ := hg.has_right_inverse,
+    let t : X → Y := g' ∘ f ∘ (pure : X → ultrafilter X),
+    let h : ultrafilter X → Y := ultrafilter.extend t,
+    have hh : continuous h := continuous_ultrafilter_extend _,
+    use ⟨h, hh⟩,
+    apply faithful.map_injective (forget Profinite),
+    simp only [forget_map_eq_coe, continuous_map.coe_mk, coe_comp],
+    refine dense_range_pure.equalizer (g.continuous.comp hh) f.continuous _,
+    rw [comp.assoc, ultrafilter_extend_extends, ← comp.assoc, hg'.comp_eq_id, comp.left_id],
+  end }
+
+/-- For any profinite `X`, the natural map `ultrafilter X → X` is a projective presentation. -/
+def projective_presentation (X : Profinite) : projective_presentation X :=
+{ P := of $ ultrafilter X,
+  f := ⟨_, continuous_ultrafilter_extend id⟩,
+  projective := Profinite.projective_ultrafilter X,
+  epi := concrete_category.epi_of_surjective _ $
+    λ x, ⟨(pure x : ultrafilter X), congr_fun (ultrafilter_extend_extends (𝟙 X)) x⟩ }
+
+instance : enough_projectives Profinite :=
+{ presentation := λ X, ⟨projective_presentation X⟩ }
+
+end Profinite

src/topology/homeomorph.lean

@@ -170,6 +170,22 @@ h.embedding.is_compact_iff_is_compact_image.symm
 lemma compact_preimage {s : set β} (h : α ≃ₜ β) : is_compact (h ⁻¹' s) ↔ is_compact s :=
 by rw ← image_symm; exact h.symm.compact_image
 
+lemma compact_space [compact_space α] (h : α ≃ₜ β) : compact_space β :=
+{ compact_univ := by { rw [← image_univ_of_surjective h.surjective, h.compact_image],
+    apply compact_space.compact_univ } }
+
+lemma t2_space [t2_space α] (h : α ≃ₜ β) : t2_space β :=
+{ t2 :=
+  begin
+    intros x y hxy,
+    obtain ⟨u, v, hu, hv, hxu, hyv, huv⟩ := t2_separation (h.symm.injective.ne hxy),
+    refine ⟨h.symm ⁻¹' u, h.symm ⁻¹' v,
+      h.symm.continuous.is_open_preimage _ hu,
+      h.symm.continuous.is_open_preimage _ hv,
+      hxu, hyv, _⟩,
+    rw [← preimage_inter, huv, preimage_empty],
+  end }
+
 protected lemma dense_embedding (h : α ≃ₜ β) : dense_embedding h :=
 { dense   := h.surjective.dense_range,
   .. h.embedding }

src/topology/stone_cech.lean

@@ -84,6 +84,20 @@ t2_iff_ultrafilter.mpr $ assume x y f fx fy,
   have hy : y = mjoin f, from ultrafilter_converges_iff.mp fy,
   hx.trans hy.symm
 
+instance : totally_disconnected_space (ultrafilter α) :=
+begin
+  rw totally_disconnected_space_iff_connected_component_singleton,
+  intro A,
+  simp only [set.eq_singleton_iff_unique_mem, mem_connected_component, true_and],
+  intros B hB,
+  rw ← ultrafilter.coe_le_coe,
+  intros s hs,
+  rw [connected_component_eq_Inter_clopen, set.mem_Inter] at hB,
+  let Z := { F : ultrafilter α | s ∈ F },
+  have hZ : is_clopen Z := ⟨ultrafilter_is_open_basic s, ultrafilter_is_closed_basic s⟩,
+  exact hB ⟨Z, hZ, hs⟩,
+end
+
 lemma ultrafilter_comap_pure_nhds (b : ultrafilter α) : comap pure (𝓝 b) ≤ b :=
 begin
   rw topological_space.nhds_generate_from,