Yamaguchi Lean 4 Library
CompletedGroupAlgebra/ProfiniteModules/Basic/Generators.lean
CompletedGroupAlgebra/ProfiniteModules/Basic/Generators/Source

CompletedGroupAlgebra/ProfiniteModules/Basic/Generators.lean

1import CompletedGroupAlgebra.ProfiniteModules.Basic.FiniteQuotients
2import ProCGroups.Generation.QuotientGeneratorConvergingPairs
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/Basic/Generators.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Generating sets converging to zero
14-/
16open scoped Topology
20universe u v w z
22/-- A subset converges to zero in the book's "all but finitely many elements" sense. -/
23def SetConvergesToZero {M : Type v} [TopologicalSpace M] [Zero M] (S : Set M) : Prop :=
24 ∀ U ∈ 𝓝 (0 : M), (S \ U).Finite
26/-- A map from an arbitrary index type converges to zero along the cofinite filter. This is the
27map-level version used in Lemma 5.2.5(b). -/
28def MapConvergesToZero {S : Type u} {M : Type v} [TopologicalSpace M] [Zero M]
29 (f : S → M) : Prop :=
30 Filter.Tendsto f Filter.cofinite (𝓝 (0 : M))
32/-- A map converging to zero has image set converging to zero. -/
33theorem MapConvergesToZero.setConvergesToZero_range
34 {S : Type u} {M : Type v} [TopologicalSpace M] [Zero M] {f : S → M}
36 SetConvergesToZero (Set.range f) := by
37 intro U hU
38 have hpre : {s : S | f s ∉ U}.Finite := by
39 have hmem : {s : S | f s ∈ U} ∈ (Filter.cofinite : Filter S) := hf hU
40 simpa [Filter.mem_cofinite, Set.compl_setOf] using hmem
41 exact (hpre.image f).subset (by
42 rintro y ⟨⟨s, rfl⟩, hsU⟩
43 exact ⟨s, hsU, rfl⟩)
45/-- An injective parametrization of a set converging to zero is a map converging to zero. -/
46theorem SetConvergesToZero.mapConvergesToZero_of_injective
47 {S : Type u} {M : Type v} [TopologicalSpace M] [Zero M] {f : S → M}
48 (hfconv : SetConvergesToZero (Set.range f)) (hfinj : Function.Injective f) :
50 intro U hU
51 have hbad : ({s : S | f s ∉ U} : Set S).Finite := by
52 have hpre :
53 ({s : S | f s ∉ U} : Set S) = f ⁻¹' (Set.range f \ U) := by
54 ext s
55 simp only [Set.mem_setOf_eq, Set.preimage_diff, Set.preimage_range, Set.mem_diff, Set.mem_univ,
56 Set.mem_preimage, true_and]
57 rw [hpre]
58 exact Set.Finite.preimage (f := f) (s := Set.range f \ U) hfinj.injOn
59 (hfconv U hU)
60 simpa [Filter.mem_cofinite, Set.compl_setOf] using hbad
62/-- The inclusion of a set converging to zero, viewed as a parametrized map, converges to zero. -/
63theorem SetConvergesToZero.subtype_val
64 {M : Type v} [TopologicalSpace M] [Zero M] {S : Set M}
66 MapConvergesToZero (fun s : S => (s : M)) := by
67 have hrange : Set.range (fun s : S => (s : M)) = S := by
68 ext x
69 constructor
70 · rintro ⟨s, rfl⟩
71 exact s.2
72 · intro hx
73 exact ⟨⟨x, hx⟩, rfl⟩
74 have hRangeConv : SetConvergesToZero (Set.range fun s : S => (s : M)) := by
75 simpa [hrange] using hS
76 exact hRangeConv.mapConvergesToZero_of_injective Subtype.val_injective
78/-- A map from a discrete set converges to zero iff its zero-extension to the one-point
79compactification is continuous. -/
81 {S : Type u} {M : Type v} [TopologicalSpace S] [DiscreteTopology S]
82 [TopologicalSpace M] [Zero M] (f : S → M) :
83 Continuous (fun x : OnePoint S => x.elim 0 f) ↔ MapConvergesToZero f := by
84 rw [OnePoint.continuous_iff_from_discrete]
85 rfl
87/-- Finite subsets converge to zero in the book's "all but finitely many elements" sense. -/
89 {M : Type v} [TopologicalSpace M] [Zero M] {S : Set M} (hS : S.Finite) :
91 intro U _hU
92 exact hS.subset Set.diff_subset
94/-- A set of topological module generators converging to zero. -/
95def HasGeneratingSetConvergingToZero (Λ : Type u) (M : Type v) [Ring Λ]
96 [TopologicalSpace M] [AddCommGroup M] [Module Λ M] : Prop :=
97 ∃ S : Set M, closure (Submodule.span Λ S : Set M) = Set.univ ∧ SetConvergesToZero S
99/-- A finite dense generating set is a generating set converging to zero. This gives the
100finite-generated special case of Lemma 5.1.1(c). -/
102 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M] [AddCommGroup M]
103 [Module Λ M] {S : Set M}
104 (hgen : closure (Submodule.span Λ S : Set M) = Set.univ) (hS : S.Finite) :
106 exact ⟨S, hgen, finite_setConvergesToZero hS⟩
108/-- A dense additive generating set is also a dense module generating set. -/
110 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M] [AddCommGroup M]
111 [Module Λ M] {S : Set M}
112 (hspan : closure (((AddSubgroup.closure S : AddSubgroup M) : Set M)) = Set.univ)
113 (hconv : SetConvergesToZero S) :
115 refine ⟨S, ?_, hconv⟩
116 have hsubset : ((AddSubgroup.closure S : AddSubgroup M) : Set M) ⊆
117 ((Submodule.span Λ S : Submodule Λ M) : Set M) := by
118 intro x hx
119 have hle : AddSubgroup.closure S ≤ (Submodule.span Λ S).toAddSubgroup :=
120 (AddSubgroup.closure_le (K := (Submodule.span Λ S).toAddSubgroup)).2
121 fun y hy => Submodule.subset_span hy
122 exact hle hx
123 have hclosure :
124 closure (((AddSubgroup.closure S : AddSubgroup M) : Set M)) ⊆
125 closure (((Submodule.span Λ S : Submodule Λ M) : Set M)) :=
126 closure_mono hsubset
127 exact Set.eq_univ_of_univ_subset (by simpa [hspan] using hclosure)
129private def multiplicativeHomeomorph (M : Type*) [TopologicalSpace M] : M ≃ₜ Multiplicative M where
130 toEquiv := Multiplicative.ofAdd
131 continuous_toFun := continuous_ofAdd
132 continuous_invFun := continuous_toAdd
134/-- Lemma 5.1.1(c): every profinite module has a generating set converging to zero. -/
136 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
137 [AddCommGroup M] [TopologicalSpace M] [Module Λ M]
138 (hM : IsProfiniteModule Λ M) :
140 letI : IsTopologicalAddGroup M := hM.2.1
141 letI : ContinuousSMul Λ M := hM.2.2.1
142 letI : CompactSpace M := hM.2.2.2.1
143 letI : T2Space M := hM.2.2.2.2.1
144 letI : TotallyDisconnectedSpace M := hM.2.2.2.2.2
145 let e : M ≃ₜ Multiplicative M := multiplicativeHomeomorph M
146 letI : CompactSpace (Multiplicative M) := e.compactSpace
147 letI : T2Space (Multiplicative M) := e.t2Space
148 letI : TotallyDisconnectedSpace (Multiplicative M) := e.totallyDisconnectedSpace
149 have hG : ProCGroups.IsProfiniteGroup (Multiplicative M) :=
150 ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
151 rcases ProCGroups.Generation.exists_generatorsConvergingToOne
152 (G := Multiplicative M) hG with ⟨X, hXgen, hXconv⟩
153 let S : Set M := Multiplicative.toAdd '' X
154 have hpre : Multiplicative.toAdd ⁻¹' S = X := by
155 ext x
156 simp only [Equiv.preimage_image, S]
157 have hsub : (AddSubgroup.closure S).toSubgroup = Subgroup.closure X := by
158 rw [AddSubgroup.toSubgroup_closure]
159 rw [hpre]
160 have hspan : closure (((AddSubgroup.closure S : AddSubgroup M) : Set M)) = Set.univ := by
161 have htopSub : (Subgroup.closure X).topologicalClosure = ⊤ := by
163 have htopMul : ((AddSubgroup.closure S).toSubgroup).topologicalClosure = ⊤ := by
164 simpa [hsub] using htopSub
165 change ((AddSubgroup.closure S).topologicalClosure : Set M) = Set.univ
166 ext x
167 constructor
168 · intro _
169 simp only [Set.mem_univ]
170 · intro _
171 have hxmul : Multiplicative.ofAdd x ∈
172 (((AddSubgroup.closure S).toSubgroup).topologicalClosure :
173 Set (Multiplicative M)) := by
174 rw [htopMul]
175 simp only [Subgroup.coe_top, Set.mem_univ]
176 simpa [AddSubgroup.topologicalClosure_coe] using hxmul
177 have hconv : SetConvergesToZero S := by
178 intro U hU
180 ⟨N, hNopen, hNU, _⟩
181 let V : OpenSubgroup (Multiplicative M) :=
182 { toSubgroup := N.toAddSubgroup.toSubgroup
183 isOpen' := by
184 simpa using hNopen }
185 have hsubset : S \ U ⊆ Multiplicative.toAdd '' (X \ (V : Set (Multiplicative M))) := by
186 intro y hy
187 rcases hy with ⟨hyS, hyU⟩
188 rcases hyS with ⟨x, hxX, rfl⟩
189 refine ⟨x, ⟨hxX, ?_⟩, rfl⟩
190 intro hxV
191 exact hyU (hNU (by simpa [V] using hxV))
192 exact ((hXconv V).image Multiplicative.toAdd).subset hsubset