Yamaguchi Lean 4 Library
ProCGroups/FreeProC/Spaces.lean
ProCGroups/FreeProC/Spaces/Source

ProCGroups/FreeProC/Spaces.lean

1import ProCGroups.FreeProC.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/FreeProC/Spaces.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free pro-C groups
14Develops free pro-C groups on spaces and pointed spaces, their universal properties, finite quotient characterizations, and standard comparison isomorphisms.
15-/
17open Set
18open scoped Topology
20namespace ProCGroups.FreeProC
22universe u v
24section GeneralTopologicalSpaces
29 {G : Type u} [Group G] [TopologicalSpace G] (hG : IsProfiniteGroup G) :
30 InverseSystems.IsProfiniteSpace G :=
31 (InverseSystems.isProfiniteSpace_iff_compact_t2_totallyDisconnected (X := G)).2
32 ⟨hG.2.1, hG.2.2.1, hG.2.2.2⟩
34/-- A closed equivalence relation with finite Hausdorff quotient, viewed as one of the finite
35pointed quotients used to build the profinite reflection of a pointed space. -/
37 (X : Type u) [TopologicalSpace X] (_x0 : X) where
38 toSetoid : Setoid X
39 closed_rel : IsClosed {p : X × X | toSetoid.r p.1 p.2}
40 finite_quotient : Finite (Quotient toSetoid)
41 t2_quotient : T2Space (Quotient toSetoid)
43attribute [instance] PointedFiniteClosedEquivalenceRelation.t2_quotient
45/-- The cardinal `ρ(X)` of clopen subsets of a space. -/
46noncomputable def clopenCardinal
47 (X : Type u) [TopologicalSpace X] : Cardinal :=
48 Cardinal.mk {U : Set X // IsClopen U}
50/-- A bundled profinite reflection of a pointed topological space. This packages the inverse-limit
51space `X̌`, its basepoint, and the natural map `τ : X → X̌`. -/
53 (X : Type u) [TopologicalSpace X] (x0 : X) where
54 carrier : Type u
55 instTopologicalSpace : TopologicalSpace carrier
56 point : carrier
57 τ : X → carrier
58 continuous_τ : Continuous τ
59 map_base : τ x0 = point
60 denseRange_τ : DenseRange τ
61 isProfinite : InverseSystems.IsProfiniteSpace carrier
62 existsUnique_factor :
63 ∀ {Y : Type u} [TopologicalSpace Y],
64 InverseSystems.IsProfiniteSpace Y →
65 ∀ (y0 : Y) (f : X → Y), Continuous f → f x0 = y0 →
66 ∃! ftilde : carrier → Y,
67 Continuous ftilde ∧ ftilde point = y0 ∧ ∀ x, ftilde (τ x) = f x
68 cardinal_quotients_eq_clopen :
72attribute [instance] PointedProfiniteReflectionData.instTopologicalSpace
74/-- After factoring through the profinite reflection, the same free pro-`C` group is free on the
75pointed profinite space `(X̌, ∗)`.
77This formulation includes the bridge saying that `ProC`-targets are profinite spaces. -/
79 {X : Type u} [TopologicalSpace X] {x0 : X}
80 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
81 {ι : X → F}
83 (hProfinite :
84 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
85 ProC (G := G) → InverseSystems.IsProfiniteSpace G)
86 (hι : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι) :
87 ∃ ιtilde : Xhat.carrier → F,
88 Continuous ιtilde ∧
89 ιtilde Xhat.point = 1 ∧
90 (∀ x, ιtilde (Xhat.τ x) = ι x) ∧
91 IsPointedFreeProCGroupOn (ProC := ProC) Xhat.carrier Xhat.point F ιtilde := by
92 let hfactor :=
93 Xhat.existsUnique_factor (hProfinite hι.isProC) 1 ι hι.continuous_ι hι.map_base
94 let ιtilde : Xhat.carrier → F := Classical.choose (ExistsUnique.exists hfactor)
95 have hιtilde : Continuous ιtilde ∧ ιtilde Xhat.point = 1 ∧
96 ∀ x, ιtilde (Xhat.τ x) = ι x :=
97 Classical.choose_spec (ExistsUnique.exists hfactor)
98 refine ⟨ιtilde, hιtilde.1, hιtilde.2.1, hιtilde.2.2, ?_⟩
99 refine ⟨hι.isProC, hιtilde.1, hιtilde.2.1, ?_, ?_⟩
100 · have hsubset : Set.range ι ⊆ Set.range ιtilde := by
101 rintro z ⟨x, rfl⟩
102 exact ⟨Xhat.τ x, hιtilde.2.2 x⟩
103 have hsub :
104 Subgroup.closure (Set.range ι) ≤
105 Subgroup.closure (Set.range ιtilde) :=
106 Subgroup.closure_mono hsubset
107 have hsub' :
108 (Subgroup.closure (Set.range ι)).topologicalClosure ≤
109 (Subgroup.closure (Set.range ιtilde)).topologicalClosure := by
110 exact Subgroup.topologicalClosure_minimal _ (hsub.trans (Subgroup.le_topologicalClosure _))
111 (Subgroup.isClosed_topologicalClosure _)
112 rw [hι.generates_range] at hsub'
113 exact top_unique hsub'
114 intro G _ _ _ hG φ hφ hφ0 hgen
115 let ψ : X → G := φ ∘ Xhat.τ
116 have hψ : Continuous ψ := hφ.comp Xhat.continuous_τ
117 have hψ0 : ψ x0 = 1 := by
118 simpa [ψ, Function.comp, Xhat.map_base] using hφ0
119 have hgenψ : Generation.TopologicallyGenerates (G := G) (Set.range ψ) := by
120 have hclosureRange : closure (Set.range ψ) = closure (Set.range φ) := by
121 have hsubset : Set.range ψ ⊆ Set.range φ := by
122 rintro z ⟨x, rfl⟩
123 exact ⟨Xhat.τ x, rfl⟩
124 apply le_antisymm
125 · exact closure_mono hsubset
126 · have hdense : Dense (Set.range Xhat.τ) := Xhat.denseRange_τ
127 have hrange : Set.range φ ⊆ closure (Set.range ψ) := by
128 simpa [Set.range_comp, Function.comp, ψ] using
129 (Continuous.range_subset_closure_image_dense (f := φ) hφ hdense)
130 exact closure_minimal hrange isClosed_closure
131 have hgenClosure :
132 Generation.TopologicallyGenerates (G := G) (closure (Set.range ψ)) := by
133 rw [hclosureRange]
134 exact (Generation.topologicallyGenerates_closure_iff (G := G) (X := Set.range φ)).1 hgen
135 exact (Generation.topologicallyGenerates_closure_iff (G := G) (X := Set.range ψ)).2 hgenClosure
136 rcases hι.existsUnique_lift hG ψ hψ hψ0 hgenψ with ⟨f, hf, huniq⟩
137 refine ⟨f, ⟨hf.1, ?_⟩, ?_⟩
138 · have hGprofinite : InverseSystems.IsProfiniteSpace G := hProfinite hG
139 let hGctd :=
140 (InverseSystems.isProfiniteSpace_iff_compact_t2_totallyDisconnected (X := G)).1 hGprofinite
141 letI : CompactSpace G := hGctd.1
142 letI : T2Space G := hGctd.2.1
143 have hEq :
144 (fun y => f (ιtilde y)) = φ := by
145 apply DenseRange.equalizer (f := Xhat.τ) Xhat.denseRange_τ
146 · exact hf.1.comp hιtilde.1
147 · exact hφ
148 · funext x
149 simpa [Function.comp, ψ, hιtilde.2.2 x] using hf.2 x
150 intro y
151 exact congrFun hEq y
152 · intro g hg
153 apply huniq g
154 refine ⟨hg.1, ?_⟩
155 intro x
156 simpa [ψ, Function.comp, hιtilde.2.2 x] using
157 hg.2 (Xhat.τ x)
159end GeneralTopologicalSpaces
161end ProCGroups.FreeProC