Yamaguchi Lean 4 Library
ProCGroups/ProC/OpenNormalSubgroups/LimitPresentation.lean
ProCGroups/ProC/OpenNormalSubgroups/LimitPresentation/Source

ProCGroups/ProC/OpenNormalSubgroups/LimitPresentation.lean

1import ProCGroups.InverseSystems.ProfiniteSpace
2import ProCGroups.InverseSystems.CompatibilityAndSurjectivity
3import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
4import ProCGroups.Topologies.ContinuousMulEquiv
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/ProC/OpenNormalSubgroups/LimitPresentation.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Inverse-limit presentations of pro-`C` groups
17Canonical inverse-limit and exact-basis characterizations for pro-`C` groups.
18-/
20namespace ProCGroups.ProC
22universe u v
24variable {C : FiniteGroupClass.{u}}
25variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
27namespace IsProCGroup
29/-- A pro-`C` group is canonically the inverse limit of its quotients by open normal subgroups
30whose quotients lie in `C`. -/
32 (hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
33 G ≃ₜ* (openNormalSubgroupInClassSystem C G).inverseLimit := by
35 letI : Nonempty (OpenNormalSubgroupInClass C G) := openNormalSubgroupInClass_nonempty hG
36 letI : Nonempty (OrderDual (OpenNormalSubgroupInClass C G)) := inferInstance
37 letI : CompactSpace G := IsProCGroup.compactSpace hG
38 letI : T2Space G := IsProCGroup.t2Space hG
39 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), Group (S.X U) := fun U => by
41 infer_instance
42 letI : InverseSystems.IsGroupSystem S := by
43 dsimp [S]
44 infer_instance
45 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), T2Space (S.X U) := fun U => by
46 letI : DiscreteTopology (S.X U) := by
48 exact QuotientGroup.discreteTopology
49 (openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
50 infer_instance
51 letI : Group S.inverseLimit := by infer_instance
52 letI : T2Space S.inverseLimit := S.t2Space_inverseLimit
53 let φ : G →* S.inverseLimit :=
54 { toFun := S.inverseLimitLift
55 (fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
56 openNormalSubgroupInClassProj (C := C) (G := G) U)
58 map_one' := by
59 apply S.ext
60 intro i
61 rfl
62 map_mul' := by
63 intro x y
64 apply S.ext
65 intro i
66 rfl }
67 have hφcont : Continuous φ :=
68 S.continuous_inverseLimitLift
69 (fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
70 openNormalSubgroupInClassProj (C := C) (G := G) U)
71 (fun _ => continuous_quotient_mk')
73 have hφinj : Function.Injective φ := by
74 intro x y hxy
75 have hmem :
76 x⁻¹ * y ∈ iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) := by
77 rw [Subgroup.mem_iInf]
78 intro U
79 let i : OrderDual (OpenNormalSubgroupInClass C G) := OrderDual.toDual U
80 have hi :
81 openNormalSubgroupInClassProj (C := C) (G := G) i x =
82 openNormalSubgroupInClassProj (C := C) (G := G) i y := by
83 simpa [φ] using congrArg (fun z : S.inverseLimit => S.projection i z) hxy
84 exact QuotientGroup.eq.1 (by
86 have hone : x⁻¹ * y = 1 := by
87 have : x⁻¹ * y ∈ (⊥ : Subgroup G) := by
88 simpa [hG.iInf_openNormalSubgroupInClass_eq_bot] using hmem
89 simpa using this
90 calc
91 x = x * 1 := by simp only [mul_one]
92 _ = x * (x⁻¹ * y) := by rw [hone]
93 _ = y := by simp only [mul_inv_cancel_left]
94 have hφsurj : Function.Surjective φ :=
95 InverseSystems.InverseSystem.surjective_inverseLimitLift (S := S)
96 (fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
97 openNormalSubgroupInClassProj (C := C) (G := G) U)
98 (fun _ => continuous_quotient_mk')
100 (fun U => openNormalSubgroupInClassProj_surjective (C := C) (G := G) U)
101 (directed_openNormalSubgroupInClass (C := C) (G := G) hForm)
102 exact ContinuousMulEquiv.ofBijectiveCompactToT2 φ hφcont ⟨hφinj, hφsurj⟩
105 (hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G)
106 (U : OrderDual (OpenNormalSubgroupInClass C G)) (g : G) :
109 (C := C) (G := G) hForm hG g) =
110 openNormalSubgroupInClassProj (C := C) (G := G) U g := by
111 simp only [openNormalSubgroupInClassMulEquivInverseLimit, ContinuousMulEquiv.ofBijectiveCompactToT2, id_eq,
112 MonoidHom.coe_mk, OneHom.coe_mk, ContinuousMulEquiv.coe_mk', Equiv.toHomeomorphOfContinuousClosed_apply,
113 Equiv.ofBijective_apply, InverseSystems.InverseSystem.inverseLimitLift,
114 InverseSystems.InverseSystem.projection_apply]
116/-- A pro-`C` group is topologically isomorphic to an inverse limit of finite groups in `C`,
117realized using the quotient system indexed by the open normal subgroups whose quotients lie in
118`C`. -/
120 (hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
122 (∀ U : OrderDual (OpenNormalSubgroupInClass C G), C (S.X U) ∧ Finite (S.X U)) ∧
123 Nonempty (G ≃ₜ* S.inverseLimit) := by
125 refine ⟨?_, ⟨openNormalSubgroupInClassMulEquivInverseLimit (C := C) (G := G) hForm hG⟩⟩
126 intro U
128 refine ⟨(OrderDual.ofDual U).2, ?_⟩
129 exact hForm.finiteOnly (OrderDual.ofDual U).2
131end IsProCGroup
133/-- Existence of an exact open-normal subgroup basis with quotients in `C`. -/
134def HasExactOpenNormalQuotientBasisInClass (C : FiniteGroupClass.{u})
135 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
136 CompactSpace G ∧
137 ∃ ι : Type u, ∃ U : ι → OpenNormalSubgroup G,
138 (∀ i, C (G ⧸ (U i : Subgroup G))) ∧
139 (∀ W : Set G, IsOpen W → (1 : G) ∈ W →
140 ∃ i, (((U i : Subgroup G) : Set G)) ⊆ W) ∧
141 iInf (fun i => (U i : Subgroup G)) = (⊥ : Subgroup G)
143/-- An exact open-normal family with trivial intersection makes the group Hausdorff. -/
145 (hC : HasExactOpenNormalQuotientBasisInClass C G) : T2Space G := by
146 rcases hC with ⟨_, ι, U, _, _, hInf⟩
147 refine ⟨?_⟩
148 intro x y hxy
149 have hxy' : x⁻¹ * y ≠ 1 := by
150 intro h1
151 apply hxy
152 simpa using inv_mul_eq_one.mp h1
153 have hsep : ∃ i : ι, x⁻¹ * y ∉ (U i : Subgroup G) := by
154 by_contra hsep
155 have hxall : ∀ i : ι, x⁻¹ * y ∈ (U i : Subgroup G) := by
156 intro i
157 by_contra hxyi
158 exact hsep ⟨i, hxyi⟩
159 have hxinf : x⁻¹ * y ∈ iInf (fun i => (U i : Subgroup G)) := by
160 simpa [Subgroup.mem_iInf] using hxall
161 have hxbot : x⁻¹ * y ∈ (⊥ : Subgroup G) := by
162 simpa [hInf] using hxinf
163 exact hxy' (by simpa using hxbot)
164 rcases hsep with ⟨i, hxyi⟩
165 have hclopenCoset :
166 ∀ z : G, IsClopen {g : G | z⁻¹ * g ∈ (U i : Subgroup G)} := by
167 intro z
168 let f : G → G := fun g => z⁻¹ * g
169 have hf : Continuous f := continuous_const.mul continuous_id
170 refine ⟨?_, ?_⟩
171 · simpa [f] using (openSubgroup_isClosed (G := G) (U i).toOpenSubgroup).preimage hf
172 · simpa [f] using (openSubgroup_isOpen (G := G) (U i).toOpenSubgroup).preimage hf
173 refine ⟨{g : G | x⁻¹ * g ∈ (U i : Subgroup G)},
174 {g : G | y⁻¹ * g ∈ (U i : Subgroup G)}, ?_, ?_, ?_, ?_, ?_⟩
175 · exact (hclopenCoset x).2
176 · exact (hclopenCoset y).2
177 · simp only [OpenSubgroup.mem_toSubgroup, Set.mem_setOf_eq, inv_mul_cancel, one_mem]
178 · simp only [OpenSubgroup.mem_toSubgroup, Set.mem_setOf_eq, inv_mul_cancel, one_mem]
179 · refine Set.disjoint_left.2 ?_
180 intro g hx hg
181 apply hxyi
182 have hmul :
183 (x⁻¹ * g) * (y⁻¹ * g)⁻¹ ∈ (U i : Subgroup G) :=
184 (U i).mul_mem hx ((U i).inv_mem hg)
185 simpa [mul_assoc] using hmul
187/-- An exact open-normal family yields a clopen basis and hence total disconnectedness. -/
189 (hC : HasExactOpenNormalQuotientBasisInClass C G) : TotallyDisconnectedSpace G := by
190 have hC' := hC
191 rcases hC' with ⟨_, ι, U, _, hbasis, _⟩
192 letI : T2Space G := t2Space_of_exactOpenNormalQuotientBasisInClass (C := C) hC
193 have hclopenBasis : TopologicalSpace.IsTopologicalBasis {s : Set G | IsClopen s} := by
194 refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
195 · intro s hs
196 exact hs.2
197 · intro x W hxW hW
198 let W₁ : Set G := (fun g : G => x * g) ⁻¹' W
199 have hW₁ : IsOpen W₁ := hW.preimage (continuous_const.mul continuous_id)
200 have h1W₁ : (1 : G) ∈ W₁ := by
201 simpa [W₁] using hxW
202 rcases hbasis W₁ hW₁ h1W₁ with ⟨i, hi⟩
203 have hclopenCoset : IsClopen {g : G | x⁻¹ * g ∈ (U i : Subgroup G)} := by
204 let f : G → G := fun g => x⁻¹ * g
205 have hf : Continuous f := continuous_const.mul continuous_id
206 refine ⟨?_, ?_⟩
207 · simpa [f] using (openSubgroup_isClosed (G := G) (U i).toOpenSubgroup).preimage hf
208 · simpa [f] using (openSubgroup_isOpen (G := G) (U i).toOpenSubgroup).preimage hf
209 refine ⟨{g : G | x⁻¹ * g ∈ (U i : Subgroup G)}, ?_, by simp only [OpenSubgroup.mem_toSubgroup, Set.mem_setOf_eq, inv_mul_cancel, one_mem], ?_⟩
210 · exact hclopenCoset
211 · intro g hg
212 have hxgW₁ : x⁻¹ * g ∈ W₁ := hi hg
213 simpa [W₁, mul_assoc] using hxgW₁
214 exact InverseSystems.totallyDisconnectedSpace_of_t2_basis_clopen G hclopenBasis
216/-- An exact open-normal family with quotients in `C` implies the working Lean notion of a
217pro-`C` group. This direction needs no formation closure: the exact basis already supplies the
218required open-normal quotients in `C`. -/
220 (hC : HasExactOpenNormalQuotientBasisInClass C G) : IsProCGroup C G := by
221 have hC' := hC
222 rcases hC' with ⟨hcompact, ι, U, hCU, hbasis, hInf⟩
223 letI : CompactSpace G := hcompact
224 letI : T2Space G := t2Space_of_exactOpenNormalQuotientBasisInClass (C := C) hC
225 letI : TotallyDisconnectedSpace G :=
227 refine ⟨⟨inferInstance, hcompact, inferInstance, inferInstance⟩, ?_⟩
228 intro W hW h1W
229 rcases hbasis W hW h1W with ⟨i, hiW⟩
230 exact ⟨U i, hiW, hCU i⟩
232end ProCGroups.ProC