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.toTop}
(hC : CategoryTheory.Limits.IsLimit C)
(hU : IsClopen 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_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.toTop) (Fin 2))
:
∃ (j : J) (g : LocallyConstant (↑(F.obj j).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.toTop) α)
:
∃ (j : J) (g : LocallyConstant (↑(F.obj j).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.toTop) α)
:
∃ (j : J) (g : LocallyConstant (↑(F.obj j).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.toTop) α)
:
∃ (j : J) (g : LocallyConstant (↑(F.obj j).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.