CompletedGroupAlgebra/ProfiniteModules/Basic/OpenSubmodule.lean
1import Mathlib.Topology.Algebra.LinearTopology
2import CompletedGroupAlgebra.ProfiniteModules.Basic.Definitions
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/Basic/OpenSubmodule.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Open submodules of profinite modules
14-/
16open scoped Topology
18namespace CompletedGroupAlgebra
20universe u v w z
22/-- A compact Hausdorff totally disconnected additive group has arbitrarily small open additive
23subgroups at zero. -/
25 {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
26 [CompactSpace M] [T2Space M] [TotallyDisconnectedSpace M]
27 {U : Set M} (hUopen : IsOpen U) (h0U : (0 : M) ∈ U) :
28 ∃ H : OpenAddSubgroup M, (H : Set M) ⊆ U := by
29 rcases ((nhds_basis_clopen (0 : M)).mem_iff.mp (hUopen.mem_nhds h0U)) with
30 ⟨W, hW, hWU⟩
31 rcases IsTopologicalAddGroup.exist_openAddSubgroup_sub_clopen_nhds_of_zero hW.2 hW.1 with
32 ⟨H, hH⟩
33 exact ⟨H, hH.trans hWU⟩
35/-- Around zero there is an open additive subgroup whose scalar multiples all land in a given
36open additive subgroup. -/
38 {Λ : Type u} {M : Type v} [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
39 [TopologicalSpace M] [Module Λ M] [CompactSpace Λ] [IsTopologicalAddGroup M]
40 [CompactSpace M] [T2Space M] [TotallyDisconnectedSpace M] [ContinuousSMul Λ M]
41 (A : OpenAddSubgroup M) :
42 ∃ V : OpenAddSubgroup M, ∀ lam : Λ, ∀ v : M, v ∈ V → lam • v ∈ A := by
43 let T : Set (Λ × M) := {p | p.1 • p.2 ∈ (A : Set M)}
44 have hTopen : IsOpen T := by
45 exact (OpenAddSubgroup.isOpen A).preimage continuous_smul
46 have hcontains : (Set.univ : Set Λ) ×ˢ ({0} : Set M) ⊆ T := by
47 rintro ⟨lam, m⟩ ⟨_hlam, hm⟩
48 rw [Set.mem_singleton_iff] at hm
49 change m = 0 at hm
50 change lam • m ∈ A
51 rw [hm]
52 simp only [smul_zero, zero_mem]
53 rcases generalized_tube_lemma (s := (Set.univ : Set Λ)) isCompact_univ
54 (t := ({0} : Set M)) isCompact_singleton hTopen hcontains with
55 ⟨_W, V, _hWopen, hVopen, hWuniv, h0V, hWV⟩
56 have hzeroV : (0 : M) ∈ V := h0V (by simp only [Set.mem_singleton_iff])
57 rcases exists_openAddSubgroup_subset_open_nhds_zero hVopen hzeroV with ⟨H, hH⟩
58 refine ⟨H, ?_⟩
59 intro lam v hv
60 show (lam, v) ∈ T
61 exact hWV ⟨hWuniv trivial, hH hv⟩
63/-- The submodule generated by all scalar multiples of an open additive subgroup. -/
65 (Λ : Type u) (M : Type v) [Ring Λ] [AddCommGroup M] [Module Λ M]
66 (V : AddSubgroup M) : Submodule Λ M where
67 carrier := AddSubgroup.closure {x : M | ∃ lam : Λ, ∃ v : M, v ∈ V ∧ x = lam • v}
68 zero_mem' := by
69 exact AddSubgroup.zero_mem _
70 add_mem' := by
71 intro x y hx hy
72 exact AddSubgroup.add_mem _ hx hy
73 smul_mem' := by
74 intro lam x hx
75 change lam • x ∈
76 AddSubgroup.closure {x : M | ∃ mu : Λ, ∃ v : M, v ∈ V ∧ x = mu • v}
77 induction hx using AddSubgroup.closure_induction with
78 | mem y hy =>
79 rcases hy with ⟨mu, v, hv, rfl⟩
80 exact AddSubgroup.subset_closure ⟨lam * mu, v, hv, by simp only [mul_smul]⟩
82 simp only [smul_zero, zero_mem]
84 simpa [smul_add] using AddSubgroup.add_mem _ hx hy
86 simpa using AddSubgroup.neg_mem _ hx
88/-- The submodule generated by scalar multiples of an open additive subgroup is open. -/
90 (Λ : Type u) (M : Type v) [Ring Λ] [AddCommGroup M] [TopologicalSpace M]
91 [Module Λ M] [ContinuousAdd M] (V : OpenAddSubgroup M) :
92 IsOpen (submoduleGeneratedByScalarMultiples Λ M V : Set M) := by
93 let N := submoduleGeneratedByScalarMultiples Λ M V
94 have hVsub : (V : Set M) ⊆ (N : Set M) := by
95 intro v hv
96 exact AddSubgroup.subset_closure ⟨1, v, hv, by simp only [one_smul]⟩
97 exact N.toAddSubgroup.isOpen_of_mem_nhds
98 (Filter.mem_of_superset ((OpenAddSubgroup.isOpen V).mem_nhds (zero_mem V)) hVsub)
100/-- To bound the scalar-multiple generated submodule, it suffices to bound each generator. -/
102 (Λ : Type u) (M : Type v) [Ring Λ] [AddCommGroup M] [Module Λ M]
103 (V A : AddSubgroup M)
104 (hVA : ∀ lam : Λ, ∀ v : M, v ∈ V → lam • v ∈ A) :
105 (submoduleGeneratedByScalarMultiples Λ M V : Set M) ⊆ (A : Set M) := by
106 intro x hx
107 change x ∈ A
108 induction hx using AddSubgroup.closure_induction with
109 | mem y hy =>
110 rcases hy with ⟨lam, v, hv, rfl⟩
111 exact hVA lam v hv
113 exact zero_mem A
115 exact AddSubgroup.add_mem A hx hy
117 exact AddSubgroup.neg_mem A hx
119/-- Lemma 5.1.1(b), linear-topology part: the topology of a profinite module is linear.
122neighborhood; compactness of the coefficient ring gives a smaller open additive subgroup whose
123scalar multiples stay inside it; the additive subgroup generated by all scalar multiples is then
124an open submodule. -/
126 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
127 [TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M) :
128 IsLinearTopology Λ M := by
129 letI : IsTopologicalRing Λ := hM.1.1
130 letI : CompactSpace Λ := hM.1.2.1
131 letI : IsTopologicalAddGroup M := hM.2.1
132 letI : ContinuousAdd M := inferInstance
133 letI : ContinuousSMul Λ M := hM.2.2.1
134 letI : CompactSpace M := hM.2.2.2.1
135 letI : T2Space M := hM.2.2.2.2.1
136 letI : TotallyDisconnectedSpace M := hM.2.2.2.2.2
137 rw [isLinearTopology_iff_hasBasis_open_submodule]
138 refine Filter.hasBasis_iff.mpr ?_
139 intro U
140 constructor
141 · intro hU
142 rcases mem_nhds_iff.mp hU with ⟨O, hOU, hOopen, h0O⟩
143 rcases exists_openAddSubgroup_subset_open_nhds_zero hOopen h0O with ⟨A, hAO⟩
144 rcases exists_openAddSubgroup_forall_smul_mem (Λ := Λ) A with ⟨V, hV⟩
145 let N := submoduleGeneratedByScalarMultiples Λ M V.toAddSubgroup
146 have hNopen : IsOpen (N : Set M) :=
148 have hNA : (N : Set M) ⊆ (A : Set M) :=
149 submoduleGeneratedByScalarMultiples_subset Λ M V.toAddSubgroup A.toAddSubgroup hV
150 exact ⟨N, hNopen, hNA.trans (hAO.trans hOU)⟩
151 · rintro ⟨N, hNopen, hNU⟩
152 exact Filter.mem_of_superset (hNopen.mem_nhds (zero_mem N)) hNU
154/-- An open submodule of a compact topological additive group has finite quotient. This is the
157 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
158 [TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M)
159 (N : Submodule Λ M) (hN : IsOpen (N : Set M)) :
160 Nonempty (Fintype (M ⧸ N)) := by
161 letI : IsTopologicalAddGroup M := hM.2.1
162 letI : ContinuousAdd M := inferInstance
163 letI : CompactSpace M := hM.2.2.2.1
164 haveI : Finite (M ⧸ N) :=
165 AddSubgroup.quotient_finite_of_isOpen N.toAddSubgroup hN
166 exact ⟨Fintype.ofFinite (M ⧸ N)⟩
168/-- The quotient by an open submodule is a discrete topological module. -/
170 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
171 [TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M)
172 (N : Submodule Λ M) (hN : IsOpen (N : Set M)) :
173 IsDiscreteModule Λ (M ⧸ N) := by
174 letI : IsTopologicalRing Λ := hM.1.1
175 letI : IsTopologicalAddGroup M := hM.2.1
176 letI : ContinuousAdd M := inferInstance
177 letI : ContinuousSMul Λ M := hM.2.2.1
178 haveI : DiscreteTopology (M ⧸ N) :=
179 QuotientAddGroup.discreteTopology (N := N.toAddSubgroup) hN
180 exact ⟨⟨hM.1.1, inferInstance, inferInstance⟩, inferInstance⟩
182/-- Open submodule quotients are finite discrete modules. -/
184 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
185 [TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M)
186 (N : Submodule Λ M) (hN : IsOpen (N : Set M)) :
187 IsDiscreteModule Λ (M ⧸ N) ∧ Nonempty (Fintype (M ⧸ N)) :=
188 ⟨quotient_openSubmodule_isDiscreteModule Λ M hM N hN,
189 finite_quotient_of_openSubmodule Λ M hM N hN⟩