CompletedGroupAlgebra/Basic/AllFinite/Stage.lean
1import CompletedGroupAlgebra.Basic.AllFinite.Index
2import ProCGroups.Completion.ProCInteger
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/CompletedGroupAlgebra/Basic/AllFinite/Stage.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Finite stages and transition maps
15This module defines the finite quotient stages, transition maps, and stage maps for the all-finite completed group algebra.
16-/
18open scoped Topology
20namespace CompletedGroupAlgebra
22noncomputable section
24open ProCGroups
25open ProCGroups.ProC
26open ProCGroups.InverseSystems
27open ProCGroups.Completion
29universe u v w
31variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32variable (R : Type u) [CommRing R]
34/-- The finite-stage group algebra `R[G/U]` from Ribes--Zalesskii §5.3. -/
35abbrev CompletedGroupAlgebraStage (R : Type u) (G : Type v) [CommRing R] [Group G]
36 [TopologicalSpace G] [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
37 Type (max u v) :=
38 MonoidAlgebra R (CompletedGroupAlgebraQuotient G U)
40/-- Change coefficients on one all-finite completed-group-algebra stage. -/
42 (S : Type w) [CommRing S] (f : R →+* S) (U : CompletedGroupAlgebraIndex G) :
43 CompletedGroupAlgebraStage R G U →+* CompletedGroupAlgebraStage S G U :=
44 MonoidAlgebra.mapRangeRingHom (CompletedGroupAlgebraQuotient G U) f
46@[simp]
48 (S : Type w) [CommRing S] (f : R →+* S) (U : CompletedGroupAlgebraIndex G)
49 (q : CompletedGroupAlgebraQuotient G U) (r : R) :
50 completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U
51 (MonoidAlgebra.single q r) =
52 MonoidAlgebra.single q (f r) := by
53 exact MonoidAlgebra.mapRangeRingHom_single f q r
55@[simp]
57 (S : Type w) (T : Type*) [CommRing S] [CommRing T]
58 (f : R →+* S) (g : S →+* T) (U : CompletedGroupAlgebraIndex G) :
59 (completedGroupAlgebraStageCoeffMap (R := S) (G := G) T g U).comp
60 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U) =
61 completedGroupAlgebraStageCoeffMap (R := R) (G := G) T (g.comp f) U := by
62 exact (MonoidAlgebra.mapRangeRingHom_comp
63 (M := CompletedGroupAlgebraQuotient G U) g f).symm
65/-- A finite coefficient ring gives finite all-finite completed-group-algebra stages. -/
66theorem finite_completedGroupAlgebraStage [Finite R] (U : CompletedGroupAlgebraIndex G) :
67 Finite (CompletedGroupAlgebraStage R G U) := by
68 classical
69 letI : Fintype (CompletedGroupAlgebraQuotient G U) := Fintype.ofFinite _
70 letI : Fintype R := Fintype.ofFinite R
71 letI : DecidableEq (CompletedGroupAlgebraQuotient G U) := Classical.decEq _
72 letI : Finite (CompletedGroupAlgebraQuotient G U → R) := by
73 letI : Fintype (CompletedGroupAlgebraQuotient G U → R) := inferInstance
74 exact Finite.of_fintype _
75 let f : CompletedGroupAlgebraStage R G U → CompletedGroupAlgebraQuotient G U → R :=
76 fun x q => x q
77 refine Finite.of_injective f ?_
78 intro x y hxy
79 ext q
80 exact congrFun hxy q
82/-- The transition map `R[G/V] -> R[G/U]` induced by the quotient map `G/V -> G/U`. -/
83def completedGroupAlgebraTransition (R : Type u) (G : Type v) [CommRing R] [Group G]
84 [TopologicalSpace G] [IsTopologicalGroup G] {U V : CompletedGroupAlgebraIndex G}
85 (hUV : U ≤ V) :
86 CompletedGroupAlgebraStage R G V →+* CompletedGroupAlgebraStage R G U :=
87 MonoidAlgebra.mapDomainRingHom R
88 (OpenNormalSubgroupInClass.map
89 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
90 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
92/-- The transition map sends a basis element to the induced basis element. -/
93@[simp]
95 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
96 (g : CompletedGroupAlgebraQuotient G V) :
97 completedGroupAlgebraTransition R G hUV (MonoidAlgebra.of R _ g) =
98 MonoidAlgebra.single ((OpenNormalSubgroupInClass.map
99 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
100 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1 := by
101 classical
102 simp only [completedGroupAlgebraTransition, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
103 OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
104 rfl
106/-- The transition map sends singleton coefficients by quotient projection. -/
107@[simp]
109 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
110 (q : CompletedGroupAlgebraQuotient G V) (r : R) :
111 completedGroupAlgebraTransition R G hUV (MonoidAlgebra.single q r) =
112 MonoidAlgebra.single
113 ((OpenNormalSubgroupInClass.map
114 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
115 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) r := by
116 classical
117 simp only [completedGroupAlgebraTransition, MonoidAlgebra.single, MonoidAlgebra.mapDomainRingHom_apply,
118 Finsupp.mapDomain_single]
119 rfl
121/-- The transition map for the reflexive relation is the identity. -/
122@[simp]
123theorem completedGroupAlgebraTransition_id (U : CompletedGroupAlgebraIndex G) :
124 completedGroupAlgebraTransition R G (le_rfl : U ≤ U) = RingHom.id _ := by
125 rw [completedGroupAlgebraTransition, OpenNormalSubgroupInClass.map_id]
126 exact MonoidAlgebra.mapDomainRingHom_id
127 (R := R) (M := CompletedGroupAlgebraQuotient G U)
129/-- Transition maps compose along refinements of finite quotients. -/
130@[simp]
132 {U V W : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (hVW : V ≤ W) :
133 (completedGroupAlgebraTransition R G hUV).comp
134 (completedGroupAlgebraTransition R G hVW) =
135 completedGroupAlgebraTransition R G (hUV.trans hVW) := by
137 completedGroupAlgebraTransition, ← MonoidAlgebra.mapDomainRingHom_comp]
138 congr 1
139 exact OpenNormalSubgroupInClass.map_comp
140 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
141 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)
142 hUV hVW
144/-- Stage transitions commute with coefficient change. -/
145@[simp]
147 (S : Type w) [CommRing S] (f : R →+* S)
148 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
149 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U).comp
150 (completedGroupAlgebraTransition R G hUV) =
151 (completedGroupAlgebraTransition S G hUV).comp
152 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f V) := by
153 exact MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom
154 (f := f)
155 (g := OpenNormalSubgroupInClass.map
156 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
157 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
159/-- Two coefficient changes and two group-quotient transitions compose as the combined change
160and combined transition. -/
161@[simp 900]
163 (S : Type w) (T : Type*) [CommRing S] [CommRing T]
164 (f : R →+* S) (g : S →+* T)
165 {U V W : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (hVW : V ≤ W) :
166 ((completedGroupAlgebraStageCoeffMap (R := S) (G := G) T g U).comp
167 (completedGroupAlgebraTransition S G hUV)).comp
168 ((completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f V).comp
169 (completedGroupAlgebraTransition R G hVW)) =
170 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) T (g.comp f) U).comp
171 (completedGroupAlgebraTransition R G (hUV.trans hVW)) := by
172 calc
173 ((completedGroupAlgebraStageCoeffMap (R := S) (G := G) T g U).comp
174 (completedGroupAlgebraTransition S G hUV)).comp
175 ((completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f V).comp
176 (completedGroupAlgebraTransition R G hVW))
177 =
178 (completedGroupAlgebraStageCoeffMap (R := S) (G := G) T g U).comp
179 (((completedGroupAlgebraTransition S G hUV).comp
180 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f V)).comp
181 (completedGroupAlgebraTransition R G hVW)) := by
182 apply RingHom.ext
183 intro x
184 rfl
185 _ =
186 (completedGroupAlgebraStageCoeffMap (R := S) (G := G) T g U).comp
187 (((completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U).comp
188 (completedGroupAlgebraTransition R G hUV)).comp
189 (completedGroupAlgebraTransition R G hVW)) := by
191 (R := R) (G := G) S f hUV]
192 _ =
193 ((completedGroupAlgebraStageCoeffMap (R := S) (G := G) T g U).comp
194 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U)).comp
195 ((completedGroupAlgebraTransition R G hUV).comp
196 (completedGroupAlgebraTransition R G hVW)) := by
197 apply RingHom.ext
198 intro x
199 rfl
200 _ =
201 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) T (g.comp f) U).comp
202 ((completedGroupAlgebraTransition R G hUV).comp
203 (completedGroupAlgebraTransition R G hVW)) := by
205 _ =
206 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) T (g.comp f) U).comp
207 (completedGroupAlgebraTransition R G (hUV.trans hVW)) := by
210variable [TopologicalSpace R] [IsTopologicalRing R]
212/-- The inverse system `U ↦ R[G/U]` with the finite product topology on each stage. -/
213def completedGroupAlgebraSystem (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
214 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
215 ProCGroups.InverseSystems.InverseSystem (I := CompletedGroupAlgebraIndex G) where
216 X := CompletedGroupAlgebraStage R G
217 topologicalSpace := fun U => finiteGroupAlgebraTopology R (CompletedGroupAlgebraQuotient G U)
218 map := fun {U V} hUV => completedGroupAlgebraTransition R G hUV
219 continuous_map := by
220 intro U V hUV
223 (OpenNormalSubgroupInClass.map
224 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
225 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
226 map_id := by
227 intro U
228 funext x
229 exact congrFun
230 (congrArg DFunLike.coe (completedGroupAlgebraTransition_id (R := R) (G := G) U)) x
231 map_comp := by
232 intro U V W hUV hVW
233 funext x
234 exact congrFun
235 (congrArg DFunLike.coe
236 (completedGroupAlgebraTransition_comp (R := R) (G := G) hUV hVW)) x
238end