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

CompletedGroupAlgebra/ProfiniteModules/Basic/FiniteQuotients.lean

1import CompletedGroupAlgebra.ProfiniteModules.Basic.OpenSubmodule
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/Basic/FiniteQuotients.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finite quotient bases for profinite modules
13-/
15open scoped Topology
19universe u v w z
21/-- Lemma 5.1.1(b), linear-topology interface: a profinite module with a linear topology has a
22basis of open finite-index submodules at zero. -/
24 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
25 [TopologicalSpace M] [Module Λ M] [IsLinearTopology Λ M]
26 (hM : IsProfiniteModule Λ M) :
28 letI : IsTopologicalAddGroup M := hM.2.1
29 letI : ContinuousAdd M := inferInstance
30 intro U hU
31 rcases ((IsLinearTopology.hasBasis_open_submodule Λ).mem_iff.mp hU) with
32 ⟨N, hNopen, hNU⟩
33 exact ⟨N, hNopen, hNU,
36/-- Lemma 5.1.1(b), inverse-limit formulation under the same linear-topology hypothesis. -/
38 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
39 [TopologicalSpace M] [Module Λ M] [IsLinearTopology Λ M]
40 (hM : IsProfiniteModule Λ M) :
45/-- Lemma 5.1.1(b): finite-index submodules form a neighborhood basis at zero in a profinite
46module. -/
48 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
49 [TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M) :
51 letI : IsLinearTopology Λ M := profiniteModule_isLinearTopology Λ M hM
54/-- Open submodule quotients separate points of a profinite module. -/
56 {R : Type u} (N : Type v) [Ring R] [TopologicalSpace R]
57 [AddCommGroup N] [TopologicalSpace N] [Module R N]
58 (hN : IsProfiniteModule R N) {x y : N}
59 (h : ∀ W : Submodule R N, IsOpen (W : Set N) → Submodule.mkQ W x = Submodule.mkQ W y) :
60 x = y := by
61 by_contra hxy
62 letI : T2Space N := hN.2.2.2.2.1
63 let O : Set N := ({x - y} : Set N)ᶜ
64 have hd0 : x - y ≠ 0 := by
65 intro hd
66 exact hxy (sub_eq_zero.mp hd)
67 have hOopen : IsOpen O := isClosed_singleton.isOpen_compl
68 have h0O : (0 : N) ∈ O := by
69 change (0 : N) ≠ x - y
70 exact hd0.symm
71 rcases profiniteModule_hasFiniteIndexSubmoduleBasis R N hN O (hOopen.mem_nhds h0O) with
72 ⟨W, hWopen, hWO, _hfinite⟩
73 have hq := h W hWopen
74 rw [Submodule.mkQ_apply, Submodule.mkQ_apply] at hq
75 have hdiff : x - y ∈ W := (Submodule.Quotient.eq W).1 hq
76 have hdO : x - y ∈ O := hWO hdiff
77 exact hdO (by simp only [Set.mem_singleton_iff])
79/-- Open submodules of a profinite module. -/
81 (R : Type u) (N : Type v) [Ring R] [AddCommGroup N] [Module R N]
82 [TopologicalSpace N] : Type _ :=
83 {W : Submodule R N // IsOpen (W : Set N)}
85/-- Open submodule quotients detect continuity of maps into a profinite module. -/
87 {R : Type u} (N : Type v) [Ring R] [TopologicalSpace R]
88 [AddCommGroup N] [TopologicalSpace N] [Module R N]
90 {Y : Type z} [TopologicalSpace Y] {F : Y → N}
91 (hF : ∀ W : Submodule R N, IsOpen (W : Set N) →
92 Continuous fun y : Y => Submodule.mkQ W (F y)) :
93 Continuous F := by
94 letI : IsTopologicalAddGroup N := hN.2.1
95 letI : ContinuousAdd N := inferInstance
96 rw [continuous_iff_continuousAt]
97 intro y
98 rw [continuousAt_def]
99 intro A hA
100 rcases mem_nhds_iff.mp hA with ⟨O, hOA, hOopen, hFO⟩
101 let U0 : Set N := {z | F y + z ∈ O}
102 have hU0 : U0 ∈ 𝓝 (0 : N) := by
103 apply IsOpen.mem_nhds
104 · exact hOopen.preimage (continuous_const.add continuous_id)
105 · simp only [Set.mem_setOf_eq, add_zero, hFO, U0]
107 ⟨W, hWopen, hWU, _hfinite⟩
108 let hdisc : IsDiscreteModule R (N ⧸ W) :=
110 letI : DiscreteTopology (N ⧸ W) := hdisc.2
111 let q : Y → N ⧸ W := fun z => Submodule.mkQ W (F z)
112 let B : Set (N ⧸ W) := {Submodule.mkQ W (F y)}
113 have hqcont : Continuous q := hF W hWopen
114 have hpreOpen : IsOpen (q ⁻¹' B) := (isOpen_discrete B).preimage hqcont
115 have hypre : y ∈ q ⁻¹' B := by
116 simp only [Submodule.mkQ_apply, Set.mem_preimage, Set.mem_singleton_iff, q, B]
117 refine Filter.mem_of_superset (hpreOpen.mem_nhds hypre) ?_
118 intro z hz
119 apply hOA
120 have hquot : Submodule.mkQ W (F z) = Submodule.mkQ W (F y) := by
121 simpa [q, B] using hz
122 rw [Submodule.mkQ_apply, Submodule.mkQ_apply] at hquot
123 have hdiff : F z - F y ∈ W := (Submodule.Quotient.eq W).1 hquot
124 have hU : F z - F y ∈ U0 := hWU hdiff
125 change F y + (F z - F y) ∈ O at hU
126 simpa [sub_eq_add_neg, add_assoc, add_comm, add_left_comm] using hU
128/-- A finite family of open submodules has an open submodule contained in all of them. -/
130 {R : Type u} (N : Type v) [Ring R] [AddCommGroup N] [TopologicalSpace N] [Module R N]
131 (s : Finset (ProfiniteModuleOpenSubmodule (R := R) N)) :
132 ∃ K : ProfiniteModuleOpenSubmodule (R := R) N,
133 ∀ W ∈ s, K.1 ≤ W.1 := by
134 classical
135 refine Finset.induction_on s ?empty ?insert
136 · refine ⟨⟨⊤, isOpen_univ⟩, ?_⟩
137 simp only [Finset.notMem_empty, top_le_iff, IsEmpty.forall_iff, implies_true]
138 · intro W s hWs ih
139 rcases ih with ⟨K, hK⟩
140 refine ⟨⟨K.1 ⊓ W.1, K.2.inter W.2⟩, ?_⟩
141 intro V hV
142 rw [Finset.mem_insert] at hV
143 rcases hV with hVW | hVs
144 · subst V
145 exact inf_le_right
146 · exact inf_le_left.trans (hK V hVs)
148/-- The quotient of a profinite module by a closed submodule is profinite. -/
150 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
151 [TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M)
152 (K : Submodule Λ M) (hK : IsClosed (K : Set M)) :
153 IsProfiniteModule Λ (M ⧸ K) := by
154 classical
155 letI : IsTopologicalRing Λ := hM.1.1
156 letI : IsTopologicalAddGroup M := hM.2.1
157 letI : ContinuousAdd M := inferInstance
158 letI : ContinuousSMul Λ M := hM.2.2.1
159 letI : CompactSpace M := hM.2.2.2.1
160 letI : T2Space M := hM.2.2.2.2.1
161 letI : TotallyDisconnectedSpace M := hM.2.2.2.2.2
162 letI : IsClosed (K : Set M) := hK
163 letI : IsTopologicalAddGroup (M ⧸ K) := Submodule.topologicalAddGroup_quotient K
164 letI : ContinuousAdd (M ⧸ K) := inferInstance
165 letI : ContinuousSMul Λ (M ⧸ K) := Submodule.continuousSMul_quotient K
166 letI : CompactSpace (M ⧸ K) := Quotient.compactSpace
167 letI : T3Space (M ⧸ K) := Submodule.t3_quotient_of_isClosed K
168 letI : T2Space (M ⧸ K) := inferInstance
169 have htotSep : TotallySeparatedSpace (M ⧸ K) := by
170 rw [totallySeparatedSpace_iff_exists_isClopen]
171 intro a
172 refine Submodule.Quotient.induction_on K a ?_
173 intro x b
174 refine Submodule.Quotient.induction_on K b ?_
175 intro y hab
176 have hxyK : x - y ∉ K := by
177 intro hxy
178 exact hab ((Submodule.Quotient.eq K).2 hxy)
179 let O : Set M := {z | x - y - z ∉ K}
180 have hOopen : IsOpen O := by
181 exact hK.isOpen_compl.preimage ((continuous_const.sub continuous_const).sub continuous_id)
182 have h0O : (0 : M) ∈ O := by
183 simpa [O] using hxyK
185 (hOopen.mem_nhds h0O) with
186 ⟨W, hWopen, hWO, _hWfinite⟩
187 let H : Submodule Λ M := K ⊔ W
188 have hHopen : IsOpen (H : Set M) := by
189 have hWsubH : (W : Set M) ⊆ (H : Set M) := fun z hz =>
190 Submodule.mem_sup_right hz
191 exact H.toAddSubgroup.isOpen_of_mem_nhds
192 (Filter.mem_of_superset (hWopen.mem_nhds (zero_mem W)) hWsubH)
193 have hxyH : x - y ∉ H := by
194 intro hxyH
195 rcases (Submodule.mem_sup.1 hxyH) with ⟨k, hk, w, hw, hkw⟩
196 have hwO : w ∈ O := hWO hw
197 have hxysub : x - y - w = k := by
198 rw [← hkw]
199 abel
200 exact hwO (by simpa [hxysub] using hk)
201 let Q : Submodule Λ (M ⧸ K) := Submodule.map K.mkQ H
202 have hQopen : IsOpen (Q : Set (M ⧸ K)) := by
203 rw [Submodule.map_coe]
204 exact K.isOpenMap_mkQ (H : Set M) hHopen
205 have hQclosed : IsClosed (Q : Set (M ⧸ K)) :=
206 AddSubgroup.isClosed_of_isOpen Q.toAddSubgroup hQopen
207 have hmk_mem_Q_iff : ∀ z : M, Submodule.Quotient.mk z ∈ Q ↔ z ∈ H := by
208 intro z
209 constructor
210 · intro hz
211 rcases (Submodule.mem_map.1 hz) with ⟨h, hh, hhz⟩
212 have hdiff : h - z ∈ K := (Submodule.Quotient.eq K).1 hhz
213 have hdiffH : h - z ∈ H := Submodule.mem_sup_left hdiff
214 have hzH : h - (h - z) ∈ H := H.sub_mem hh hdiffH
215 simpa using hzH
216 · intro hz
217 exact Submodule.mem_map.2 ⟨z, hz, rfl⟩
218 let C : Set (M ⧸ K) := {q | q - Submodule.Quotient.mk x ∈ Q}
219 have hCclosed : IsClosed C :=
220 hQclosed.preimage (continuous_id.sub continuous_const)
221 have hCopen : IsOpen C :=
222 hQopen.preimage (continuous_id.sub continuous_const)
223 refine ⟨C, ⟨hCclosed, hCopen⟩, ?_, ?_⟩
224 · simp only [Set.mem_setOf_eq, sub_self, zero_mem, C]
225 · intro hyC
226 have hyxQ : Submodule.Quotient.mk (y - x) ∈ Q := by
227 simpa [C] using hyC
228 have hyxH : y - x ∈ H := (hmk_mem_Q_iff (y - x)).1 hyxQ
229 have hxyH' : x - y ∈ H := by
230 simpa using H.neg_mem hyxH
231 exact hxyH hxyH'
232 letI : TotallySeparatedSpace (M ⧸ K) := htotSep
233 letI : TotallyDisconnectedSpace (M ⧸ K) := inferInstance
234 exact ⟨hM.1, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance⟩
236/-- Strengthened finite quotient basis: the quotients can be used as finite discrete modules. -/
238 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
239 [TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M) :
240 ∀ U ∈ 𝓝 (0 : M), ∃ N : Submodule Λ M,
241 IsOpen (N : Set M) ∧ (N : Set M) ⊆ U ∧
242 IsDiscreteModule Λ (M ⧸ N) ∧ Nonempty (Fintype (M ⧸ N)) := by
243 intro U hU
245 ⟨N, hNopen, hNU, _hfinite⟩
246 exact ⟨N, hNopen, hNU, quotient_openSubmodule_isDiscreteModule Λ M hM N hNopen,
249/-- Lemma 5.1.1(b): a profinite module is the inverse limit of its finite quotient modules, in the
250finite-index-basis formulation used by this file. -/
252 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
253 [TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M) :