CompletedGroupAlgebra/UniversalProperty/Basic.lean

1import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/CompletedGroupAlgebra/UniversalProperty/Basic.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

10-/

11/-!

12# Completed group algebra group-like elements

14This module isolates the group-like elements and dense algebraic group-ring map that control maps out of a completed group algebra.

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 concrete inverse-limit construction satisfies the completed-group-algebra

34property package. -/

35theorem completedGroupAlgebra_isCompletedGroupAlgebraModel

36 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :

37 IsCompletedGroupAlgebraModel R G (Carrier R G) := by

38 refine ⟨hR, hG, completedGroupAlgebra_isProfiniteRing (R := R) (G := G) hR, ?_⟩

39 refine ⟨completedGroupAlgebraNaturalTopology R G, ?_⟩

40 letI : TopologicalSpace (MonoidAlgebra R G) :=

41 completedGroupAlgebraNaturalTopology R G

42 exact ⟨toCompletedGroupAlgebraRingHom R G,

43 denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG,

44 continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G)⟩

46/-- The image of a group element in the completed group algebra. -/

47def completedGroupAlgebraOf (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]

48 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

49 (g : G) : Carrier R G :=

50 toCompletedGroupAlgebra R G (MonoidAlgebra.of R G g)

52/-- Projection of a completed group-like element to a finite quotient stage. -/

53@[simp]

54theorem completedGroupAlgebraProjection_of

55 (U : CompletedGroupAlgebraIndex G) (g : G) :

56 completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G g) =

57 MonoidAlgebra.single (openNormalSubgroupInClassProj

58 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1 := by

59 rw [completedGroupAlgebraOf, completedGroupAlgebraProjection_toCompletedGroupAlgebra,

60 completedGroupAlgebraStageMap_of]

62/-- The completed group-like element attached to `1` is the unit. -/

63@[simp]

64theorem completedGroupAlgebraOf_one :

65 completedGroupAlgebraOf R G 1 = (1 : Carrier R G) := by

66 apply (completedGroupAlgebraSystem R G).ext

67 intro U

68 change completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G 1) =

69 completedGroupAlgebraProjection R G U (1 : Carrier R G)

70 rw [completedGroupAlgebraProjection_of, completedGroupAlgebraProjection_one]

71 change MonoidAlgebra.single

72 (openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U 1) (1 : R) = 1

73 rfl

75/-- Completed group-like elements multiply according to the group law. -/

76@[simp]

77theorem completedGroupAlgebraOf_mul (g h : G) :

78 completedGroupAlgebraOf R G (g * h) =

79 completedGroupAlgebraOf R G g * completedGroupAlgebraOf R G h := by

80 apply (completedGroupAlgebraSystem R G).ext

81 intro U

82 change completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G (g * h)) =

83 completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G g * completedGroupAlgebraOf R G h)

84 rw [completedGroupAlgebraProjection_of, completedGroupAlgebraProjection_mul,

85 completedGroupAlgebraProjection_of, completedGroupAlgebraProjection_of]

86 change MonoidAlgebra.single

87 (openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U (g * h)) (1 : R) =

88 MonoidAlgebra.single

89 (openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1 *

90 MonoidAlgebra.single

91 (openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U h) 1

92 simp only [map_mul, MonoidAlgebra.single_mul_single, mul_one]

94/-- The finite-stage group-like map `G → R[G/U]` is continuous. -/

95theorem continuous_completedGroupAlgebraStageMap_of

96 (U : CompletedGroupAlgebraIndex G) :

97 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=

98 (completedGroupAlgebraSystem R G).topologicalSpace U

99 Continuous fun g : G => completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g) := by

100 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=

101 (completedGroupAlgebraSystem R G).topologicalSpace U

102 letI : DiscreteTopology (CompletedGroupAlgebraQuotient G U) :=

103 QuotientGroup.discreteTopology

104 (ProCGroups.openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))

105 have hbasis :

106 Continuous fun q : CompletedGroupAlgebraQuotient G U =>

107 (MonoidAlgebra.of R (CompletedGroupAlgebraQuotient G U) q :

108 CompletedGroupAlgebraStage R G U) :=

109 continuous_of_discreteTopology

110 have hproj :

111 Continuous fun g : G =>

112 openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g := by

113 change Continuous

114 (QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G))

115 exact continuous_quotient_mk'

116 simpa [MonoidAlgebra.of, completedGroupAlgebraStageMap_single] using hbasis.comp hproj

117

118/-- The completed group-like map `G → [[RG]]` is continuous. -/

119theorem continuous_completedGroupAlgebraOf :

120 Continuous (completedGroupAlgebraOf R G) := by

121 letI : ∀ U : CompletedGroupAlgebraIndex G, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=

122 fun U => (completedGroupAlgebraSystem R G).topologicalSpace U

123 have hval : Continuous fun g : G =>

124 fun U : CompletedGroupAlgebraIndex G =>

125 (show CompletedGroupAlgebraStage R G U from (completedGroupAlgebraOf R G g).1 U) := by

126 change Continuous fun g : G =>

127 fun U : CompletedGroupAlgebraIndex G =>

128 completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g)

129 apply continuous_pi

130 intro U

131 exact continuous_completedGroupAlgebraStageMap_of (R := R) (G := G) U

132 exact Continuous.subtype_mk hval fun g => (completedGroupAlgebraOf R G g).2

133

134/-- The dense abstract group-algebra map lands in the span of the completed group-like

135elements. -/

136theorem toCompletedGroupAlgebraRingHom_mem_span_completedGroupAlgebraOf

137 (x : MonoidAlgebra R G) :

138 toCompletedGroupAlgebraRingHom R G x ∈

139 Submodule.span R (Set.range (completedGroupAlgebraOf R G)) := by

140 classical

141 induction x using Finsupp.induction with

142 | zero =>

143 rw [show toCompletedGroupAlgebraRingHom R G (0 : MonoidAlgebra R G) =

144 (0 : Carrier R G) by

145 exact map_zero (toCompletedGroupAlgebraRingHom R G)]

146 exact Submodule.zero_mem _

147 | single_add g r x _ _ ih =>

148 rw [map_add]

149 refine Submodule.add_mem _ ?_ ih

150 have hsingle :

151 toCompletedGroupAlgebraRingHom R G (MonoidAlgebra.single g r) =

152 r • completedGroupAlgebraOf R G g := by

153 rw [show MonoidAlgebra.single g r =

154 r • MonoidAlgebra.of R G g by

155 simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.smul_single, smul_eq_mul, mul_one]]

156 change toCompletedGroupAlgebra R G (r • MonoidAlgebra.of R G g) =

157 r • completedGroupAlgebraOf R G g

158 rw [toCompletedGroupAlgebra_smul]

159 rfl

160 rw [hsingle]

161 exact Submodule.smul_mem _ r (Submodule.subset_span ⟨g, rfl⟩)

162

163/-- The completed group-like elements topologically generate `[[RG]]` as an `R`-module. -/

164theorem completedGroupAlgebraOf_dense_span (hG : ProCGroups.IsProfiniteGroup G) :

165 closure (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :

166 Set (Carrier R G)) = Set.univ := by

167 rw [Set.eq_univ_iff_forall]

168 intro y

169 have hy :

170 y ∈ closure (Set.range (toCompletedGroupAlgebraRingHom R G)) := by

171 rw [(denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG).closure_range]

172 exact Set.mem_univ y

173 exact closure_mono (by

174 intro z hz

175 rcases hz with ⟨x, rfl⟩

176 exact toCompletedGroupAlgebraRingHom_mem_span_completedGroupAlgebraOf

177 (R := R) (G := G) x) hy

178

179/-- The structural inputs for Lemma 5.3.5(d)'s free profinite-module statement; the full

180continuous-linear universal property is proved below. -/

181theorem completedGroupAlgebraOf_freeProfiniteModule_prerequisites

182 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :

183 IsProfiniteRing R ∧ IsProfiniteModule R (Carrier R G) ∧

184 Continuous (completedGroupAlgebraOf R G) ∧

185 closure (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :

186 Set (Carrier R G)) = Set.univ := by

187 exact ⟨hR, completedGroupAlgebra_isProfiniteModule (R := R) (G := G) hR,

188 continuous_completedGroupAlgebraOf (R := R) (G := G),

189 completedGroupAlgebraOf_dense_span (R := R) (G := G) hG⟩

190

191/-- Uniqueness half of Lemma 5.3.5(d)'s universal property: a continuous linear map out of

192`[[RG]]` is determined by its values on the completed group-like elements. -/

193theorem completedGroupAlgebraContinuousLinearMap_ext_of_basis

194 (hG : ProCGroups.IsProfiniteGroup G)

195 {N : Type (max u v)} [AddCommGroup N] [TopologicalSpace N] [Module R N] [T2Space N]

196 {F K : Carrier R G →L[R] N}

197 (hbasis : ∀ g : G, F (completedGroupAlgebraOf R G g) =

198 K (completedGroupAlgebraOf R G g)) :

199 F = K := by

200 apply ContinuousLinearMap.ext

201 intro x

202 have hclosed : IsClosed {x : Carrier R G | F x = K x} :=

203 isClosed_eq F.continuous K.continuous

204 have hspan :

205 (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :

206 Set (Carrier R G)) ⊆

207 {x : Carrier R G | F x = K x} := by

208 intro y hy

209 exact Submodule.span_induction

210 (fun z hz => by

211 rcases hz with ⟨g, rfl⟩

212 exact hbasis g)

213 (by simp only [Set.mem_setOf_eq, map_zero])

214 (fun z w _ _ hz hw => by

215 change F (z + w) = K (z + w)

216 rw [map_add, map_add, hz, hw])

217 (fun r z _ hz => by

218 change F (r • z) = K (r • z)

219 rw [map_smul, map_smul, hz])

220 hy

221 have hx :

222 x ∈ closure (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :

223 Set (Carrier R G)) := by

224 rw [completedGroupAlgebraOf_dense_span (R := R) (G := G) hG]

225 exact Set.mem_univ x

226 exact hclosed.closure_subset_iff.2 hspan hx

227end

228

229end CompletedGroupAlgebra