feat(topology/Profinite/cofiltered_limit): Locally constant functions from cofiltered limits (#7992)

This generalizes one of the main technical theorems from LTE about cofiltered limits of profinite sets.
This theorem should be useful for a future proof of Stone duality.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Author: adamtopaz

src/topology/category/Profinite/cofiltered_limit.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz
 -/
 import topology.category.Profinite
+import topology.locally_constant.basic
+import topology.discrete_quotient
 
 /-!
 # Cofiltered limits of profinite sets.
@@ -14,6 +16,8 @@ This file contains some theorems about cofiltered limits of profinite sets.
 
 - `exists_clopen_of_cofiltered` shows that any clopen set in a cofiltered limit of profinite
   sets is the pullback of a clopen set from one of the factors in the limit.
+- `exists_locally_constant` shows that any locally constant function from a cofiltered limit
+  of profinite sets factors through one of the components.
 -/
 
 
@@ -110,4 +114,129 @@ begin
       rwa [dif_pos hs, ← set.preimage_comp, ← Profinite.coe_comp, C.w] at hx } }
 end
 
+lemma exists_locally_constant_fin_two (f : locally_constant C.X (fin 2)) :
+  ∃ (j : J) (g : locally_constant (F.obj j) (fin 2)), f = g.comap (C.π.app _) :=
+begin
+  let U := f ⁻¹' {0},
+  have hU : is_clopen U := f.is_locally_constant.is_clopen_fiber _,
+  obtain ⟨j,V,hV,h⟩ := exists_clopen_of_cofiltered C hC hU,
+  use [j, locally_constant.of_clopen hV],
+  apply locally_constant.locally_constant_eq_of_fiber_zero_eq,
+  rw locally_constant.coe_comap _ _ (C.π.app j).continuous,
+  conv_rhs { rw set.preimage_comp },
+  rw [locally_constant.of_clopen_fiber_zero hV, ← h],
+end
+
+theorem exists_locally_constant_fintype_aux {α : Type*} [fintype α] (f : locally_constant C.X α) :
+  ∃ (j : J) (g : locally_constant (F.obj j) (α → fin 2)),
+    f.map (λ a b, if a = b then (0 : fin 2) else 1) = g.comap (C.π.app _) :=
+begin
+  let ι : α → α → fin 2 := λ x y, if x = y then 0 else 1,
+  let ff := (f.map ι).flip,
+  have hff := λ (a : α), exists_locally_constant_fin_two _ hC (ff a),
+  choose j g h using hff,
+  let G : finset J := finset.univ.image j,
+  obtain ⟨j0,hj0⟩ := is_cofiltered.inf_objs_exists G,
+  have hj : ∀ a, j a ∈ G,
+  { intros a,
+    simp [G] },
+  let fs : Π (a : α), j0 ⟶ j a := λ a, (hj0 (hj a)).some,
+  let gg : α → locally_constant (F.obj j0) (fin 2) := λ a, (g a).comap (F.map (fs _)),
+  let ggg := locally_constant.unflip gg,
+  refine ⟨j0, ggg, _⟩,
+  have : f.map ι = locally_constant.unflip (f.map ι).flip, by simp,
+  rw this, clear this,
+  have : locally_constant.comap (C.π.app j0) ggg =
+    locally_constant.unflip (locally_constant.comap (C.π.app j0) ggg).flip, by simp,
+  rw this, clear this,
+  congr' 1,
+  ext1 a,
+  change ff a = _,
+  rw h,
+  dsimp [ggg, gg],
+  ext1,
+  repeat {
+    rw locally_constant.coe_comap,
+    dsimp [locally_constant.flip, locally_constant.unflip] },
+  { congr' 1,
+    change _ = ((C.π.app j0) ≫ (F.map (fs a))) x,
+    rw C.w },
+  all_goals { continuity },
+end
+
+theorem exists_locally_constant_fintype_nonempty {α : Type*} [fintype α] [nonempty α]
+  (f : locally_constant C.X α) :
+  ∃ (j : J) (g : locally_constant (F.obj j) α), f = g.comap (C.π.app _) :=
+begin
+  inhabit α,
+  obtain ⟨j,gg,h⟩ := exists_locally_constant_fintype_aux _ hC f,
+  let ι : α → α → fin 2 := λ a b, if a = b then 0 else 1,
+  let σ : (α → fin 2) → α := λ f, if h : ∃ (a : α), ι a = f then h.some else arbitrary _,
+  refine ⟨j, gg.map σ, _⟩,
+  ext,
+  rw locally_constant.coe_comap _ _ (C.π.app j).continuous,
+  dsimp [σ],
+  have h1 : ι (f x) = gg (C.π.app j x),
+  { change f.map (λ a b, if a = b then (0 : fin 2) else 1) x = _,
+    rw [h, locally_constant.coe_comap _ _ (C.π.app j).continuous] },
+  have h2 : ∃ a : α, ι a = gg (C.π.app j x) := ⟨f x, h1⟩,
+  rw dif_pos h2,
+  apply_fun ι,
+  { rw h2.some_spec,
+    exact h1 },
+  { intros a b hh,
+    apply_fun (λ e, e a) at hh,
+    dsimp [ι] at hh,
+    rw if_pos rfl at hh,
+    split_ifs at hh with hh1 hh1,
+    { exact hh1.symm },
+    { exact false.elim (bot_ne_top hh) } }
+end
+
+/-- Any locally constant function from a cofiltered limit of profinite sets factors through
+one of the components. -/
+theorem exists_locally_constant {α : Type*} (f : locally_constant C.X α) :
+  ∃ (j : J) (g : locally_constant (F.obj j) α), f = g.comap (C.π.app _) :=
+begin
+  let S := f.discrete_quotient,
+  let ff : S → α := f.lift,
+  by_cases hα : nonempty S,
+  { resetI,
+    let f' : locally_constant C.X S := ⟨S.proj, S.proj_is_locally_constant⟩,
+    obtain ⟨j,g',h⟩ := exists_locally_constant_fintype_nonempty _ hC f',
+    use j,
+    refine ⟨⟨ff ∘ g', g'.is_locally_constant.comp _⟩,_⟩,
+    ext1 t,
+    apply_fun (λ e, e t) at h,
+    rw locally_constant.coe_comap _ _ (C.π.app j).continuous at h ⊢,
+    dsimp at h ⊢,
+    rw ← h,
+    refl },
+  { suffices : ∃ j : J, ¬ nonempty (F.obj j),
+    { obtain ⟨j,hj⟩ := this,
+      use j,
+      refine ⟨⟨λ x, false.elim (hj ⟨x⟩), λ A, _⟩, _⟩,
+      { convert is_open_empty,
+        rw set.eq_empty_iff_forall_not_mem,
+        intros x,
+        exact false.elim (hj ⟨x⟩) },
+      { ext x,
+        exact false.elim (hj ⟨C.π.app j x⟩) } },
+    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,
+      (infer_instance : t2_space (F.obj 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),
+    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,
+    have CD := (hD.cone_point_unique_up_to_iso (Top.limit_cone_is_limit _)).inv,
+    exact cond.map CD }
+end
+
 end Profinite

src/topology/discrete_quotient.lean

@@ -326,3 +326,30 @@ begin
 end
 
 end discrete_quotient
+
+namespace locally_constant
+
+variables {X} {α : Type*} (f : locally_constant X α)
+
+/-- Any locally constant function induces a discrete quotient. -/
+def discrete_quotient : discrete_quotient X :=
+{ rel := λ a b, f b = f a,
+  equiv := ⟨by tauto, by tauto, λ a b c h1 h2, by rw [h2, h1]⟩,
+  clopen := λ x, f.is_locally_constant.is_clopen_fiber _ }
+
+/-- The function from the discrete quotient associated to a locally constant function. -/
+def lift : f.discrete_quotient → α := λ a, quotient.lift_on' a f (λ a b h, h.symm)
+
+lemma lift_is_locally_constant : _root_.is_locally_constant f.lift := λ A, trivial
+
+/-- A locally constant version of `locally_constant.lift`. -/
+def locally_constant_lift : locally_constant f.discrete_quotient α :=
+⟨f.lift, f.lift_is_locally_constant⟩
+
+@[simp]
+lemma lift_eq_coe : f.lift = f.locally_constant_lift := rfl
+
+@[simp]
+lemma factors : f.locally_constant_lift ∘ f.discrete_quotient.proj = f := by { ext, refl }
+
+end locally_constant

src/topology/locally_constant/basic.lean

@@ -64,6 +64,14 @@ lemma is_open_fiber {f : X → Y} (hf : is_locally_constant f) (y : Y) :
   is_open {x | f x = y} :=
 hf {y}
 
+lemma is_closed_fiber {f : X → Y} (hf : is_locally_constant f) (y : Y) :
+  is_closed {x | f x = y} :=
+⟨hf {y}ᶜ⟩
+
+lemma is_clopen_fiber {f : X → Y} (hf : is_locally_constant f) (y : Y) :
+  is_clopen {x | f x = y} :=
+⟨is_open_fiber hf _, is_closed_fiber hf _⟩
+
 lemma iff_exists_open (f : X → Y) :
   is_locally_constant f ↔ ∀ x, ∃ (U : set X) (hU : is_open U) (hx : x ∈ U), ∀ x' ∈ U, f x' = f x :=
 (is_locally_constant.tfae f).out 0 4
@@ -161,7 +169,7 @@ lemma div [has_div Y] ⦃f g : X → Y⦄ (hf : is_locally_constant f) (hg : is_
   is_locally_constant (f / g) :=
 hf.comp₂ hg (/)
 
-/-- If a composition of a function `f` followed by an injection `g` is locally 
+/-- If a composition of a function `f` followed by an injection `g` is locally
 constant, then the locally constant property descends to `f`. -/
 lemma desc {α β : Type*} (f : X → α) (g : α → β)
   (h : is_locally_constant (g ∘ f)) (inj : function.injective g) : is_locally_constant f :=