Profinite.exists_isClopen_of_cofiltered
theorem Profinite.exists_isClopen_of_cofiltered :
∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsCofiltered J]
{F : CategoryTheory.Functor J ProfiniteMax} (C : CategoryTheory.Limits.Cone F) {U : Set ↑C.pt.toCompHaus.toTop},
CategoryTheory.Limits.IsLimit C → IsClopen U → ∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
The theorem `Profinite.exists_isClopen_of_cofiltered` states that if `X` is a cofiltered limit of profinite sets (these are compact, Hausdorff, and totally disconnected spaces), then for any clopen set `U` in `X`, there exists a clopen set `V` in one of the terms in the limit such that `U` is the preimage of `V` under the function defined by the morphism from the category limit to the term `j`. Here, a clopen set is a set that is both open and closed, while a cofiltered limit is a specific way to construct a limit in a category that ensures that the limit exists under certain conditions.
More concisely: Given a cofiltered limit of profinite sets X and a clopen set U in X, there exists a clopen set V in some term of the limit such that U is the preimage of V under the limit morphism.
|
Profinite.exists_locallyConstant
theorem Profinite.exists_locallyConstant :
∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsCofiltered J]
{F : CategoryTheory.Functor J ProfiniteMax} (C : CategoryTheory.Limits.Cone F) {α : Type u_1},
CategoryTheory.Limits.IsLimit C →
∀ (f : LocallyConstant (↑C.pt.toCompHaus.toTop) α), ∃ j g, f = LocallyConstant.comap (C.π.app j) g
The theorem `Profinite.exists_locallyConstant` states that for any locally constant function from a cofiltered limit of profinite sets, there exists a component through which it factors. More precisely, given any category `J` (which should be small and cofiltered), a functor `F` from `J` to the category of profinite sets (which is represented by the type `ProfiniteMax`), a cone `C` over `F`, and a locally constant function `f` from the underlying topological space of the apex of the cone to another type `α`, provided that `C` is a limit cone, there exists an object `j` in `J` and a locally constant function `g` such that `f` is the pullback of `g` along the morphism from the apex of `C` to `F(j)` given by the cone.
This theorem essentially conveys that locally constant functions from a limit of profinite sets can be described in terms of locally constant functions from the individual sets that make up the limit.
More concisely: Given a cofiltered limit `C` of profinite sets `J` with functor `F`, a locally constant function `f` on the limit's underlying topological space, and a limit cone `C`, there exists an object `j` in `J` and a locally constant function `g` on `F(j)` such that `f` is the pullback of `g` along the cone's morphism to `F(j)`.
|