ProCGroups/InverseSystems/Quotients.lean
1import ProCGroups.InverseSystems.CompatibilityAndSurjectivity
2import ProCGroups.Topologies.QuotientMaps
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/InverseSystems/Quotients.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 scoped Topology
20namespace ProCGroups
21namespace InverseSystems
23universe u v
25namespace InverseSystem
27variable {I : Type u} [Preorder I]
28variable (S : InverseSystem.{u, v} (I := I))
29variable [∀ i, Group (S.X i)] [IsGroupSystem S]
30variable [∀ i, IsTopologicalGroup (S.X i)]
32/-- The transition map of a group-valued inverse system, bundled as a homomorphism. -/
33def transitionHom {i j : I} (hij : i ≤ j) : S.X j →* S.X i where
34 toFun := S.map hij
35 map_one' := IsGroupSystem.map_one (S := S) hij
36 map_mul' := IsGroupSystem.map_mul (S := S) hij
38omit [∀ i, IsTopologicalGroup (S.X i)] in
39@[simp] theorem transitionHom_apply {i j : I} (hij : i ≤ j) (x : S.X j) :
40 S.transitionHom hij x = S.map hij x := rfl
42omit [∀ i, IsTopologicalGroup (S.X i)] in
43/-- The bundled transition homomorphism is continuous. -/
44theorem continuous_transitionHom {i j : I} (hij : i ≤ j) :
45 Continuous (S.transitionHom hij) :=
46 S.continuous_map hij
48/-- Closed normal subgroups of the stages, compatible with transition maps. -/
49structure CompatibleClosedNormalSubgroups where
50 N : ∀ i, Subgroup (S.X i)
51 normal : ∀ i, (N i).Normal
52 closed : ∀ i, IsClosed ((N i : Subgroup (S.X i)) : Set (S.X i))
53 map_le :
54 ∀ {i j : I} (hij : i ≤ j), N j ≤ (N i).comap (S.transitionHom hij)
56namespace CompatibleClosedNormalSubgroups
58variable {S}
59variable (Q : S.CompatibleClosedNormalSubgroups)
61instance instNormalN (i : I) : (Q.N i).Normal := Q.normal i
63/-- The transition map induced on stage quotients. -/
64def quotientMap {i j : I} (hij : i ≤ j) :
65 S.X j ⧸ Q.N j →* S.X i ⧸ Q.N i :=
66 QuotientGroup.map (N := Q.N j) (M := Q.N i) (f := S.transitionHom hij) (Q.map_le hij)
68omit [∀ i, IsTopologicalGroup (S.X i)] in
69@[simp] theorem quotientMap_mk {i j : I} (hij : i ≤ j) (x : S.X j) :
70 Q.quotientMap hij (QuotientGroup.mk' (Q.N j) x) =
71 QuotientGroup.mk' (Q.N i) (S.map hij x) := by
72 exact QuotientGroup.map_mk' (N := Q.N j) (M := Q.N i)
73 (f := S.transitionHom hij) (Q.map_le hij) x
75omit [∀ i, IsTopologicalGroup (S.X i)] in
76/-- The induced map on stage quotients is continuous. -/
77theorem continuous_quotientMap {i j : I} (hij : i ≤ j) :
78 Continuous (Q.quotientMap hij) := by
79 refine (QuotientGroup.isQuotientMap_mk (N := Q.N j)).continuous_iff.2 ?_
80 change Continuous fun x : S.X j => QuotientGroup.mk' (Q.N i) (S.map hij x)
81 exact QuotientGroup.continuous_mk.comp (S.continuous_map hij)
83/-- The inverse system obtained by quotienting each stage by a compatible closed normal subgroup. -/
84def quotientInverseSystem : InverseSystem (I := I) where
85 X := fun i => S.X i ⧸ Q.N i
86 topologicalSpace := fun i => inferInstance
87 map := fun {_i _j} hij => Q.quotientMap hij
88 continuous_map := fun {_i _j} hij => Q.continuous_quotientMap hij
89 map_id := by
90 intro i
91 funext x
92 refine Quotient.inductionOn' x ?_
93 intro a
94 change QuotientGroup.mk' (Q.N i) (S.map (le_rfl : i ≤ i) a) =
95 QuotientGroup.mk' (Q.N i) a
96 exact congrArg (QuotientGroup.mk' (Q.N i)) (S.map_id_apply i a)
97 map_comp := by
98 intro i j k hij hjk
99 funext x
100 refine Quotient.inductionOn' x ?_
101 intro a
102 change QuotientGroup.mk' (Q.N i) (S.map hij (S.map hjk a)) =
103 QuotientGroup.mk' (Q.N i) (S.map (hij.trans hjk) a)
104 exact congrArg (QuotientGroup.mk' (Q.N i)) (S.map_comp_apply hij hjk a)
106instance quotientInverseSystem_stageGroup (i : I) :
107 Group (Q.quotientInverseSystem.X i) := by
108 change Group (S.X i ⧸ Q.N i)
109 infer_instance
111instance quotientInverseSystem_stageTopologicalGroup (i : I) :
112 IsTopologicalGroup (Q.quotientInverseSystem.X i) := by
113 change IsTopologicalGroup (S.X i ⧸ Q.N i)
114 infer_instance
116/-- The quotient inverse system is group-valued. -/
117instance quotientInverseSystem_isGroupSystem :
118 IsGroupSystem Q.quotientInverseSystem where
120 intro i j hij
123 intro i j hij x y
125 map_inv := by
126 intro i j hij x
127 exact (Q.quotientMap hij).map_inv x
129/-- The stagewise quotient maps form a morphism from the original system to the quotient system. -/
130def toQuotientInverseSystem : S.Morphism Q.quotientInverseSystem where
131 map := fun i => QuotientGroup.mk' (Q.N i)
132 continuous_map := fun _ => QuotientGroup.continuous_mk
133 comm := by
134 intro i j hij
135 funext x
136 exact (Q.quotientMap_mk hij x).symm
138/-- Kernel of the map from the inverse limit to the inverse limit of stage quotients. -/
139def inverseLimitKernel : Subgroup S.inverseLimit :=
140 ⨅ i, (Q.N i).comap (projectionHom (S := S) i)
142instance inverseLimitKernel_normal : Q.inverseLimitKernel.Normal where
143 conj_mem x hx g := by
144 rw [inverseLimitKernel] at hx ⊢
145 simp only [projectionHom, Subgroup.mem_iInf, Subgroup.mem_comap, MonoidHom.coe_mk, OneHom.coe_mk,
146 projection_apply] at hx ⊢
147 intro i
148 simpa using (Q.normal i).conj_mem (S.projection i x) (hx i) (S.projection i g)
150omit [∀ i, IsTopologicalGroup (S.X i)] in
151theorem mem_inverseLimitKernel_iff (x : S.inverseLimit) :
152 x ∈ Q.inverseLimitKernel ↔ ∀ i, S.projection i x ∈ Q.N i := by
153 simp only [inverseLimitKernel, projectionHom, Subgroup.mem_iInf, Subgroup.mem_comap, MonoidHom.coe_mk,
154 OneHom.coe_mk, projection_apply]
156/-- The canonical comparison from the quotient of the inverse limit to the inverse limit of the
157stage quotients. -/
158noncomputable def quotientInverseLimitComparison :
159 S.inverseLimit ⧸ Q.inverseLimitKernel →ₜ* Q.quotientInverseSystem.inverseLimit := by
160 let T : InverseSystem (I := I) := Q.quotientInverseSystem
161 let φ : S.inverseLimit →ₜ* T.inverseLimit :=
162 { toMonoidHom :=
163 { toFun := S.limMap Q.toQuotientInverseSystem
164 map_one' := by
165 apply T.ext
166 intro i
167 calc
168 T.projection i (S.limMap Q.toQuotientInverseSystem 1) =
169 Q.toQuotientInverseSystem.map i (S.projection i (1 : S.inverseLimit)) := by
170 exact S.π_limMap_apply Q.toQuotientInverseSystem i 1
171 _ = 1 := by
172 change QuotientGroup.mk' (Q.N i) (S.projection i (1 : S.inverseLimit)) = 1
173 rw [projection_one (S := S) i]
174 simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one]
175 map_mul' := by
176 intro x y
177 apply T.ext
178 intro i
179 calc
180 T.projection i (S.limMap Q.toQuotientInverseSystem (x * y)) =
181 Q.toQuotientInverseSystem.map i (S.projection i (x * y)) := by
182 exact S.π_limMap_apply Q.toQuotientInverseSystem i (x * y)
183 _ =
184 Q.toQuotientInverseSystem.map i (S.projection i x) *
185 Q.toQuotientInverseSystem.map i (S.projection i y) := by
186 change QuotientGroup.mk' (Q.N i) (S.projection i (x * y)) =
187 QuotientGroup.mk' (Q.N i) (S.projection i x) *
188 QuotientGroup.mk' (Q.N i) (S.projection i y)
189 rw [projection_mul (S := S) i x y]
190 simp only [projection_apply, QuotientGroup.mk'_apply, QuotientGroup.mk_mul]
191 _ =
192 T.projection i (S.limMap Q.toQuotientInverseSystem x) *
193 T.projection i (S.limMap Q.toQuotientInverseSystem y) := by
194 rw [← S.π_limMap_apply Q.toQuotientInverseSystem i x,
195 ← S.π_limMap_apply Q.toQuotientInverseSystem i y] }
196 continuous_toFun := S.continuous_limMap Q.toQuotientInverseSystem }
197 refine QuotientGroup.liftₜ Q.inverseLimitKernel φ ?_
198 intro x hx
199 apply T.ext
200 intro i
201 have hxi : S.projection i x ∈ Q.N i := (Q.mem_inverseLimitKernel_iff x).1 hx i
202 change QuotientGroup.mk' (Q.N i) (S.projection i x) = 1
203 exact (QuotientGroup.eq_one_iff (N := Q.N i) (S.projection i x)).2 hxi
205omit [∀ i, IsTopologicalGroup (S.X i)] in
206@[simp] theorem quotientInverseLimitComparison_mk (x : S.inverseLimit) :
207 Q.quotientInverseLimitComparison (QuotientGroup.mk' Q.inverseLimitKernel x) =
208 S.limMap Q.toQuotientInverseSystem x :=
209 by
211 rfl
213omit [∀ i, IsTopologicalGroup (S.X i)] in
214@[simp] theorem projection_quotientInverseLimitComparison_mk
215 (i : I) (x : S.inverseLimit) :
216 Q.quotientInverseSystem.projection i
217 (Q.quotientInverseLimitComparison (QuotientGroup.mk' Q.inverseLimitKernel x)) =
218 QuotientGroup.mk' (Q.N i) (S.projection i x) := by
220 rfl
222omit [∀ i, IsTopologicalGroup (S.X i)] in
223/-- The comparison map has trivial kernel. -/
224theorem ker_quotientInverseLimitComparison :
225 Q.quotientInverseLimitComparison.toMonoidHom.ker = ⊥ := by
226 ext a
227 constructor
228 · intro ha
229 refine Quotient.inductionOn' a ?_ ha
230 intro x hx
231 rw [MonoidHom.mem_ker] at hx
232 rw [Subgroup.mem_bot]
233 exact (QuotientGroup.eq_one_iff (N := Q.inverseLimitKernel) x).2 <| by
234 rw [Q.mem_inverseLimitKernel_iff]
235 intro i
236 have hcoord :=
237 congrArg (fun y => Q.quotientInverseSystem.projection i y) hx
238 change QuotientGroup.mk' (Q.N i) (S.projection i x) = 1 at hcoord
239 exact (QuotientGroup.eq_one_iff (N := Q.N i) (S.projection i x)).1 hcoord
240 · intro ha
241 rw [Subgroup.mem_bot] at ha
242 rw [MonoidHom.mem_ker, ha]
245omit [∀ i, IsTopologicalGroup (S.X i)] in
246/-- The comparison map is injective: its kernel is exactly the subgroup used in the quotient. -/
248 Function.Injective Q.quotientInverseLimitComparison :=
249 (MonoidHom.ker_eq_bot_iff (f := Q.quotientInverseLimitComparison.toMonoidHom)).mp
250 Q.ker_quotientInverseLimitComparison
252/-- The comparison map is surjective for compact Hausdorff systems over a directed index. -/
254 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
255 (hdir : Directed (· ≤ ·) (id : I → I)) :
256 Function.Surjective Q.quotientInverseLimitComparison := by
257 let T : InverseSystem (I := I) := Q.quotientInverseSystem
258 letI : ∀ i, T2Space (T.X i) := fun i => by
259 dsimp [T, quotientInverseSystem]
260 haveI : IsClosed ((Q.N i : Subgroup (S.X i)) : Set (S.X i)) := Q.closed i
261 infer_instance
262 have hlimsurj : Function.Surjective (S.limMap Q.toQuotientInverseSystem) :=
263 S.surjective_limMap (T := T) hdir Q.toQuotientInverseSystem
264 (fun i => QuotientGroup.mk'_surjective (Q.N i))
265 intro y
266 rcases hlimsurj y with ⟨x, hx⟩
267 refine ⟨QuotientGroup.mk' Q.inverseLimitKernel x, ?_⟩
268 simpa [quotientInverseLimitComparison_mk] using hx
270/-- The comparison map is bijective for compact Hausdorff systems over a directed index. -/
272 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
273 (hdir : Directed (· ≤ ·) (id : I → I)) :
274 Function.Bijective Q.quotientInverseLimitComparison :=
275 ⟨Q.injective_quotientInverseLimitComparison,
276 Q.surjective_quotientInverseLimitComparison hdir⟩
278/-- The quotient of an inverse limit by a compatible closed normal family is the inverse limit of
279the stage quotients. -/
280noncomputable def quotientInverseLimitContinuousMulEquiv
281 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
282 (hdir : Directed (· ≤ ·) (id : I → I)) :
283 S.inverseLimit ⧸ Q.inverseLimitKernel ≃ₜ* Q.quotientInverseSystem.inverseLimit := by
284 let T : InverseSystem (I := I) := Q.quotientInverseSystem
285 let f := Q.quotientInverseLimitComparison
286 letI : CompactSpace S.inverseLimit := inferInstance
287 letI : CompactSpace (S.inverseLimit ⧸ Q.inverseLimitKernel) := inferInstance
288 letI : ∀ i, T2Space (T.X i) := fun i => by
289 dsimp [T, quotientInverseSystem]
290 haveI : IsClosed ((Q.N i : Subgroup (S.X i)) : Set (S.X i)) := Q.closed i
291 infer_instance
292 letI : T2Space T.inverseLimit := T.t2Space_inverseLimit
293 exact ContinuousMulEquiv.ofBijectiveCompactToT2
294 f.toMonoidHom f.continuous_toFun (Q.bijective_quotientInverseLimitComparison hdir)
298end InverseSystem
300end InverseSystems
301end ProCGroups