CompletedGroupAlgebra/Basic/AllFinite/Topology.lean
1import CompletedGroupAlgebra.Basic.AllFinite.Projections
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Basic/AllFinite/Topology.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Topology and profiniteness
14This module equips the all-finite completed group algebra with its inverse-limit topology and proves the resulting profiniteness properties.
15-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
26open ProCGroups.Completion
28universe u v w
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
33/-- Each finite stage `R[G/U]` is a topological ring for its product topology. -/
34theorem completedGroupAlgebraStage_isTopologicalRing (U : CompletedGroupAlgebraIndex G) :
35 IsTopologicalRing ((completedGroupAlgebraSystem R G).X U) := by
39instance instContinuousSMulCompletedGroupAlgebra :
40 ContinuousSMul R (Carrier R G) where
41 continuous_smul := by
42 let A := Carrier R G
43 letI : ∀ U : CompletedGroupAlgebraIndex G, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
44 fun U => (completedGroupAlgebraSystem R G).topologicalSpace U
45 have hval : Continuous fun p : R × A =>
46 fun U : CompletedGroupAlgebraIndex G =>
47 (show CompletedGroupAlgebraStage R G U from (p.1 • p.2).1 U) := by
48 change Continuous fun p : R × A =>
49 fun U : CompletedGroupAlgebraIndex G =>
50 p.1 • completedGroupAlgebraProjection R G U p.2
51 apply continuous_pi
52 intro U
53 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
54 (completedGroupAlgebraSystem R G).topologicalSpace U
55 letI : ContinuousSMul R (CompletedGroupAlgebraStage R G U) :=
57 exact continuous_fst.smul
58 (((completedGroupAlgebraSystem R G).continuous_projection U).comp continuous_snd)
59 exact Continuous.subtype_mk hval fun p => (p.1 • p.2).2
61instance instContinuousAddCompletedGroupAlgebra :
62 ContinuousAdd (Carrier R G) where
63 continuous_add := by
64 let A := Carrier R G
65 letI : ∀ U : CompletedGroupAlgebraIndex G, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
66 fun U => (completedGroupAlgebraSystem R G).topologicalSpace U
67 have hval : Continuous fun p : A × A =>
68 ((p.1 + p.2 : A) :
69 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) := by
70 change Continuous fun p : A × A =>
71 fun U : CompletedGroupAlgebraIndex G =>
72 completedGroupAlgebraProjection R G U p.1 +
73 completedGroupAlgebraProjection R G U p.2
74 apply continuous_pi
75 intro U
76 letI : IsTopologicalRing ((completedGroupAlgebraSystem R G).X U) :=
77 completedGroupAlgebraStage_isTopologicalRing (R := R) (G := G) U
78 exact (((completedGroupAlgebraSystem R G).continuous_projection U).comp continuous_fst).add
79 (((completedGroupAlgebraSystem R G).continuous_projection U).comp continuous_snd)
80 exact Continuous.subtype_mk hval fun p => (p.1 + p.2).2
82instance instContinuousNegCompletedGroupAlgebra :
83 ContinuousNeg (Carrier R G) where
84 continuous_neg := by
85 let A := Carrier R G
86 letI : ∀ U : CompletedGroupAlgebraIndex G, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
87 fun U => (completedGroupAlgebraSystem R G).topologicalSpace U
88 have hval : Continuous fun x : A =>
89 ((-x : A) :
90 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) := by
91 change Continuous fun x : A =>
92 fun U : CompletedGroupAlgebraIndex G => -completedGroupAlgebraProjection R G U x
93 apply continuous_pi
94 intro U
95 letI : IsTopologicalRing ((completedGroupAlgebraSystem R G).X U) :=
96 completedGroupAlgebraStage_isTopologicalRing (R := R) (G := G) U
97 exact ((completedGroupAlgebraSystem R G).continuous_projection U).neg
98 exact Continuous.subtype_mk hval fun x => (-x).2
100instance instContinuousMulCompletedGroupAlgebra :
101 ContinuousMul (Carrier R G) where
102 continuous_mul := by
103 let A := Carrier R G
104 letI : ∀ U : CompletedGroupAlgebraIndex G, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
105 fun U => (completedGroupAlgebraSystem R G).topologicalSpace U
106 have hval : Continuous fun p : A × A =>
107 ((p.1 * p.2 : A) :
108 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) := by
109 change Continuous fun p : A × A =>
110 fun U : CompletedGroupAlgebraIndex G =>
111 completedGroupAlgebraProjection R G U p.1 *
112 completedGroupAlgebraProjection R G U p.2
113 apply continuous_pi
114 intro U
115 letI : IsTopologicalRing ((completedGroupAlgebraSystem R G).X U) :=
116 completedGroupAlgebraStage_isTopologicalRing (R := R) (G := G) U
117 exact (((completedGroupAlgebraSystem R G).continuous_projection U).comp continuous_fst).mul
118 (((completedGroupAlgebraSystem R G).continuous_projection U).comp continuous_snd)
119 exact Continuous.subtype_mk hval fun p => (p.1 * p.2).2
122 IsTopologicalRing (Carrier R G) := by
123 letI : ContinuousAdd (Carrier R G) :=
124 instContinuousAddCompletedGroupAlgebra (R := R) (G := G)
125 letI : ContinuousMul (Carrier R G) :=
126 instContinuousMulCompletedGroupAlgebra (R := R) (G := G)
127 letI : ContinuousNeg (Carrier R G) :=
128 instContinuousNegCompletedGroupAlgebra (R := R) (G := G)
129 letI : IsTopologicalSemiring (Carrier R G) := IsTopologicalSemiring.mk
130 exact IsTopologicalRing.mk
132/-- Each finite stage is profinite when the coefficient ring is profinite. -/
134 (hR : IsProfiniteRing R) (U : CompletedGroupAlgebraIndex G) :
135 IsProfiniteRing ((completedGroupAlgebraSystem R G).X U) := by
137 exact finiteGroupAlgebra_isProfiniteRing R (CompletedGroupAlgebraQuotient G U) hR
139/-- The completed group algebra is compact when the coefficient ring is profinite. -/
140theorem completedGroupAlgebra_compactSpace (hR : IsProfiniteRing R) :
141 CompactSpace (Carrier R G) := by
142 letI : ∀ U : CompletedGroupAlgebraIndex G,
143 CompactSpace ((completedGroupAlgebraSystem R G).X U) := fun U =>
144 (completedGroupAlgebraStage_isProfiniteRing (R := R) (G := G) hR U).2.1
145 letI : ∀ U : CompletedGroupAlgebraIndex G,
146 T2Space ((completedGroupAlgebraSystem R G).X U) := fun U =>
147 (completedGroupAlgebraStage_isProfiniteRing (R := R) (G := G) hR U).2.2.1
148 infer_instance
150/-- The completed group algebra is Hausdorff when the coefficient ring is profinite. -/
151theorem completedGroupAlgebra_t2Space (hR : IsProfiniteRing R) :
152 T2Space (Carrier R G) := by
153 letI : ∀ U : CompletedGroupAlgebraIndex G,
154 T2Space ((completedGroupAlgebraSystem R G).X U) := fun U =>
155 (completedGroupAlgebraStage_isProfiniteRing (R := R) (G := G) hR U).2.2.1
156 exact (completedGroupAlgebraSystem R G).t2Space_inverseLimit
158/-- The completed group algebra is totally disconnected when the coefficient ring is profinite. -/
159theorem completedGroupAlgebra_totallyDisconnectedSpace (hR : IsProfiniteRing R) :
160 TotallyDisconnectedSpace (Carrier R G) := by
161 letI : ∀ U : CompletedGroupAlgebraIndex G,
162 TotallyDisconnectedSpace ((completedGroupAlgebraSystem R G).X U) := fun U =>
163 (completedGroupAlgebraStage_isProfiniteRing (R := R) (G := G) hR U).2.2.2
166/-- The book §5.3 completed group algebra is a profinite topological ring. -/
167theorem completedGroupAlgebra_isProfiniteRing (hR : IsProfiniteRing R) :
168 IsProfiniteRing (Carrier R G) := by
169 letI : CompactSpace (Carrier R G) :=
170 completedGroupAlgebra_compactSpace (R := R) (G := G) hR
171 letI : T2Space (Carrier R G) :=
172 completedGroupAlgebra_t2Space (R := R) (G := G) hR
173 letI : TotallyDisconnectedSpace (Carrier R G) :=
174 completedGroupAlgebra_totallyDisconnectedSpace (R := R) (G := G) hR
175 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
177/-- The completed group algebra is a profinite module over its profinite coefficient ring. -/
178theorem completedGroupAlgebra_isProfiniteModule (hR : IsProfiniteRing R) :
179 IsProfiniteModule R (Carrier R G) := by
180 letI : IsTopologicalRing R := hR.1
181 letI : IsTopologicalRing (Carrier R G) :=
182 instIsTopologicalRingCompletedGroupAlgebra (R := R) (G := G)
183 letI : IsTopologicalAddGroup (Carrier R G) := inferInstance
184 letI : ContinuousSMul R (Carrier R G) :=
185 instContinuousSMulCompletedGroupAlgebra (R := R) (G := G)
186 letI : CompactSpace (Carrier R G) :=
187 completedGroupAlgebra_compactSpace (R := R) (G := G) hR
188 letI : T2Space (Carrier R G) :=
189 completedGroupAlgebra_t2Space (R := R) (G := G) hR
190 letI : TotallyDisconnectedSpace (Carrier R G) :=
191 completedGroupAlgebra_totallyDisconnectedSpace (R := R) (G := G) hR
192 exact ⟨hR, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance⟩
194/-- The finite-stage projection preserves compatible. -/
195@[simp]
197 (x : Carrier R G) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
198 completedGroupAlgebraTransition R G hUV (completedGroupAlgebraProjection R G V x) =
199 completedGroupAlgebraProjection R G U x :=
200 (completedGroupAlgebraSystem R G).projection_compatible x U V hUV
202end