Cofiltered limits of profinite sets.

This file contains some theorems about cofiltered limits of profinite sets.

Main Results

• exists_isClopen_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.

theorem Profinite.exists_isClopen_of_cofiltered {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {U : Set ↑C.pt.toCompHaus.toTop} (hC : CategoryTheory.Limits.IsLimit C) (hU : IsClopen U) : ∃ (j : J) (V : Set ↑(F.obj j).toCompHaus.toTop), IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V

If X is a cofiltered limit of profinite sets, then any clopen subset of X arises from a clopen set in one of the terms in the limit.

theorem Profinite.exists_locallyConstant_fin_two {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)) : ∃ (j : J) (g : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Fin 2)), f = LocallyConstant.comap (C.π.app j) g

theorem Profinite.exists_locallyConstant_finite_aux {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {α : Type u_1} [Finite α] (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toCompHaus.toTop) α) : ∃ (j : J) (g : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)), LocallyConstant.map (fun (a b : α) => if a = b then 0 else 1) f = LocallyConstant.comap (C.π.app j) g

theorem Profinite.exists_locallyConstant_finite_nonempty {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {α : Type u_1} [Finite α] [Nonempty α] (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toCompHaus.toTop) α) : ∃ (j : J) (g : LocallyConstant (↑(F.obj j).toCompHaus.toTop) α), f = LocallyConstant.comap (C.π.app j) g

theorem Profinite.exists_locallyConstant {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {α : Type u_1} (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toCompHaus.toTop) α) : ∃ (j : J) (g : LocallyConstant (↑(F.obj j).toCompHaus.toTop) α), f = LocallyConstant.comap (C.π.app j) g

Any locally constant function from a cofiltered limit of profinite sets factors through one of the components.