Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra

1import Mathlib.Algebra.MonoidAlgebra.MapDomain

2import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup

4/-!

5# Fox differential: completed — coefficient rings — completed group algebra

7The principal declarations in this module are:

9- `CompletedGroupAlgebraIndexInClass`

10 The index set for a completed group algebra over finite quotients belonging to a class `C`.

11- `CompletedGroupAlgebraQuotientInClass`

12 The finite quotient of `G` attached to one class-restricted completed-group-algebra stage.

13- `completedGroupAlgebraTransitionInClass_id`

14 Identity case for completedGroupAlgebraTransitionInClass_id.

15- `completedGroupAlgebraTransitionInClass_comp`

16 Composition lemma completedGroupAlgebraTransitionInClass_comp.

17-/

19namespace FoxDifferential

21open Set

22open ProCGroups

23open ProCGroups.InverseSystems

24open ProCGroups.ProC

25open scoped Topology

27noncomputable section

29universe u v w

31variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

33/-- The index set for a completed group algebra over finite quotients belonging to a class `C`. -/

34abbrev CompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{u}) :=

35 OrderDual (OpenNormalSubgroupInClass C G)

37/-- The finite quotient of `G` attached to one class-restricted completed-group-algebra stage. -/

38abbrev CompletedGroupAlgebraQuotientInClass

39 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _ :=

40 (openNormalSubgroupInClassSystem C G).X U

42/-- The discrete group ring over one class-restricted finite quotient of `G`. -/

43abbrev CompletedGroupAlgebraStageInClass

44 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _ :=

45 MonoidAlgebra ℤ (CompletedGroupAlgebraQuotientInClass G C U)

47/-- The transition map between two class-restricted completed-group-algebra stages. -/

48def completedGroupAlgebraTransitionInClass

49 (C : ProCGroups.FiniteGroupClass.{u})

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

51 CompletedGroupAlgebraStageInClass G C V →+*

52 CompletedGroupAlgebraStageInClass G C U :=

53 MonoidAlgebra.mapDomainRingHom ℤ

54 (OpenNormalSubgroupInClass.map

55 (C := C) (G := G)

56 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

58/-- Identity case for completedGroupAlgebraTransitionInClass_id. -/

59@[simp]

60theorem completedGroupAlgebraTransitionInClass_id

61 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :

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

63 rw [completedGroupAlgebraTransitionInClass, OpenNormalSubgroupInClass.map_id]

64 exact MonoidAlgebra.mapDomainRingHom_id

65 (R := ℤ) (M := CompletedGroupAlgebraQuotientInClass G C U)

67/-- Composition lemma completedGroupAlgebraTransitionInClass_comp. -/

68@[simp]

69theorem completedGroupAlgebraTransitionInClass_comp

70 (C : ProCGroups.FiniteGroupClass.{u})

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

72 (completedGroupAlgebraTransitionInClass G C hUV).comp

73 (completedGroupAlgebraTransitionInClass G C hVW) =

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

75 rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraTransitionInClass,

76 completedGroupAlgebraTransitionInClass, ← MonoidAlgebra.mapDomainRingHom_comp]

77 congr 1

78 exact OpenNormalSubgroupInClass.map_comp

79 (C := C) (G := G)

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

81 hUV hVW

83/-- The class-restricted inverse system of finite-stage integral group rings. -/

84def completedGroupAlgebraSystemInClass

85 (C : ProCGroups.FiniteGroupClass.{u}) :

86 InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where

87 X := CompletedGroupAlgebraStageInClass G C

88 topologicalSpace := fun _ => ⊥

89 map := fun {U V} hUV => completedGroupAlgebraTransitionInClass G C hUV

90 continuous_map := by

91 intro U V hUV

92 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass G C U) := ⊥

93 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass G C V) := ⊥

94 letI : DiscreteTopology (CompletedGroupAlgebraStageInClass G C V) := ⟨rfl⟩

95 exact continuous_of_discreteTopology

96 map_id := by

97 intro U

98 funext x

99 exact congrFun

100 (congrArg DFunLike.coe

101 (completedGroupAlgebraTransitionInClass_id G C U)) x

102 map_comp := by

103 intro U V W hUV hVW

104 funext x

105 exact congrFun

106 (congrArg DFunLike.coe

107 (completedGroupAlgebraTransitionInClass_comp G C hUV hVW)) x

108

109/-- The quotient ring map from `ℤ[G]` to one class-restricted finite stage. -/

110def completedGroupAlgebraStageMapInClass

111 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :

112 MonoidAlgebra ℤ G →+* CompletedGroupAlgebraStageInClass G C U :=

113 MonoidAlgebra.mapDomainRingHom ℤ

114 (openNormalSubgroupInClassProj (C := C) (G := G) U)

115

116/-- Evaluation formula for completedGroupAlgebraStageMapInClass_of. -/

117@[simp]

118theorem completedGroupAlgebraStageMapInClass_of

119 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :

120 completedGroupAlgebraStageMapInClass G C U (MonoidAlgebra.of ℤ _ g) =

121 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1 := by

122 classical

123 change

124 MonoidAlgebra.mapDomain

125 (openNormalSubgroupInClassProj (C := C) (G := G) U)

126 (MonoidAlgebra.single g 1) =

127 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1

128 exact MonoidAlgebra.mapDomain_single

129

130/-- Compatibility lemma completedGroupAlgebraStageMapInClass_compatible. -/

131@[simp]

132theorem completedGroupAlgebraStageMapInClass_compatible

133 (C : ProCGroups.FiniteGroupClass.{u})

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

135 (completedGroupAlgebraTransitionInClass G C hUV).comp

136 (completedGroupAlgebraStageMapInClass G C V) =

137 completedGroupAlgebraStageMapInClass G C U := by

138 rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraStageMapInClass,

139 completedGroupAlgebraStageMapInClass, ← MonoidAlgebra.mapDomainRingHom_comp]

140 congr 1

141

142/-- Compatibility for a class-restricted completed group algebra family. -/

143def CompletedGroupAlgebraCompatibleInClass

144 (C : ProCGroups.FiniteGroupClass.{u})

145 (x : ∀ U : CompletedGroupAlgebraIndexInClass G C,

146 CompletedGroupAlgebraStageInClass G C U) : Prop :=

147 (completedGroupAlgebraSystemInClass G C).Compatible x

148

149/-- The class-restricted completed group algebra as an inverse-limit subtype. -/

150abbrev CompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=

151 {x : ∀ U : CompletedGroupAlgebraIndexInClass G C,

152 CompletedGroupAlgebraStageInClass G C U //

153 CompletedGroupAlgebraCompatibleInClass G C x}

154

155/-- Projection from the class-restricted completed group algebra to one finite stage. -/

156def completedGroupAlgebraProjectionInClass

157 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :

158 CompletedGroupAlgebraInClass G C → CompletedGroupAlgebraStageInClass G C U :=

159 (completedGroupAlgebraSystemInClass G C).projection U

160

161section ComapInClass

162

163variable {G H : Type u}

164variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

165variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

166

167/-- Pull back a class-restricted finite quotient along a continuous homomorphism.

168

169The hereditary hypothesis is the precise extra closure property needed: the pulled-back quotient

170embeds into the target quotient, so membership in `C` follows from closure under subgroups. -/

171def completedGroupAlgebraComapIndexInClass

172 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)

173 (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) :

174 CompletedGroupAlgebraIndexInClass G C := by

175 let V : OpenNormalSubgroup H := (OrderDual.ofDual U).1

176 let W : OpenNormalSubgroup G := OpenNormalSubgroup.comap ψ.toMonoidHom ψ.continuous_toFun V

177 refine OrderDual.toDual ⟨W, ?_⟩

178 let f : G ⧸ (W : Subgroup G) →* H ⧸ (V : Subgroup H) :=

179 QuotientGroup.map _ _ ψ.toMonoidHom (by

180 intro g hg

181 simpa [W] using hg)

182 have hf : Function.Injective f := by

183 intro x y hxy

184 rcases QuotientGroup.mk'_surjective (W : Subgroup G) x with ⟨a, rfl⟩

185 rcases QuotientGroup.mk'_surjective (W : Subgroup G) y with ⟨b, rfl⟩

186 apply QuotientGroup.eq.2

187 change ψ (a⁻¹ * b) ∈ (V : Subgroup H)

188 have hv : (ψ a)⁻¹ * ψ b ∈ (V : Subgroup H) := QuotientGroup.eq.1 hxy

189 simpa using hv

190 exact hC.of_injective (OrderDual.ofDual U).2 f hf

191

192/-- The finite quotient map induced by a continuous homomorphism after pulling back the stage. -/

193def completedGroupAlgebraComapQuotientMapInClass

194 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)

195 (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) :

196 CompletedGroupAlgebraQuotientInClass G C

197 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U) →*

198 CompletedGroupAlgebraQuotientInClass H C U := by

199 let V : OpenNormalSubgroup H := (OrderDual.ofDual U).1

200 let W : OpenNormalSubgroup G := OpenNormalSubgroup.comap ψ.toMonoidHom ψ.continuous_toFun V

201 exact QuotientGroup.map _ _ ψ.toMonoidHom (by

202 intro g hg

203 simpa [W, completedGroupAlgebraComapIndexInClass] using hg)

204

205/-- Evaluation formula for completedGroupAlgebraComapQuotientMapInClass_mk. -/

206@[simp]

207theorem completedGroupAlgebraComapQuotientMapInClass_mk

208 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)

209 (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) (g : G) :

210 completedGroupAlgebraComapQuotientMapInClass

211 (G := G) (H := H) C hC ψ U

212 (QuotientGroup.mk'

213 ((((OrderDual.ofDual

214 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U)).1 :

215 OpenNormalSubgroup G) : Subgroup G)) g) =

216 QuotientGroup.mk' ((((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H))

217 (ψ g) := rfl

218

219/-- Surjectivity lemma completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective. -/

220theorem completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective

221 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)

222 (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)

223 (U : CompletedGroupAlgebraIndexInClass H C) :

224 Function.Surjective

225 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ U) := by

226 intro h

227 rcases QuotientGroup.mk'_surjective

228 ((((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)) h with ⟨a, rfl⟩

229 rcases hψ a with ⟨g, rfl⟩

230 refine ⟨QuotientGroup.mk'

231 ((((OrderDual.ofDual

232 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U)).1 :

233 OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩

234 rw [completedGroupAlgebraComapQuotientMapInClass_mk]

235

236omit [IsTopologicalGroup G] in

237/-- 有限群クラスを固定した標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/

238theorem completedGroupAlgebraComapIndexInClass_mono

239 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)

240 (ψ : ContinuousMonoidHom G H) {U V : CompletedGroupAlgebraIndexInClass H C}

241 (hUV : U ≤ V) :

242 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U ≤

243 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V := by

244 change

245 Subgroup.comap ψ.toMonoidHom

246 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H) ≤

247 Subgroup.comap ψ.toMonoidHom

248 (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)

249 exact Subgroup.comap_mono hUV

250

251/-- Compatibility lemma completedGroupAlgebraComapQuotientMapInClass_compatible. -/

252@[simp]

253theorem completedGroupAlgebraComapQuotientMapInClass_compatible

254 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)

255 (ψ : ContinuousMonoidHom G H) {U V : CompletedGroupAlgebraIndexInClass H C}

256 (hUV : U ≤ V) :

257 (OpenNormalSubgroupInClass.map

258 (C := C) (G := H)

259 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV).comp

260 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ V) =

261 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ U).comp

262 (OpenNormalSubgroupInClass.map

263 (C := C) (G := G)

264 (U := OrderDual.ofDual

265 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U))

266 (V := OrderDual.ofDual

267 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V))

268 (completedGroupAlgebraComapIndexInClass_mono (G := G) (H := H) C hC ψ hUV)) := by

269 ext q

270 rcases QuotientGroup.mk'_surjective

271 ((((OrderDual.ofDual

272 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V)).1 :

273 OpenNormalSubgroup G) : Subgroup G)) q with ⟨g, rfl⟩

274 rfl

275

276/-- Pulling a finite quotient back along the identity continuous homomorphism gives the same

277class-restricted index. This is intentionally an equality theorem, since dependent inverse-limit

278indices are often not definitionally equal after target naturality rewrites. -/

279@[simp]

280theorem completedGroupAlgebraComapIndexInClass_id

281 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)

282 (U : CompletedGroupAlgebraIndexInClass G C) :

283 completedGroupAlgebraComapIndexInClass (G := G) (H := G) C hC

284 (ContinuousMonoidHom.id G) U = U := by

285 apply OrderDual.ofDual.injective

286 ext x

287 simp only [completedGroupAlgebraComapIndexInClass, ContinuousMonoidHom.coe_toMonoidHom,

288 OrderDual.ofDual_toDual, OpenNormalSubgroup.toSubgroup_comap, Subsemigroup.mem_carrier,

289 Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid, Subgroup.mem_comap, MonoidHom.coe_coe,

290 ContinuousMonoidHom.id_toFun, OpenSubgroup.mem_toSubgroup]

291

292omit [IsTopologicalGroup G] in

293/-- Pullback of class-restricted finite quotients is functorial for continuous target maps.

294

295This is the index-level rewrite needed when the two inverse-limit stage indices produced by a

296composite target map are propositionally, but not definitionally, the same. -/

297@[simp]

298theorem completedGroupAlgebraComapIndexInClass_comp

299 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)

300 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]

301 (φ : G →ₜ* H) (ψ : H →ₜ* K) (U : CompletedGroupAlgebraIndexInClass K C) :

302 completedGroupAlgebraComapIndexInClass (G := G) (H := K) C hC (ψ.comp φ) U =

303 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC φ

304 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC ψ U) := by

305 apply OrderDual.ofDual.injective

306 ext x

307 simp only [completedGroupAlgebraComapIndexInClass, ContinuousMonoidHom.coe_toMonoidHom,

308 OrderDual.ofDual_toDual, OpenNormalSubgroup.toSubgroup_comap, Subsemigroup.mem_carrier,

309 Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid, Subgroup.mem_comap, MonoidHom.coe_coe,

310 ContinuousMonoidHom.comp_toFun, OpenSubgroup.mem_toSubgroup]

311

312omit [IsTopologicalGroup G] in

313/-- Pulling back the canonical trivial quotient gives the canonical trivial quotient. -/

314@[simp]

315theorem completedGroupAlgebraComapIndexInClass_top

316 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)

317 [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]

318 (ψ : G →ₜ* H) :

319 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ

320 (OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := H))) =

321 OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := G)) := by

322 apply OrderDual.ofDual.injective

323 ext x

324 simp only [completedGroupAlgebraComapIndexInClass, ContinuousMonoidHom.coe_toMonoidHom,

325 OrderDual.ofDual_toDual, OpenNormalSubgroup.toSubgroup_comap, Subsemigroup.mem_carrier,

326 Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid, Subgroup.mem_comap, MonoidHom.coe_coe,

327 OpenSubgroup.mem_toSubgroup]

328 constructor <;> intro _ <;> trivial

329

330end ComapInClass

331

332end

333

334end FoxDifferential