CompletedGroupAlgebra/Basic/InClass/Stage.lean

1import CompletedGroupAlgebra.Basic.InClass.Index

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/CompletedGroupAlgebra/Basic/InClass/Stage.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

10-/

11/-!

12# Class-Indexed Completed Group Algebras

14Finite-class-indexed inverse systems and inverse limits for completed group algebras.

15-/

17open scoped Topology

19namespace CompletedGroupAlgebra

21noncomputable section

23open ProCGroups

24open ProCGroups.ProC

25open ProCGroups.InverseSystems

27universe u v w

29variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

30variable (R : Type u) [CommRing R]

32section InClass

34/-- The finite-stage group algebra `R[G/U]` for a `C`-indexed quotient. -/

35abbrev CompletedGroupAlgebraStageInClass (C : ProCGroups.FiniteGroupClass.{v})

36 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]

37 [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndexInClass G C) :

38 Type (max u v) :=

39 MonoidAlgebra R (CompletedGroupAlgebraQuotientInClass G C U)

41/-- Change coefficients on one `C`-indexed completed-group-algebra stage. -/

42def completedGroupAlgebraStageCoeffMapInClass

43 (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S]

44 (f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C) :

45 CompletedGroupAlgebraStageInClass C R G U →+*

46 CompletedGroupAlgebraStageInClass C S G U :=

47 MonoidAlgebra.mapRangeRingHom (CompletedGroupAlgebraQuotientInClass G C U) f

49@[simp]

50theorem completedGroupAlgebraStageCoeffMapInClass_single

51 (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S]

52 (f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C)

53 (q : CompletedGroupAlgebraQuotientInClass G C U) (r : R) :

54 completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U

55 (MonoidAlgebra.single q r) =

56 MonoidAlgebra.single q (f r) := by

57 exact MonoidAlgebra.mapRangeRingHom_single f q r

59@[simp]

60theorem completedGroupAlgebraStageCoeffMapInClass_comp

61 (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) (T : Type*) [CommRing S]

62 [CommRing T] (f : R →+* S) (g : S →+* T)

63 (U : CompletedGroupAlgebraIndexInClass G C) :

64 (completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp

65 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U) =

66 completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C T (g.comp f) U := by

67 exact (MonoidAlgebra.mapRangeRingHom_comp

68 (M := CompletedGroupAlgebraQuotientInClass G C U) g f).symm

70/-- A finite coefficient ring gives finite `C`-indexed completed-group-algebra stages. -/

71theorem finite_completedGroupAlgebraStageInClass

72 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)

73 [Finite R] (U : CompletedGroupAlgebraIndexInClass G C) :

74 Finite (CompletedGroupAlgebraStageInClass C R G U) := by

75 classical

76 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=

77 finite_completedGroupAlgebraQuotientInClass G C hC U

78 letI : Fintype (CompletedGroupAlgebraQuotientInClass G C U) := Fintype.ofFinite _

79 letI : Fintype R := Fintype.ofFinite R

80 letI : DecidableEq (CompletedGroupAlgebraQuotientInClass G C U) := Classical.decEq _

81 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U → R) := by

82 letI : Fintype (CompletedGroupAlgebraQuotientInClass G C U → R) := inferInstance

83 exact Finite.of_fintype _

84 let f :

85 CompletedGroupAlgebraStageInClass C R G U →

86 CompletedGroupAlgebraQuotientInClass G C U → R := fun x q => x q

87 refine Finite.of_injective f ?_

88 intro x y hxy

89 ext q

90 exact congrFun hxy q

92instance instRingCompletedGroupAlgebraStageInClass

93 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :

94 Ring (CompletedGroupAlgebraStageInClass C R G U) := by

95 dsimp [CompletedGroupAlgebraStageInClass, CompletedGroupAlgebraQuotientInClass]

96 infer_instance

98/-- The transition map `R[G/V] -> R[G/U]` in the `C`-indexed completed-group-algebra tower. -/

99def completedGroupAlgebraTransitionInClass

100 (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]

101 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

102 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :

103 CompletedGroupAlgebraStageInClass C R G V →+*

104 CompletedGroupAlgebraStageInClass C R G U :=

105 MonoidAlgebra.mapDomainRingHom R

106 (OpenNormalSubgroupInClass.map

107 (C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

108

109/-- The transition map sends group-like basis elements by quotient projection. -/

110@[simp]

111theorem completedGroupAlgebraTransitionInClass_of

112 (C : ProCGroups.FiniteGroupClass.{v})

113 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)

114 (g : CompletedGroupAlgebraQuotientInClass G C V) :

115 completedGroupAlgebraTransitionInClass C R G hUV (MonoidAlgebra.of R _ g) =

116 MonoidAlgebra.single ((OpenNormalSubgroupInClass.map

117 (C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1 := by

118 classical

119 simp only [completedGroupAlgebraTransitionInClass, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,

120 OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]

121 rfl

122

123/-- The transition map sends singleton coefficients by quotient projection. -/

124@[simp]

125theorem completedGroupAlgebraTransitionInClass_single

126 (C : ProCGroups.FiniteGroupClass.{v})

127 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)

128 (q : CompletedGroupAlgebraQuotientInClass G C V) (r : R) :

129 completedGroupAlgebraTransitionInClass C R G hUV (MonoidAlgebra.single q r) =

130 MonoidAlgebra.single

131 ((OpenNormalSubgroupInClass.map

132 (C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) r := by

133 classical

134 simp only [completedGroupAlgebraTransitionInClass, MonoidAlgebra.single, MonoidAlgebra.mapDomainRingHom_apply,

135 Finsupp.mapDomain_single]

136 rfl

137

138/-- The identity transition map in the `C`-indexed tower is the identity ring homomorphism. -/

139@[simp]

140theorem completedGroupAlgebraTransitionInClass_id

141 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :

142 completedGroupAlgebraTransitionInClass C R G (le_rfl : U ≤ U) = RingHom.id _ := by

143 rw [completedGroupAlgebraTransitionInClass, OpenNormalSubgroupInClass.map_id]

144 exact MonoidAlgebra.mapDomainRingHom_id

145 (R := R) (M := CompletedGroupAlgebraQuotientInClass G C U)

146

147/-- Transition maps in the `C`-indexed tower compose as expected. -/

148@[simp]

149theorem completedGroupAlgebraTransitionInClass_comp

150 (C : ProCGroups.FiniteGroupClass.{v})

151 {U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :

152 (completedGroupAlgebraTransitionInClass C R G hUV).comp

153 (completedGroupAlgebraTransitionInClass C R G hVW) =

154 completedGroupAlgebraTransitionInClass C R G (hUV.trans hVW) := by

155 rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraTransitionInClass,

156 completedGroupAlgebraTransitionInClass, ← MonoidAlgebra.mapDomainRingHom_comp]

157 congr 1

158 exact OpenNormalSubgroupInClass.map_comp

159 (C := C) (G := G)

160 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)

161 hUV hVW

162

163/-- `C`-indexed stage transitions commute with coefficient change. -/

164@[simp]

165theorem completedGroupAlgebraStageCoeffMapInClass_compatible

166 (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S] (f : R →+* S)

167 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :

168 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U).comp

169 (completedGroupAlgebraTransitionInClass C R G hUV) =

170 (completedGroupAlgebraTransitionInClass C S G hUV).comp

171 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V) := by

172 exact MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom

173 (f := f)

174 (g := OpenNormalSubgroupInClass.map

175 (C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

176

177/-- Two coefficient changes and two `C`-indexed group-quotient transitions compose as the

178combined change and combined transition. -/

179@[simp 900]

180theorem completedGroupAlgebraStageCoeffMapInClass_transition_comp

181 (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) (T : Type*) [CommRing S]

182 [CommRing T] (f : R →+* S) (g : S →+* T)

183 {U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :

184 ((completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp

185 (completedGroupAlgebraTransitionInClass C S G hUV)).comp

186 ((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V).comp

187 (completedGroupAlgebraTransitionInClass C R G hVW)) =

188 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C T (g.comp f) U).comp

189 (completedGroupAlgebraTransitionInClass C R G (hUV.trans hVW)) := by

190 calc

191 ((completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp

192 (completedGroupAlgebraTransitionInClass C S G hUV)).comp

193 ((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V).comp

194 (completedGroupAlgebraTransitionInClass C R G hVW))

195 =

196 (completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp

197 (((completedGroupAlgebraTransitionInClass C S G hUV).comp

198 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V)).comp

199 (completedGroupAlgebraTransitionInClass C R G hVW)) := by

200 apply RingHom.ext

201 intro x

202 rfl

203 _ =

204 (completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp

205 (((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U).comp

206 (completedGroupAlgebraTransitionInClass C R G hUV)).comp

207 (completedGroupAlgebraTransitionInClass C R G hVW)) := by

208 rw [← completedGroupAlgebraStageCoeffMapInClass_compatible

209 (R := R) (G := G) C S f hUV]

210 _ =

211 ((completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp

212 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)).comp

213 ((completedGroupAlgebraTransitionInClass C R G hUV).comp

214 (completedGroupAlgebraTransitionInClass C R G hVW)) := by

215 apply RingHom.ext

216 intro x

217 rfl

218 _ =

219 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C T (g.comp f) U).comp

220 ((completedGroupAlgebraTransitionInClass C R G hUV).comp

221 (completedGroupAlgebraTransitionInClass C R G hVW)) := by

222 rw [completedGroupAlgebraStageCoeffMapInClass_comp]

223 _ =

224 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C T (g.comp f) U).comp

225 (completedGroupAlgebraTransitionInClass C R G (hUV.trans hVW)) := by

226 rw [completedGroupAlgebraTransitionInClass_comp]

227

228/-- Transition maps commute with scalar multiplication by coefficients. -/

229theorem completedGroupAlgebraTransitionInClass_smul

230 (C : ProCGroups.FiniteGroupClass.{v})

231 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)

232 (r : R) (x : CompletedGroupAlgebraStageInClass C R G V) :

233 completedGroupAlgebraTransitionInClass C R G hUV (r • x) =

234 r • completedGroupAlgebraTransitionInClass C R G hUV x := by

235 rw [Algebra.smul_def, Algebra.smul_def, map_mul]

236 congr 1

237 simp only [completedGroupAlgebraTransitionInClass, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,

238 RingHom.coe_id, Function.comp_apply, id_eq, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]

239

240/-- Transition maps commute with the coefficient algebra maps. -/

241theorem completedGroupAlgebraTransitionInClass_algebraMap

242 (C : ProCGroups.FiniteGroupClass.{v})

243 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (r : R) :

244 completedGroupAlgebraTransitionInClass C R G hUV

245 (algebraMap R (CompletedGroupAlgebraStageInClass C R G V) r) =

246 algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r := by

247 simp only [completedGroupAlgebraTransitionInClass, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,

248 RingHom.coe_id, Function.comp_apply, id_eq, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]

249

250variable [TopologicalSpace R] [IsTopologicalRing R]

251

252end InClass

253

254end

255

256end CompletedGroupAlgebra