CompletedGroupAlgebra/UniversalProperty/ProfiniteModule.lean
1import CompletedGroupAlgebra.UniversalProperty.OpenSubmoduleQuotient
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/UniversalProperty/ProfiniteModule.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14This module upgrades finite-discrete and open-quotient lifting results to the universal property for profinite target modules.
15-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
26open ProCGroups.Completion
28universe u v w
30variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
31variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33/-- The closed fiber in a profinite target determined by the quotient-valued extension modulo
36 (hG : ProCGroups.IsProfiniteGroup G)
37 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
38 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
39 (x : Carrier R G)
40 (W : ProfiniteModuleOpenSubmodule (R := R) N) : Set N :=
41 {y | Submodule.mkQ W.1 y =
43 (R := R) (G := G) hG N hN f hf W.1 W.2 x}
45/-- The quotient fiber attached to an open submodule is closed. -/
47 (hG : ProCGroups.IsProfiniteGroup G)
48 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
49 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
50 (x : Carrier R G)
51 (W : ProfiniteModuleOpenSubmodule (R := R) N) :
52 IsClosed (completedGroupAlgebraLiftFiberSet
53 (R := R) (G := G) hG N hN f hf x W) := by
54 let hdisc : IsDiscreteModule R (N ⧸ W.1) :=
55 quotient_openSubmodule_isDiscreteModule R N hN W.1 W.2
56 letI : DiscreteTopology (N ⧸ W.1) := hdisc.2
57 have hqcont : Continuous (Submodule.mkQ W.1 : N → N ⧸ W.1) := by
58 change Continuous (Submodule.Quotient.mk (p := W.1))
59 exact continuous_quotient_mk'
60 change IsClosed ((Submodule.mkQ W.1 : N → N ⧸ W.1) ⁻¹'
62 (R := R) (G := G) hG N hN f hf W.1 W.2 x} : Set (N ⧸ W.1)))
63 exact (isClosed_discrete _).preimage hqcont
65/-- Finite intersection property for the fibers used to assemble the profinite-target lift. -/
67 (hG : ProCGroups.IsProfiniteGroup G)
68 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
69 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
70 (x : Carrier R G)
71 (s : Finset (ProfiniteModuleOpenSubmodule (R := R) N)) :
72 (⋂ W ∈ s, completedGroupAlgebraLiftFiberSet
73 (R := R) (G := G) hG N hN f hf x W).Nonempty := by
74 classical
75 rcases exists_openSubmodule_le_finset (R := R) N s with ⟨K, hK⟩
76 rcases Submodule.mkQ_surjective K.1
78 (R := R) (G := G) hG N hN f hf K.1 K.2 x) with
79 ⟨z, hz⟩
80 refine ⟨z, ?_⟩
81 simp only [Set.mem_iInter]
82 intro W hWs
83 dsimp [completedGroupAlgebraLiftFiberSet]
84 calc
85 Submodule.mkQ W.1 z = Submodule.factor (hK W hWs) (Submodule.mkQ K.1 z) := by
86 rw [Submodule.factor_mk]
87 _ = Submodule.factor (hK W hWs)
89 (R := R) (G := G) hG N hN f hf K.1 K.2 x) := by
90 rw [hz]
92 (R := R) (G := G) hG N hN f hf W.1 W.2 x := by
94 (R := R) (G := G) hG N hN f hf (hK W hWs) K.2 W.2 x
96/-- Compactness of the profinite target gives a simultaneous lift of the compatible quotient
97values. -/
99 (hG : ProCGroups.IsProfiniteGroup G)
100 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
101 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
102 (x : Carrier R G) :
103 (⋂ W : ProfiniteModuleOpenSubmodule (R := R) N,
105 (R := R) (G := G) hG N hN f hf x W).Nonempty := by
106 letI : CompactSpace N := hN.2.2.2.1
107 exact CompactSpace.iInter_nonempty
108 (t := fun W : ProfiniteModuleOpenSubmodule (R := R) N =>
110 (R := R) (G := G) hG N hN f hf x W)
112 (R := R) (G := G) hG N hN f hf x W)
114 (R := R) (G := G) hG N hN f hf x s)
116/-- The assembled pointwise lift from `[[RG]]` to a profinite target module. -/
118 (hG : ProCGroups.IsProfiniteGroup G)
119 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
120 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f) :
121 Carrier R G → N :=
122 fun x => Classical.choose
124 (R := R) (G := G) hG N hN f hf x)
126/-- The assembled point maps to the prescribed quotient-valued extension modulo every open
127submodule. -/
129 (hG : ProCGroups.IsProfiniteGroup G)
130 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
131 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
132 (W : ProfiniteModuleOpenSubmodule (R := R) N)
133 (x : Carrier R G) :
134 Submodule.mkQ W.1
136 (R := R) (G := G) hG N hN f hf x) =
138 (R := R) (G := G) hG N hN f hf W.1 W.2 x := by
139 have hmem := Classical.choose_spec
141 (R := R) (G := G) hG N hN f hf x)
142 exact (Set.mem_iInter.1 hmem W : _)
144/-- The assembled lift has the prescribed values on the completed group-like elements. -/
145@[simp]
147 (hG : ProCGroups.IsProfiniteGroup G)
148 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
149 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
150 (g : G) :
152 (R := R) (G := G) hG N hN f hf (completedGroupAlgebraOf R G g) = f g := by
153 apply profiniteModule_ext_of_openSubmoduleQuotients (R := R) N hN
154 intro W hW
156 (R := R) (G := G) hG N hN f hf ⟨W, hW⟩,
159/-- Additivity of the assembled profinite-target lift, checked after all open-submodule
160quotients. -/
162 (hG : ProCGroups.IsProfiniteGroup G)
163 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
164 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
165 (x y : Carrier R G) :
167 (R := R) (G := G) hG N hN f hf (x + y) =
169 (R := R) (G := G) hG N hN f hf x +
171 (R := R) (G := G) hG N hN f hf y := by
172 apply profiniteModule_ext_of_openSubmoduleQuotients (R := R) N hN
173 intro W hW
175 (R := R) (G := G) hG N hN f hf ⟨W, hW⟩,
178 (R := R) (G := G) hG N hN f hf ⟨W, hW⟩ x,
180 (R := R) (G := G) hG N hN f hf ⟨W, hW⟩ y]
181 rfl
183/-- Scalar compatibility of the assembled profinite-target lift, checked after all
184open-submodule quotients. -/
186 (hG : ProCGroups.IsProfiniteGroup G)
187 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
188 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
189 (r : R) (x : Carrier R G) :
191 (R := R) (G := G) hG N hN f hf (r • x) =
193 (R := R) (G := G) hG N hN f hf x := by
194 apply profiniteModule_ext_of_openSubmoduleQuotients (R := R) N hN
195 intro W hW
197 (R := R) (G := G) hG N hN f hf ⟨W, hW⟩,
200 (R := R) (G := G) hG N hN f hf ⟨W, hW⟩ x]
201 rfl
203/-- Existence half of Lemma 5.3.5(d): a continuous map from the profinite group `G` to a
204profinite `R`-module extends to a continuous `R`-linear map out of `[[RG]]`. -/
206 (hG : ProCGroups.IsProfiniteGroup G)
207 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
208 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f) :
209 Carrier R G →L[R] N where
210 toFun := completedGroupAlgebraLiftToProfiniteModuleFun (R := R) (G := G) hG N hN f hf
211 map_add' := completedGroupAlgebraLiftToProfiniteModuleFun_add
212 (R := R) (G := G) hG N hN f hf
213 map_smul' := completedGroupAlgebraLiftToProfiniteModuleFun_smul
214 (R := R) (G := G) hG N hN f hf
215 cont := by
216 apply continuous_of_forall_openSubmodule_quotient_continuous (R := R) N hN
217 intro W hW
218 have hEq : (fun x : Carrier R G =>
219 Submodule.mkQ W
221 (R := R) (G := G) hG N hN f hf x)) =
223 (R := R) (G := G) hG N hN f hf W hW := by
224 funext x
226 (R := R) (G := G) hG N hN f hf ⟨W, hW⟩ x
227 rw [hEq]
229 (R := R) (G := G) hG N hN f hf W hW).continuous
231/-- The profinite-target lift has the prescribed value on completed group-like elements. -/
232@[simp]
234 (hG : ProCGroups.IsProfiniteGroup G)
235 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
236 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
237 (g : G) :
239 (R := R) (G := G) hG N hN f hf (completedGroupAlgebraOf R G g) = f g :=
241 (R := R) (G := G) hG N hN f hf g
243/-- Full universal property in Lemma 5.3.5(d). -/
245 (hG : ProCGroups.IsProfiniteGroup G)
246 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
247 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f) :
248 ∃! F : Carrier R G →L[R] N,
249 ∀ g : G, F (completedGroupAlgebraOf R G g) = f g := by
250 letI : T2Space N := hN.2.2.2.2.1
251 let F := completedGroupAlgebraLiftToProfiniteModule (R := R) (G := G) hG N hN f hf
252 refine ⟨F, ?_, ?_⟩
253 · intro g
255 (R := R) (G := G) hG N hN f hf g
256 · intro K hK
257 apply completedGroupAlgebraContinuousLinearMap_ext_of_basis (R := R) (G := G) hG
258 intro g
261/-- Book Lemma 5.3.5(d): `[[RG]]` is the free profinite `R`-module on the profinite space
262`G`, with basis map `g ↦ g` inside the completed group algebra. -/
264 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
265 IsFreeProfiniteModuleOn R G (Carrier R G) (completedGroupAlgebraOf R G) := by
266 refine ⟨hR, completedGroupAlgebra_isProfiniteModule (R := R) (G := G) hR,
267 continuous_completedGroupAlgebraOf (R := R) (G := G),
268 completedGroupAlgebraOf_dense_span (R := R) (G := G) hG, ?_⟩
269 intro N _addN _topN _modN hN f hf
271 (R := R) (G := G) hG N hN f hf
272end