Inverse limits of compact spaces are nonempty

An InverseSystem f over a preorder consists of types X i together with transition maps f h : X j → X i for i ≤ j, composing along the order. A compatible family, or section, of the system is an x : ∀ i, X i with f h (x j) = x i for every i ≤ j. The theorems here say that such a family exists as soon as the index is directed and every X i is nonempty and compact Hausdorff, and specialize that to the finite systems for which it is Kőnig's lemma.

The data stay unbundled: a family of transition maps and the two laws of InverseSystem, with no functor and no category instance on the index. That is the shape such a system has when it arises — the finite quotients of a profinite group and the maps between them, or the sets of Sylow subgroups of those quotients — and a compatible family is then exactly a point of the inverse limit, so these are the statements a construction of such a point applies directly. The mathematics is Mathlib's Kőnig lemma for cofiltered systems and is not reproved here.

Main statements

• TauCeti.exists_forall_map_eq_of_compact_t2: an inverse system of nonempty compact Hausdorff spaces over a directed index has a compatible family.
• TauCeti.exists_forall_map_eq_of_finite: the same for a system of nonempty finite types.
• TauCeti.exists_forall_map_eq_of_codirected_of_finite: the finite statement for a DirectedSystem over a codirected index, the form in which a system of finite quotients is usually written.
• TauCeti.exists_forall_map_succ_eq_of_compact_t2, TauCeti.exists_forall_map_succ_eq_of_finite: the sequential forms, where the system is given by its one-step maps β k : S (k + 1) → S k.
• TauCeti.exists_forall_map_succ_eq_and_forall_eq_of_surjective: a compatible family in a tower of T1 spaces lifts along a levelwise surjective map from a tower of compact Hausdorff spaces, to a compatible family upstairs. This is the exactness of sequential inverse limits of compact Hausdorff spaces, in the form used for towers of compact modules.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Proposition 1.1.4.

theorem TauCeti.exists_forall_map_eq_of_compact_t2 {ι : Type u} [Preorder ι] [IsDirectedOrder ι] {X : ι → Type w} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), CompactSpace (X i)] [∀ (i : ι), T2Space (X i)] [∀ (i : ι), Nonempty (X i)] (f : ⦃i j : ι⦄ → i ≤ j → X j → X i) [InverseSystem f] (hf : ∀ ⦃i j : ι⦄ (h : i ≤ j), Continuous (f h)) : ∃ (x : (i : ι) → X i), ∀ ⦃i j : ι⦄ (h : i ≤ j), f h (x j) = x i

Inverse limits of nonempty compact Hausdorff spaces are nonempty. Let X be a family of nonempty compact Hausdorff spaces indexed by a directed preorder, forming an inverse system whose transition maps f h : X j → X i are continuous. Then some family x : ∀ i, X i is compatible with all of them.

theorem TauCeti.exists_forall_map_eq_of_finite {ι : Type u} [Preorder ι] [IsDirectedOrder ι] {X : ι → Type w} [∀ (i : ι), Finite (X i)] [∀ (i : ι), Nonempty (X i)] (f : ⦃i j : ι⦄ → i ≤ j → X j → X i) [InverseSystem f] : ∃ (x : (i : ι) → X i), ∀ ⦃i j : ι⦄ (h : i ≤ j), f h (x j) = x i

Kőnig's lemma for a directed index. An inverse system of nonempty finite types over a directed preorder has a compatible family.

theorem TauCeti.exists_forall_map_eq_of_codirected_of_finite {ι : Type u_1} [Preorder ι] [IsCodirectedOrder ι] {X : ι → Type u_2} [∀ (i : ι), Finite (X i)] [∀ (i : ι), Nonempty (X i)] (f : ⦃i j : ι⦄ → i ≤ j → X i → X j) [DirectedSystem X f] : ∃ (x : (i : ι) → X i), ∀ ⦃i j : ι⦄ (h : i ≤ j), f h (x i) = x j

Kőnig's lemma for a codirected index. A DirectedSystem of nonempty finite types over a codirected preorder has a compatible family. This is exists_forall_map_eq_of_finite read on the order dual, and is the form taken by a system of finite quotients indexed by, say, the open normal subgroups of a profinite group ordered by inclusion: there the maps run along the order and the index is directed downwards.

theorem TauCeti.exists_forall_map_succ_eq_of_compact_t2 {S : ℕ → Type u_1} (β : (k : ℕ) → S (k + 1) → S k) [(k : ℕ) → TopologicalSpace (S k)] [∀ (k : ℕ), CompactSpace (S k)] [∀ (k : ℕ), T2Space (S k)] [∀ (k : ℕ), Nonempty (S k)] (hβ : ∀ (k : ℕ), Continuous (β k)) : ∃ (s : (k : ℕ) → S k), ∀ (k : ℕ), β k (s (k + 1)) = s k

Sequential inverse limits of nonempty compact Hausdorff spaces are nonempty. A sequence of nonempty compact Hausdorff spaces S k with continuous one-step maps β k : S (k + 1) → S k has a compatible family: some s : ∀ k, S k satisfies β k (s (k + 1)) = s k for every k.

theorem TauCeti.exists_forall_map_succ_eq_of_finite {S : ℕ → Type u_1} (β : (k : ℕ) → S (k + 1) → S k) [∀ (k : ℕ), Finite (S k)] [∀ (k : ℕ), Nonempty (S k)] : ∃ (s : (k : ℕ) → S k), ∀ (k : ℕ), β k (s (k + 1)) = s k

Kőnig's lemma, sequential form. A sequence of nonempty finite types S k with one-step maps β k : S (k + 1) → S k has a compatible family: some s : ∀ k, S k satisfies β k (s (k + 1)) = s k for every k.

theorem TauCeti.exists_forall_map_succ_eq_and_forall_eq_of_surjective {A : ℕ → Type u_2} {B : ℕ → Type u_3} [(k : ℕ) → TopologicalSpace (A k)] [∀ (k : ℕ), CompactSpace (A k)] [∀ (k : ℕ), T2Space (A k)] [(k : ℕ) → TopologicalSpace (B k)] [∀ (k : ℕ), T1Space (B k)] (α : (k : ℕ) → A (k + 1) → A k) (β : (k : ℕ) → B (k + 1) → B k) (g : (k : ℕ) → A k → B k) (hα : ∀ (k : ℕ), Continuous (α k)) (hg : ∀ (k : ℕ), Continuous (g k)) (hsq : ∀ (k : ℕ) (a : A (k + 1)), g k (α k a) = β k (g (k + 1) a)) (hgs : ∀ (k : ℕ), Function.Surjective (g k)) (b : (k : ℕ) → B k) (hb : ∀ (k : ℕ), β k (b (k + 1)) = b k) : ∃ (a : (k : ℕ) → A k), (∀ (k : ℕ), α k (a (k + 1)) = a k) ∧ ∀ (k : ℕ), g k (a k) = b k

Compatible families lift along a levelwise surjection of towers. Let α k : A (k + 1) → A k be a tower of compact Hausdorff spaces with continuous maps, β k : B (k + 1) → B k a tower of T1 spaces, and g k : A k → B k continuous surjections commuting with the towers. Then every compatible family b in the tower B is the image of a compatible family a in the tower A. In other words the induced map on sequential inverse limits is surjective. The transition maps α k need not be surjective.