# Documentation

Mathlib.Topology.Category.Profinite.CofilteredLimit

# 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 : } (C : ) {U : Set C.pt.toCompHaus.toTop} (hC : ) (hU : ) :
j V x, 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 u} {F : } (C : ) (hC : ) (f : LocallyConstant (C.pt.toCompHaus.toTop) (Fin 2)) :
j g, f = LocallyConstant.comap (↑(C.app j)) g
theorem Profinite.exists_locallyConstant_finite_aux {J : Type u} {F : } (C : ) {α : Type u_1} [] (hC : ) (f : LocallyConstant (C.pt.toCompHaus.toTop) α) :
j g, 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 u} {F : } (C : ) {α : Type u_1} [] [] (hC : ) (f : LocallyConstant (C.pt.toCompHaus.toTop) α) :
j g, f = LocallyConstant.comap (↑(C.app j)) g
theorem Profinite.exists_locallyConstant {J : Type u} {F : } (C : ) {α : Type u_1} (hC : ) (f : LocallyConstant (C.pt.toCompHaus.toTop) α) :
j g, f = LocallyConstant.comap (↑(C.app j)) g

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