Cofiltered limits of profinite sets. #
This file contains some theorems about cofiltered limits of profinite sets.
Main Results #
exists_clopen_of_cofilteredshows 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_constantshows 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}
[category_theory.small_category J]
[category_theory.is_cofiltered J]
{F : J ⥤ Profinite}
(C : category_theory.limits.cone F)
(hC : category_theory.limits.is_limit C)
{U : set ↥(C.X)}
(hU : is_clopen U) :
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}
[category_theory.small_category J]
[category_theory.is_cofiltered J]
{F : J ⥤ Profinite}
(C : category_theory.limits.cone F)
(hC : category_theory.limits.is_limit C)
(f : locally_constant ↥(C.X) (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_finite_aux
{J : Type u}
[category_theory.small_category J]
[category_theory.is_cofiltered J]
{F : J ⥤ Profinite}
(C : category_theory.limits.cone F)
(hC : category_theory.limits.is_limit C)
{α : Type u_1}
[finite α]
(f : locally_constant ↥(C.X) α) :
∃ (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_finite_nonempty
{J : Type u}
[category_theory.small_category J]
[category_theory.is_cofiltered J]
{F : J ⥤ Profinite}
(C : category_theory.limits.cone F)
(hC : category_theory.limits.is_limit C)
{α : Type u_1}
[finite α]
[nonempty α]
(f : locally_constant ↥(C.X) α) :
∃ (j : J) (g : locally_constant ↥(F.obj j) α), f = locally_constant.comap ⇑(C.π.app j) g
theorem
Profinite.exists_locally_constant
{J : Type u}
[category_theory.small_category J]
[category_theory.is_cofiltered J]
{F : J ⥤ Profinite}
(C : category_theory.limits.cone F)
(hC : category_theory.limits.is_limit C)
{α : Type u_1}
(f : locally_constant ↥(C.X) α) :
∃ (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.