Yamaguchi Lean 4 Library
FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebra.lean
FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebra/Source

FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebra.lean

1import Mathlib.Algebra.MonoidAlgebra.MapDomain
2import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebra.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Completed coefficient algebras
15Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.
16-/
17namespace FoxDifferential
19open Set
20open ProCGroups
21open ProCGroups.InverseSystems
22open ProCGroups.ProC
23open scoped Topology
25noncomputable section
27universe u v w
29variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31/-- The index set for a completed group algebra over finite quotients belonging to a class `C`. -/
32abbrev CompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{u}) :=
35/-- The finite quotient of `G` attached to one class-restricted completed-group-algebra stage. -/
36abbrev CompletedGroupAlgebraQuotientInClass
37 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _ :=
40/-- The discrete group ring over one class-restricted finite quotient of `G`. -/
41abbrev CompletedGroupAlgebraStageInClass
42 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _ :=
43 MonoidAlgebra ℤ (CompletedGroupAlgebraQuotientInClass G C U)
45/-- The transition map between two class-restricted completed-group-algebra stages. -/
46def completedGroupAlgebraTransitionInClass
47 (C : ProCGroups.FiniteGroupClass.{u})
48 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
49 CompletedGroupAlgebraStageInClass G C V →+*
50 CompletedGroupAlgebraStageInClass G C U :=
51 MonoidAlgebra.mapDomainRingHom ℤ
52 (OpenNormalSubgroupInClass.map
53 (C := C) (G := G)
54 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
56/-- Identity case for completedGroupAlgebraTransitionInClass_id. -/
57@[simp]
58theorem completedGroupAlgebraTransitionInClass_id
59 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
60 completedGroupAlgebraTransitionInClass G C (le_rfl : U ≤ U) = RingHom.id _ := by
61 rw [completedGroupAlgebraTransitionInClass, OpenNormalSubgroupInClass.map_id]
62 exact MonoidAlgebra.mapDomainRingHom_id
63 (R := ℤ) (M := CompletedGroupAlgebraQuotientInClass G C U)
65/-- Composition lemma completedGroupAlgebraTransitionInClass_comp. -/
66@[simp]
67theorem completedGroupAlgebraTransitionInClass_comp
68 (C : ProCGroups.FiniteGroupClass.{u})
69 {U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
70 (completedGroupAlgebraTransitionInClass G C hUV).comp
71 (completedGroupAlgebraTransitionInClass G C hVW) =
72 completedGroupAlgebraTransitionInClass G C (hUV.trans hVW) := by
73 rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraTransitionInClass,
74 completedGroupAlgebraTransitionInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
75 congr 1
76 exact OpenNormalSubgroupInClass.map_comp
77 (C := C) (G := G)
78 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)
79 hUV hVW
81/-- The class-restricted inverse system of finite-stage integral group rings. -/
82def completedGroupAlgebraSystemInClass
83 (C : ProCGroups.FiniteGroupClass.{u}) :
84 InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where
85 X := CompletedGroupAlgebraStageInClass G C
86 topologicalSpace := fun _ => ⊥
87 map := fun {U V} hUV => completedGroupAlgebraTransitionInClass G C hUV
88 continuous_map := by
89 intro U V hUV
90 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass G C U) := ⊥
91 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass G C V) := ⊥
92 letI : DiscreteTopology (CompletedGroupAlgebraStageInClass G C V) := ⟨rfl⟩
93 exact continuous_of_discreteTopology
94 map_id := by
95 intro U
96 funext x
97 exact congrFun
98 (congrArg DFunLike.coe
99 (completedGroupAlgebraTransitionInClass_id G C U)) x
100 map_comp := by
101 intro U V W hUV hVW
102 funext x
103 exact congrFun
104 (congrArg DFunLike.coe
105 (completedGroupAlgebraTransitionInClass_comp G C hUV hVW)) x
107/-- The quotient ring map from `ℤ[G]` to one class-restricted finite stage. -/
108def completedGroupAlgebraStageMapInClass
109 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
110 MonoidAlgebra ℤ G →+* CompletedGroupAlgebraStageInClass G C U :=
111 MonoidAlgebra.mapDomainRingHom ℤ
112 (openNormalSubgroupInClassProj (C := C) (G := G) U)
114/-- Evaluation formula for completedGroupAlgebraStageMapInClass_of. -/
115@[simp]
116theorem completedGroupAlgebraStageMapInClass_of
117 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
118 completedGroupAlgebraStageMapInClass G C U (MonoidAlgebra.of ℤ _ g) =
119 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1 := by
120 classical
121 simp only [completedGroupAlgebraStageMapInClass, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
122 OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
123 rfl
125/-- Compatibility lemma completedGroupAlgebraStageMapInClass_compatible. -/
126@[simp]
127theorem completedGroupAlgebraStageMapInClass_compatible
128 (C : ProCGroups.FiniteGroupClass.{u})
129 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
130 (completedGroupAlgebraTransitionInClass G C hUV).comp
131 (completedGroupAlgebraStageMapInClass G C V) =
132 completedGroupAlgebraStageMapInClass G C U := by
133 rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraStageMapInClass,
134 completedGroupAlgebraStageMapInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
135 congr 1
137/-- Compatibility for a class-restricted completed group algebra family. -/
139 (C : ProCGroups.FiniteGroupClass.{u})
140 (x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
141 CompletedGroupAlgebraStageInClass G C U) : Prop :=
142 (completedGroupAlgebraSystemInClass G C).Compatible x
144/-- The class-restricted completed group algebra as an inverse-limit subtype. -/
145abbrev CompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
146 {x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
147 CompletedGroupAlgebraStageInClass G C U //
150/-- Projection from the class-restricted completed group algebra to one finite stage. -/
151def completedGroupAlgebraProjectionInClass
152 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
153 CompletedGroupAlgebraInClass G C → CompletedGroupAlgebraStageInClass G C U :=
154 (completedGroupAlgebraSystemInClass G C).projection U
156section ComapInClass
158variable {G H : Type u}
159variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
160variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
162/-- Pull back a class-restricted finite quotient along a continuous homomorphism.
164The hereditary hypothesis is the precise extra closure property needed: the pulled-back quotient
165embeds into the target quotient, so membership in `C` follows from closure under subgroups. -/
166def completedGroupAlgebraComapIndexInClass
167 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
168 (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) :
169 CompletedGroupAlgebraIndexInClass G C := by
170 let V : OpenNormalSubgroup H := (OrderDual.ofDual U).1
171 let W : OpenNormalSubgroup G := OpenNormalSubgroup.comap ψ.toMonoidHom ψ.continuous_toFun V
172 refine OrderDual.toDual ⟨W, ?_⟩
173 let f : G ⧸ (W : Subgroup G) →* H ⧸ (V : Subgroup H) :=
174 QuotientGroup.map _ _ ψ.toMonoidHom (by
175 intro g hg
176 simpa [W] using hg)
177 have hf : Function.Injective f := by
178 intro x y hxy
179 rcases QuotientGroup.mk'_surjective (W : Subgroup G) x with ⟨a, rfl⟩
180 rcases QuotientGroup.mk'_surjective (W : Subgroup G) y with ⟨b, rfl⟩
181 apply QuotientGroup.eq.2
182 change ψ (a⁻¹ * b) ∈ (V : Subgroup H)
183 have hv : (ψ a)⁻¹ * ψ b ∈ (V : Subgroup H) := QuotientGroup.eq.1 hxy
184 simpa using hv
185 exact hC.of_injective (OrderDual.ofDual U).2 f hf
187/-- The finite quotient map induced by a continuous homomorphism after pulling back the stage. -/
188def completedGroupAlgebraComapQuotientMapInClass
189 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
190 (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) :
191 CompletedGroupAlgebraQuotientInClass G C
192 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U) →*
193 CompletedGroupAlgebraQuotientInClass H C U := by
194 let V : OpenNormalSubgroup H := (OrderDual.ofDual U).1
195 let W : OpenNormalSubgroup G := OpenNormalSubgroup.comap ψ.toMonoidHom ψ.continuous_toFun V
196 exact QuotientGroup.map _ _ ψ.toMonoidHom (by
197 intro g hg
198 simpa [W, completedGroupAlgebraComapIndexInClass] using hg)
200/-- Evaluation formula for completedGroupAlgebraComapQuotientMapInClass_mk. -/
201@[simp]
202theorem completedGroupAlgebraComapQuotientMapInClass_mk
203 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
204 (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) (g : G) :
205 completedGroupAlgebraComapQuotientMapInClass
206 (G := G) (H := H) C hC ψ U
207 (QuotientGroup.mk'
208 ((((OrderDual.ofDual
209 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U)).1 :
210 OpenNormalSubgroup G) : Subgroup G)) g) =
211 QuotientGroup.mk' ((((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H))
212 (ψ g) := rfl
214/-- Surjectivity lemma completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective. -/
215theorem completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
216 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
217 (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
218 (U : CompletedGroupAlgebraIndexInClass H C) :
219 Function.Surjective
220 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ U) := by
221 intro h
222 rcases QuotientGroup.mk'_surjective
223 ((((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)) h with ⟨a, rfl⟩
224 rcases hψ a with ⟨g, rfl⟩
225 refine ⟨QuotientGroup.mk'
226 ((((OrderDual.ofDual
227 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U)).1 :
228 OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
229 rw [completedGroupAlgebraComapQuotientMapInClass_mk]
231omit [IsTopologicalGroup G] in
232/-- 有限群クラスを固定した 標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
233theorem completedGroupAlgebraComapIndexInClass_mono
234 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
235 (ψ : ContinuousMonoidHom G H) {U V : CompletedGroupAlgebraIndexInClass H C}
236 (hUV : U ≤ V) :
237 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U ≤
238 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V := by
239 change
240 Subgroup.comap ψ.toMonoidHom
241 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H) ≤
242 Subgroup.comap ψ.toMonoidHom
243 (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)
244 exact Subgroup.comap_mono hUV
246/-- Compatibility lemma completedGroupAlgebraComapQuotientMapInClass_compatible. -/
247@[simp]
248theorem completedGroupAlgebraComapQuotientMapInClass_compatible
249 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
250 (ψ : ContinuousMonoidHom G H) {U V : CompletedGroupAlgebraIndexInClass H C}
251 (hUV : U ≤ V) :
252 (OpenNormalSubgroupInClass.map
253 (C := C) (G := H)
254 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV).comp
255 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ V) =
256 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ U).comp
257 (OpenNormalSubgroupInClass.map
258 (C := C) (G := G)
259 (U := OrderDual.ofDual
260 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U))
261 (V := OrderDual.ofDual
262 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V))
263 (completedGroupAlgebraComapIndexInClass_mono (G := G) (H := H) C hC ψ hUV)) := by
264 ext q
265 rcases QuotientGroup.mk'_surjective
266 ((((OrderDual.ofDual
267 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V)).1 :
268 OpenNormalSubgroup G) : Subgroup G)) q with ⟨g, rfl⟩
269 rfl
271/-- Pulling a finite quotient back along the identity continuous homomorphism gives the same
272class-restricted index. This is intentionally an equality theorem, since dependent inverse-limit
273indices are often not definitionally equal after target naturality rewrites. -/
274@[simp]
276 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
277 (U : CompletedGroupAlgebraIndexInClass G C) :
278 completedGroupAlgebraComapIndexInClass (G := G) (H := G) C hC
279 (ContinuousMonoidHom.id G) U = U := by
280 apply OrderDual.ofDual.injective
281 ext x
282 simp only [completedGroupAlgebraComapIndexInClass, ContinuousMonoidHom.coe_toMonoidHom,
283 OrderDual.ofDual_toDual, OpenNormalSubgroup.toSubgroup_comap, Subsemigroup.mem_carrier,
284 Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid, Subgroup.mem_comap, MonoidHom.coe_coe,
285 ContinuousMonoidHom.id_toFun, OpenSubgroup.mem_toSubgroup]
287omit [IsTopologicalGroup G] in
288/-- Pullback of class-restricted finite quotients is functorial for continuous target maps.
290This is the index-level rewrite needed when the two inverse-limit stage indices produced by a
291composite target map are propositionally, but not definitionally, the same. -/
292@[simp]
294 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
295 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
296 (φ : G →ₜ* H) (ψ : H →ₜ* K) (U : CompletedGroupAlgebraIndexInClass K C) :
297 completedGroupAlgebraComapIndexInClass (G := G) (H := K) C hC (ψ.comp φ) U =
298 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC φ
299 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC ψ U) := by
300 apply OrderDual.ofDual.injective
301 ext x
302 simp only [completedGroupAlgebraComapIndexInClass, ContinuousMonoidHom.coe_toMonoidHom,
303 OrderDual.ofDual_toDual, OpenNormalSubgroup.toSubgroup_comap, Subsemigroup.mem_carrier,
304 Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid, Subgroup.mem_comap, MonoidHom.coe_coe,
305 ContinuousMonoidHom.comp_toFun, OpenSubgroup.mem_toSubgroup]
307omit [IsTopologicalGroup G] in
308/-- Pulling back the canonical trivial quotient gives the canonical trivial quotient. -/
309@[simp]
311 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
313 (ψ : G →ₜ* H) :
314 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ
315 (OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := H))) =
316 OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := G)) := by
317 apply OrderDual.ofDual.injective
318 ext x
319 simp only [completedGroupAlgebraComapIndexInClass, ContinuousMonoidHom.coe_toMonoidHom,
320 OrderDual.ofDual_toDual, OpenNormalSubgroup.toSubgroup_comap, Subsemigroup.mem_carrier,
321 Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid, Subgroup.mem_comap, MonoidHom.coe_coe,
322 OpenSubgroup.mem_toSubgroup]
323 constructor <;> intro _ <;> trivial
325end ComapInClass
327end
329end FoxDifferential