# mathlibdocumentation

topology.category.Profinite.cofiltered_limit

# Cofiltered limits of profinite sets. #

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

## Main Results #

• 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.
theorem Profinite.exists_clopen_of_cofiltered {J : Type u} {F : J Profinite} {U : set (C.X)} (hU : is_clopen U) :
∃ (j : J) (V : set (F.obj j)) (hV : , 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_locally_constant_fin_two {J : Type u} {F : J Profinite} (f : (fin 2)) :
∃ (j : J) (g : locally_constant (F.obj j) (fin 2)), f = locally_constant.comap (C.π.app j) g
theorem Profinite.exists_locally_constant_fintype_aux {J : Type u} {F : J Profinite} {α : Type u_1} [fintype α] (f : α) :
∃ (j : J) (g : locally_constant (F.obj j) (α → fin 2)), locally_constant.map (λ (a b : α), ite (a = b) 0 1) f = locally_constant.comap (C.π.app j) g
theorem Profinite.exists_locally_constant_fintype_nonempty {J : Type u} {F : J Profinite} {α : Type u_1} [fintype α] [nonempty α] (f : α) :
∃ (j : J) (g : locally_constant (F.obj j) α), f = locally_constant.comap (C.π.app j) g
theorem Profinite.exists_locally_constant {J : Type u} {F : J Profinite} {α : Type u_1} (f : α) :
∃ (j : J) (g : locally_constant (F.obj j) α), f = locally_constant.comap (C.π.app j) g

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