Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.Generators
1import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.FiniteQuotients
2import ProCGroups.Generation.QuotientGeneratorConvergingPairs
4/-!
5# Generating sets converging to zero
7This file defines sets and maps converging to zero through open submodules and relates them to
8one-point extensions and dense additive generation. Every profinite module is shown to admit an
9appropriate generating set.
10-/
12open scoped Topology
14namespace CompletedGroupAlgebra
16universe u v w z
18/-- A subset converges to zero in the all-but-finitely-many-elements sense used in the book. -/
19def SetConvergesToZero {M : Type v} [TopologicalSpace M] [Zero M] (S : Set M) : Prop :=
20 ∀ U ∈ 𝓝 (0 : M), (S \ U).Finite
22/--
23A map from an arbitrary index type converges to zero along the cofinite filter. This is the
24map-level version used in Lemma 5.2.5(b).
25-/
26def MapConvergesToZero {S : Type u} {M : Type v} [TopologicalSpace M] [Zero M]
27 (f : S → M) : Prop :=
28 Filter.Tendsto f Filter.cofinite (𝓝 (0 : M))
30/-- A map converging to zero has image set converging to zero. -/
31theorem MapConvergesToZero.setConvergesToZero_range
32 {S : Type u} {M : Type v} [TopologicalSpace M] [Zero M] {f : S → M}
33 (hf : MapConvergesToZero f) :
34 SetConvergesToZero (Set.range f) := by
35 intro U hU
36 have hpre : {s : S | f s ∉ U}.Finite := by
37 have hmem : {s : S | f s ∈ U} ∈ (Filter.cofinite : Filter S) := hf hU
38 simpa [Filter.mem_cofinite, Set.compl_setOf] using hmem
39 exact (hpre.image f).subset (by
40 rintro y ⟨⟨s, rfl⟩, hsU⟩
41 exact ⟨s, hsU, rfl⟩)
43/-- An injective parametrization of a set converging to zero is a map converging to zero. -/
44theorem SetConvergesToZero.mapConvergesToZero_of_injective
45 {S : Type u} {M : Type v} [TopologicalSpace M] [Zero M] {f : S → M}
46 (hfconv : SetConvergesToZero (Set.range f)) (hfinj : Function.Injective f) :
47 MapConvergesToZero f := by
48 intro U hU
49 have hbad : ({s : S | f s ∉ U} : Set S).Finite := by
50 have hpre :
51 ({s : S | f s ∉ U} : Set S) = f ⁻¹' (Set.range f \ U) := by
52 ext s
53 simp only [Set.mem_setOf_eq, Set.preimage_sdiff, Set.preimage_range, Set.mem_sdiff,
54 Set.mem_univ,
55 Set.mem_preimage, true_and]
56 rw [hpre]
57 exact Set.Finite.preimage (f := f) (s := Set.range f \ U) hfinj.injOn
58 (hfconv U hU)
59 change f ⁻¹' U ∈ (Filter.cofinite : Filter S)
60 rw [Filter.mem_cofinite]
61 rw [← Set.preimage_compl]
62 have hpreimageCompl : f ⁻¹' Uᶜ = {s : S | f s ∉ U} := by
63 ext s
64 simp only [Set.mem_preimage, Set.mem_compl_iff, Set.mem_setOf_eq]
65 rw [hpreimageCompl]
66 exact hbad
68/-- The inclusion of a set converging to zero, viewed as a parametrized map, converges to zero. -/
69theorem SetConvergesToZero.subtype_val
70 {M : Type v} [TopologicalSpace M] [Zero M] {S : Set M}
71 (hS : SetConvergesToZero S) :
72 MapConvergesToZero (fun s : S => (s : M)) := by
73 have hrange : Set.range (fun s : S => (s : M)) = S := by
74 ext x
75 constructor
76 · rintro ⟨s, rfl⟩
77 exact s.2
78 · intro hx
79 exact ⟨⟨x, hx⟩, rfl⟩
80 have hRangeConv : SetConvergesToZero (Set.range fun s : S => (s : M)) := by
81 simpa [hrange] using hS
82 exact hRangeConv.mapConvergesToZero_of_injective Subtype.val_injective
84/--
85A map from a discrete set converges to zero if and only if its zero-extension to the one-point
86compactification is continuous.
87-/
88theorem continuous_onePoint_zero_extension_iff_mapConvergesToZero
89 {S : Type u} {M : Type v} [TopologicalSpace S] [DiscreteTopology S]
90 [TopologicalSpace M] [Zero M] {f : S → M} :
91 Continuous (fun x : OnePoint S => x.elim 0 f) ↔ MapConvergesToZero f := by
92 rw [OnePoint.continuous_iff_from_discrete]
93 rfl
95/-- Finite subsets converge to zero in the all-but-finitely-many-elements sense used in the book. -/
96theorem finite_setConvergesToZero
97 {M : Type v} [TopologicalSpace M] [Zero M] {S : Set M} (hS : S.Finite) :
98 SetConvergesToZero S := by
99 intro U _hU
100 exact hS.subset Set.sdiff_subset
102/-- A set of topological module generators converging to zero. -/
103def HasGeneratingSetConvergingToZero (Λ : Type u) (M : Type v) [Ring Λ]
104 [TopologicalSpace M] [AddCommGroup M] [Module Λ M] : Prop :=
105 ∃ S : Set M, closure (Submodule.span Λ S : Set M) = Set.univ ∧ SetConvergesToZero S
107/--
108A finite dense generating set is a generating set converging to zero. This gives the
109finite-generated special case of Lemma 5.1.1(c).
110-/
111theorem finiteGeneratingSet_convergesToZero
112 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M] [AddCommGroup M]
113 [Module Λ M] {S : Set M}
114 (hgen : closure (Submodule.span Λ S : Set M) = Set.univ) (hS : S.Finite) :
115 HasGeneratingSetConvergingToZero Λ M := by
116 exact ⟨S, hgen, finite_setConvergesToZero hS⟩
118/-- A dense additive generating set is also a dense module generating set. -/
119theorem hasGeneratingSetConvergingToZero_of_dense_addSubgroup
120 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M] [AddCommGroup M]
121 [Module Λ M] {S : Set M}
122 (hspan : closure (((AddSubgroup.closure S : AddSubgroup M) : Set M)) = Set.univ)
123 (hconv : SetConvergesToZero S) :
124 HasGeneratingSetConvergingToZero Λ M := by
125 refine ⟨S, ?_, hconv⟩
126 have hsubset : ((AddSubgroup.closure S : AddSubgroup M) : Set M) ⊆
127 ((Submodule.span Λ S : Submodule Λ M) : Set M) := by
128 intro x hx
129 have hle : AddSubgroup.closure S ≤ (Submodule.span Λ S).toAddSubgroup :=
130 (AddSubgroup.closure_le (K := (Submodule.span Λ S).toAddSubgroup)).2
131 fun y hy => Submodule.subset_span hy
132 exact hle hx
133 have hclosure :
134 closure (((AddSubgroup.closure S : AddSubgroup M) : Set M)) ⊆
135 closure (((Submodule.span Λ S : Submodule Λ M) : Set M)) :=
136 closure_mono hsubset
137 exact Set.eq_univ_of_univ_subset (by simpa [hspan] using hclosure)
139/--
140The multiplicative homeomorphism identifies the additive profinite-module structure with its
141multiplicative notation.
142-/
143private def multiplicativeHomeomorph (M : Type*) [TopologicalSpace M] : M ≃ₜ Multiplicative M where
144 toEquiv := Multiplicative.ofAdd
145 continuous_toFun := continuous_ofAdd
146 continuous_invFun := continuous_toAdd
148/-- In Lemma 5.1.1(c), every profinite module has a generating set converging to zero. -/
149theorem profiniteModule_hasGeneratingSetConvergingToZero
150 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
151 [AddCommGroup M] [TopologicalSpace M] [Module Λ M]
152 [IsTopologicalRing Λ] [CompactSpace Λ] [IsTopologicalAddGroup M]
153 [ContinuousSMul Λ M] [CompactSpace M] [T2Space M] [TotallyDisconnectedSpace M] :
154 HasGeneratingSetConvergingToZero Λ M := by
155 let e : M ≃ₜ Multiplicative M := multiplicativeHomeomorph M
156 letI : CompactSpace (Multiplicative M) := e.compactSpace
157 letI : T2Space (Multiplicative M) := e.t2Space
158 letI : TotallyDisconnectedSpace (Multiplicative M) := e.totallyDisconnectedSpace
160 (G := Multiplicative M) with ⟨X, hXgen, hXconv⟩
161 let S : Set M := Multiplicative.toAdd '' X
162 have hpre : Multiplicative.toAdd ⁻¹' S = X := by
163 ext x
164 simp only [Equiv.preimage_image, S]
165 have hsub : (AddSubgroup.closure S).toSubgroup = Subgroup.closure X := by
166 rw [AddSubgroup.toSubgroup_closure]
167 rw [hpre]
168 have hspan : closure (((AddSubgroup.closure S : AddSubgroup M) : Set M)) = Set.univ := by
169 have htopSub : (Subgroup.closure X).topologicalClosure = ⊤ := by
170 simpa [ProCGroups.Generation.TopologicallyGenerates] using hXgen
171 have htopMul : ((AddSubgroup.closure S).toSubgroup).topologicalClosure = ⊤ := by
172 simpa [hsub] using htopSub
173 change ((AddSubgroup.closure S).topologicalClosure : Set M) = Set.univ
174 ext x
175 constructor
176 · intro _
177 simp only [Set.mem_univ]
178 · intro _
179 have hxmul : Multiplicative.ofAdd x ∈
180 (((AddSubgroup.closure S).toSubgroup).topologicalClosure :
181 Set (Multiplicative M)) := by
182 rw [htopMul]
183 simp only [Subgroup.coe_top, Set.mem_univ]
184 have hxpre :
185 x ∈ e ⁻¹' closure
186 (((AddSubgroup.closure S).toSubgroup : Subgroup (Multiplicative M)) :
187 Set (Multiplicative M)) :=
188 hxmul
189 rw [e.preimage_closure] at hxpre
190 have hpreimage :
191 Multiplicative.ofAdd ⁻¹'
192 (Multiplicative.toAdd ⁻¹'
193 (((AddSubgroup.closure S : AddSubgroup M) : Set M))) =
194 ((AddSubgroup.closure S : AddSubgroup M) : Set M) := by
195 ext y
196 rfl
197 rw [show (e ⁻¹'
198 (((AddSubgroup.closure S).toSubgroup : Subgroup (Multiplicative M)) :
199 Set (Multiplicative M))) =
200 ((AddSubgroup.closure S : AddSubgroup M) : Set M) by
201 simpa [e, multiplicativeHomeomorph] using hpreimage] at hxpre
202 exact hxpre
203 have hconv : SetConvergesToZero S := by
204 intro U hU
205 rcases profiniteModule_hasFiniteIndexSubmoduleBasis Λ M U hU with
206 ⟨N, hNopen, hNU, _⟩
207 let V : OpenSubgroup (Multiplicative M) :=
208 { toSubgroup := N.toAddSubgroup.toSubgroup
209 isOpen' := by
210 change IsOpen (Multiplicative.toAdd ⁻¹' (N : Set M))
211 exact hNopen.preimage continuous_toAdd }
212 have hsubset : S \ U ⊆ Multiplicative.toAdd '' (X \ (V : Set (Multiplicative M))) := by
213 intro y hy
214 rcases hy with ⟨hyS, hyU⟩
215 rcases hyS with ⟨x, hxX, rfl⟩
216 refine ⟨x, ⟨hxX, ?_⟩, rfl⟩
217 intro hxV
218 change Multiplicative.toAdd x ∈ N at hxV
219 exact hyU (hNU hxV)
220 exact ((hXconv V).image Multiplicative.toAdd).subset hsubset
221 exact hasGeneratingSetConvergingToZero_of_dense_addSubgroup Λ M hspan hconv
223end CompletedGroupAlgebra