ProCGroups/InverseSystems/CountableModels.lean
1import Mathlib.Topology.Category.LightProfinite.Basic
2import ProCGroups.InverseSystems.ProfiniteSpace
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/InverseSystems/CountableModels.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Inverse systems and inverse limits
15Defines inverse systems of topological groups and proves lift, projection, exactness, quotient, stagewise isomorphism, and finite-stage factorization results.
16-/
18open Set
19open scoped Topology
21namespace ProCGroups.InverseSystems
23universe u w
25/-- A second-countable profinite space is a sequential inverse limit of finite discrete spaces. -/
26theorem exists_nat_inverseSystem_of_secondCountable (X : Type w) [TopologicalSpace X]
27 [SecondCountableTopology X] (hX : IsProfiniteSpace X) :
28 ∃ S : InverseSystem.{0, w} (I := ℕ),
29 (∀ n, Finite (S.X n)) ∧ (∀ n, DiscreteTopology (S.X n)) ∧
30 Nonempty (X ≃ₜ S.inverseLimit) := by
31 classical
32 rcases compact_t2_totallyDisconnected_of_isProfiniteSpace X hX with
33 ⟨hcompact, hT2, htotdisc⟩
34 let _ : CompactSpace X := hcompact
35 let _ : T2Space X := hT2
36 let _ : TotallyDisconnectedSpace X := htotdisc
37 let LX : LightProfinite := LightProfinite.of X
38 let _ : Countable (DiscreteQuotient X) := by
39 simpa [LX] using (LightProfinite.instCountableDiscreteQuotient LX)
40 let e : ℕ → DiscreteQuotient X :=
41 Set.enumerateCountable (s := (Set.univ : Set (DiscreteQuotient X))) Set.countable_univ ⊤
42 let q : ℕ → DiscreteQuotient X := fun n =>
43 Nat.rec (motive := fun _ => DiscreteQuotient X) (e 0)
44 (fun n qn => qn ⊓ e (n + 1)) n
45 have hq_succ : ∀ n, q (n + 1) = q n ⊓ e (n + 1) := by
46 intro n
47 simp only [Nat.succ_eq_add_one, q]
48 have hq_antitone : Antitone q := by
49 refine antitone_nat_of_succ_le ?_
50 intro n
51 rw [hq_succ]
52 exact inf_le_left
53 have hq_le_enum : ∀ n, q n ≤ e n := by
54 intro n
55 induction n with
57 simp only [Nat.succ_eq_add_one, Nat.rec_zero, le_refl, q]
58 | succ n ih =>
59 rw [hq_succ]
60 exact inf_le_right
61 let σ : ℕ → OrderDual (DiscreteQuotient X) := fun n =>
62 (show OrderDual (DiscreteQuotient X) from q n)
63 have hσ : Monotone σ := by
64 intro m n hmn
65 change q n ≤ q m
66 exact hq_antitone hmn
67 have hdirNat : Directed (· ≤ ·) (id : ℕ → ℕ) := by
68 intro a b
69 exact ⟨max a b, le_max_left _ _, le_max_right _ _⟩
70 have hrange : Set.range e = (Set.univ : Set (DiscreteQuotient X)) := by
71 simpa [e] using
72 (Set.range_enumerateCountable_of_mem
73 (s := (Set.univ : Set (DiscreteQuotient X))) Set.countable_univ
74 (default := (⊤ : DiscreteQuotient X)) (by simp only [mem_univ]))
75 have hcofinal : ∀ Q : OrderDual (DiscreteQuotient X), ∃ n : ℕ, Q ≤ σ n := by
76 intro Q
77 have hQ : (show DiscreteQuotient X from Q) ∈ Set.range e := by
78 rw [hrange]
79 simp only [mem_univ]
80 rcases hQ with ⟨n, rfl⟩
81 refine ⟨n, ?_⟩
82 change q n ≤ e n
83 exact hq_le_enum n
84 let S0 : InverseSystem (I := OrderDual (DiscreteQuotient X)) := discreteQuotientSystem X
85 let S : InverseSystem (I := ℕ) := S0.reindex σ hσ
86 refine ⟨S, ?_, ?_, ?_⟩
87 · intro n
88 have hfiniteQ : ∀ A : DiscreteQuotient X, Finite ↥A := by
89 intro A
90 infer_instance
91 simpa using hfiniteQ (q n)
92 · intro n
93 have hdiscQ : ∀ A : DiscreteQuotient X, DiscreteTopology ↥A := by
94 intro A
95 infer_instance
96 simpa using hdiscQ (q n)
97 · refine ⟨(homeomorph_inverseLimit_discreteQuotientSystem X).trans ?_⟩
98 exact S0.homeomorph_reindex_cofinal σ hσ hdirNat hcofinal
100/-- A profinite space is second countable exactly when it admits a presentation as an inverse
103 {X : Type w} [TopologicalSpace X] (hX : IsProfiniteSpace X) :
104 SecondCountableTopology X ↔
105 ∃ (J : Type) (_ : LinearOrder J) (_ : Countable J),
106 ∃ S : InverseSystem.{0, w} (I := J),
107 (∀ j, Finite (S.X j)) ∧ (∀ j, DiscreteTopology (S.X j)) ∧
108 Nonempty (X ≃ₜ S.inverseLimit) := by
109 constructor
110 · intro hsecond
111 letI : SecondCountableTopology X := hsecond
112 rcases exists_nat_inverseSystem_of_secondCountable X hX with ⟨S, hfinite, hdisc, hhomeo⟩
113 exact ⟨ℕ, inferInstance, inferInstance, S, hfinite, hdisc, hhomeo⟩
114 · rintro ⟨J, _hJord, hJcount, S, hfinite, hdisc, ⟨e⟩⟩
115 letI : Countable J := hJcount
116 letI : ∀ j, SecondCountableTopology (S.X j) := fun j => by
117 let _ : Finite (S.X j) := hfinite j
118 let _ : DiscreteTopology (S.X j) := hdisc j
119 infer_instance
120 letI : SecondCountableTopology (∀ j, S.X j) := inferInstance
121 letI : SecondCountableTopology S.inverseLimit := by
122 change SecondCountableTopology {x : ∀ j, S.X j // S.Compatible x}
123 exact TopologicalSpace.Subtype.secondCountableTopology _
124 letI : SecondCountableTopology X := e.secondCountableTopology
125 exact inferInstance
127end ProCGroups.InverseSystems