Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenSubmodule
1import Mathlib.Topology.Algebra.LinearTopology
2import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.Definitions
4/-!
5# Open submodules of profinite modules
7This file constructs open submodules inside identity neighborhoods using scalar multiples of open
8additive subgroups. It proves the resulting linear topology and the finiteness and discreteness of
9open-submodule quotients.
10-/
12open scoped Topology
14namespace CompletedGroupAlgebra
16universe u v w z
18/--
19A compact Hausdorff totally disconnected additive group has arbitrarily small open additive
20subgroups at zero.
21-/
22theorem exists_openAddSubgroup_subset_open_nhds_zero
23 {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
24 [CompactSpace M] [T2Space M] [TotallyDisconnectedSpace M]
25 {U : Set M} (hUopen : IsOpen U) (h0U : (0 : M) ∈ U) :
26 ∃ H : OpenAddSubgroup M, (H : Set M) ⊆ U := by
27 rcases ((nhds_basis_clopen (0 : M)).mem_iff.mp (hUopen.mem_nhds h0U)) with
28 ⟨W, hW, hWU⟩
29 rcases IsTopologicalAddGroup.exist_openAddSubgroup_sub_clopen_nhds_of_zero hW.2 hW.1 with
30 ⟨H, hH⟩
31 exact ⟨H, hH.trans hWU⟩
33/--
34Around zero there is an open additive subgroup whose scalar multiples all land in a given open
35additive subgroup.
36-/
37theorem exists_openAddSubgroup_forall_smul_mem
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 change (lam, v) ∈ T
61 exact hWV ⟨hWuniv trivial, hH hv⟩
63/-- The submodule generated by all scalar multiples of an open additive subgroup. -/
64def submoduleGeneratedByScalarMultiples
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]⟩
81 | zero =>
82 simp only [smul_zero, zero_mem]
83 | add x y _ _ hx hy =>
84 simpa [smul_add] using AddSubgroup.add_mem _ hx hy
85 | neg x _ hx =>
86 simpa using AddSubgroup.neg_mem _ hx
88/-- The submodule generated by scalar multiples of an open additive subgroup is open. -/
89theorem submoduleGeneratedByScalarMultiples_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/--
101Bounds on every generator imply the corresponding bound on the scalar-multiple generated
102submodule.
103-/
104theorem submoduleGeneratedByScalarMultiples_subset
105 (Λ : Type u) (M : Type v) [Ring Λ] [AddCommGroup M] [Module Λ M]
106 (V A : AddSubgroup M)
107 (hVA : ∀ lam : Λ, ∀ v : M, v ∈ V → lam • v ∈ A) :
108 (submoduleGeneratedByScalarMultiples Λ M V : Set M) ⊆ (A : Set M) := by
109 intro x hx
110 change x ∈ A
111 induction hx using AddSubgroup.closure_induction with
112 | mem y hy =>
113 rcases hy with ⟨lam, v, hv, rfl⟩
114 exact hVA lam v hv
115 | zero =>
116 exact zero_mem A
117 | add x y _ _ hx hy =>
118 exact AddSubgroup.add_mem A hx hy
119 | neg x _ hx =>
120 exact AddSubgroup.neg_mem A hx
122/-- In Lemma 5.1.1(b), linear-topology part, the topology of a profinite module is linear. -/
123theorem profiniteModule_isLinearTopology
124 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
125 [TopologicalSpace M] [Module Λ M] [IsTopologicalRing Λ] [CompactSpace Λ]
126 [IsTopologicalAddGroup M] [ContinuousSMul Λ M] [CompactSpace M] [T2Space M]
127 [TotallyDisconnectedSpace M] :
128 IsLinearTopology Λ M := by
129 letI : ContinuousAdd M := inferInstance
130 rw [isLinearTopology_iff_hasBasis_open_submodule]
131 refine Filter.hasBasis_iff.mpr ?_
132 intro U
133 constructor
134 · intro hU
135 rcases mem_nhds_iff.mp hU with ⟨O, hOU, hOopen, h0O⟩
136 rcases exists_openAddSubgroup_subset_open_nhds_zero hOopen h0O with ⟨A, hAO⟩
137 rcases exists_openAddSubgroup_forall_smul_mem (Λ := Λ) A with ⟨V, hV⟩
138 let N := submoduleGeneratedByScalarMultiples Λ M V.toAddSubgroup
139 have hNopen : IsOpen (N : Set M) :=
140 submoduleGeneratedByScalarMultiples_open Λ M V
141 have hNA : (N : Set M) ⊆ (A : Set M) :=
142 submoduleGeneratedByScalarMultiples_subset Λ M V.toAddSubgroup A.toAddSubgroup hV
143 exact ⟨N, hNopen, hNA.trans (hAO.trans hOU)⟩
144 · rintro ⟨N, hNopen, hNU⟩
145 exact Filter.mem_of_superset (hNopen.mem_nhds (zero_mem N)) hNU
147/--
148An open submodule of a compact topological additive group has finite quotient. This is the
149finite-quotient step used in Lemma 5.1.1(b).
150-/
151theorem finite_quotient_of_openSubmodule
152 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
153 [TopologicalSpace M] [Module Λ M] [IsTopologicalAddGroup M] [CompactSpace M]
154 (N : Submodule Λ M) (hN : IsOpen (N : Set M)) :
155 Nonempty (Fintype (M ⧸ N)) := by
156 letI : ContinuousAdd M := inferInstance
157 haveI : Finite (M ⧸ N) :=
158 AddSubgroup.quotient_finite_of_isOpen N.toAddSubgroup hN
159 exact ⟨Fintype.ofFinite (M ⧸ N)⟩
161/-- The quotient by an open submodule is a discrete topological module. -/
162theorem quotient_openSubmodule_isDiscreteModule
163 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
164 [TopologicalSpace M] [Module Λ M] [IsTopologicalRing Λ]
165 [IsTopologicalAddGroup M] [ContinuousSMul Λ M]
166 (N : Submodule Λ M) (hN : IsOpen (N : Set M)) :
167 IsDiscreteModule Λ (M ⧸ N) := by
168 letI : ContinuousAdd M := inferInstance
169 haveI : DiscreteTopology (M ⧸ N) :=
170 QuotientAddGroup.discreteTopology (N := N.toAddSubgroup) hN
171 exact ⟨⟨inferInstance, inferInstance, inferInstance⟩, inferInstance⟩
173end CompletedGroupAlgebra