Source: ProCGroups.InverseSystems.CountableModels
1import Mathlib.Topology.Category.LightProfinite.Basic
2import ProCGroups.InverseSystems.ProfiniteSpace
4/-!
5# Countable inverse-system models of profinite spaces
7A second-countable profinite space is represented as an inverse limit of a sequence of finite
8discrete spaces. Conversely, the module characterizes second countability by the existence of
9a finite-discrete inverse-system presentation over a countable linear order.
10-/
12open Set
13open scoped Topology
15namespace ProCGroups.InverseSystems
17universe u w
19/-- A second-countable profinite space is a sequential inverse limit of finite discrete spaces. -/
20theorem exists_nat_inverseSystem_of_secondCountable (X : Type w) [TopologicalSpace X]
21 [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X]
22 [SecondCountableTopology X] :
23 ∃ S : InverseSystem.{0, w} (I := ℕ),
24 (∀ n, Finite (S.X n)) ∧ (∀ n, DiscreteTopology (S.X n)) ∧
25 Nonempty (X ≃ₜ S.inverseLimit) := by
26 classical
27 let _ : Countable (DiscreteQuotient X) := by
28 letI : Countable (TopologicalSpace.Clopens X) := by
29 rw [TopologicalSpace.Clopens.countable_iff_secondCountable]
30 infer_instance
31 exact (DiscreteQuotient.finsetClopens_inj X).countable
32 let e : ℕ → DiscreteQuotient X :=
33 Set.enumerateCountable (s := (Set.univ : Set (DiscreteQuotient X))) Set.countable_univ ⊤
34 let q : ℕ → DiscreteQuotient X := fun n =>
35 Nat.rec (motive := fun _ => DiscreteQuotient X) (e 0)
36 (fun n qn => qn ⊓ e (n + 1)) n
37 have hq_succ : ∀ n, q (n + 1) = q n ⊓ e (n + 1) := by
38 intro n
39 simp only [q]
40 have hq_antitone : Antitone q := by
41 refine antitone_nat_of_succ_le ?_
42 intro n
43 rw [hq_succ]
44 exact inf_le_left
45 have hq_le_enum : ∀ n, q n ≤ e n := by
46 intro n
47 induction n with
48 | zero =>
49 simp only [Nat.rec_zero, le_refl, q]
50 | succ n ih =>
51 rw [hq_succ]
52 exact inf_le_right
53 let σ : ℕ → OrderDual (DiscreteQuotient X) := fun n =>
54 (show OrderDual (DiscreteQuotient X) from q n)
55 have hσ : Monotone σ := by
56 intro m n hmn
57 change q n ≤ q m
58 exact hq_antitone hmn
59 have hdirNat : Directed (· ≤ ·) (id : ℕ → ℕ) := by
60 intro a b
61 exact ⟨max a b, le_max_left _ _, le_max_right _ _⟩
62 have hrange : Set.range e = (Set.univ : Set (DiscreteQuotient X)) := by
63 simpa [e] using
64 (Set.range_enumerateCountable_of_mem
65 (s := (Set.univ : Set (DiscreteQuotient X))) Set.countable_univ
66 (default := (⊤ : DiscreteQuotient X)) (by simp only [mem_univ]))
67 have hcofinal : ∀ Q : OrderDual (DiscreteQuotient X), ∃ n : ℕ, Q ≤ σ n := by
68 intro Q
69 have hQ : (show DiscreteQuotient X from Q) ∈ Set.range e := by
70 rw [hrange]
71 simp only [mem_univ]
72 rcases hQ with ⟨n, rfl⟩
73 refine ⟨n, ?_⟩
74 change q n ≤ e n
75 exact hq_le_enum n
76 let S0 : InverseSystem (I := OrderDual (DiscreteQuotient X)) := discreteQuotientSystem X
77 let S : InverseSystem (I := ℕ) := S0.reindex σ hσ
78 refine ⟨S, ?_, ?_, ?_⟩
79 · intro n
80 have hfiniteQ : ∀ A : DiscreteQuotient X, Finite ↥A := by
81 intro A
82 infer_instance
83 change Finite (Quotient (q n).toSetoid)
84 exact hfiniteQ (q n)
85 · intro n
86 have hdiscQ : ∀ A : DiscreteQuotient X, DiscreteTopology ↥A := by
87 intro A
88 infer_instance
89 change
90 @DiscreteTopology (Quotient (q n).toSetoid)
91 (q n).instTopologicalSpaceQuotient
92 exact hdiscQ (q n)
93 · refine ⟨(homeomorph_inverseLimit_discreteQuotientSystem X).trans ?_⟩
94 exact S0.homeomorph_reindex_cofinal σ hσ hdirNat hcofinal
96/--
97A profinite space is second countable exactly when it admits a presentation as an inverse limit
98of finite discrete spaces over a countable linear order.
99-/
100theorem secondCountable_iff_exists_countableLinearOrder_finiteDiscreteInverseSystem
101 {X : Type w} [TopologicalSpace X] [CompactSpace X] [T2Space X]
102 [TotallyDisconnectedSpace X] :
103 SecondCountableTopology X ↔
104 ∃ (J : Type) (_ : LinearOrder J) (_ : Countable J),
105 ∃ S : InverseSystem.{0, w} (I := J),
106 (∀ j, Finite (S.X j)) ∧ (∀ j, DiscreteTopology (S.X j)) ∧
107 Nonempty (X ≃ₜ S.inverseLimit) := by
108 constructor
109 · intro hsecond
110 letI : SecondCountableTopology X := hsecond
111 rcases exists_nat_inverseSystem_of_secondCountable X with ⟨S, hfinite, hdisc, hhomeo⟩
112 exact ⟨ℕ, inferInstance, inferInstance, S, hfinite, hdisc, hhomeo⟩
113 · rintro ⟨J, _hJord, hJcount, S, hfinite, hdisc, ⟨e⟩⟩
114 letI : Countable J := hJcount
115 letI : ∀ j, SecondCountableTopology (S.X j) := fun j => by
116 let _ : Finite (S.X j) := hfinite j
117 let _ : DiscreteTopology (S.X j) := hdisc j
118 infer_instance
119 letI : SecondCountableTopology (∀ j, S.X j) := inferInstance
120 letI : SecondCountableTopology S.inverseLimit := by
121 change SecondCountableTopology {x : ∀ j, S.X j // S.Compatible x}
122 exact TopologicalSpace.Subtype.secondCountableTopology _
123 letI : SecondCountableTopology X := e.secondCountableTopology
124 exact inferInstance
126end ProCGroups.InverseSystems