Cofiltered limits of profinite sets. #

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

Main Results #

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_finite_aux {J : Type u} [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 ( α) :
j g, (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑( j)) g

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