FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Basic.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation
2import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.Coeff
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Basic.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
19noncomputable section
21open ProCGroups.InverseSystems
22open ProCGroups.ProC
24universe u
26variable (ℓ : ℕ) [Fact (0 < ℓ)]
27variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29omit [Fact (0 < ℓ)] in
30/-- The class-restricted prime-power stage at index `(a, U)`, namely `(ZMod (ℓ^a))[G/U]`. -/
32 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
33 Type _ :=
34 ModNCompletedGroupAlgebraStageInClass (ℓ ^ i.1) G C i.2
36/-- 素冪係数で定めた 有限群クラスを固定した 標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
38 (C : ProCGroups.FiniteGroupClass.{u})
39 (hFinite : ∀ {Q : Type u} [Group Q], C Q → Finite Q)
40 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
41 Finite (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) := by
42 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
44 (n := ℓ ^ i.1) (G := G) C hFinite i.2
46omit [Fact (0 < ℓ)] in
47/-- The combined transition map for class-restricted prime-power stage calculus. -/
49 (C : ProCGroups.FiniteGroupClass.{u})
50 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
51 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j →+*
52 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i := by
53 exact
55 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
56 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
57 (modNCompletedGroupAlgebraTransitionInClass (n := ℓ ^ j.1) (G := G) C hij.2)
59omit [Fact (0 < ℓ)] in
60/-- Evaluation formula for primePowerCompletedGroupAlgebraTransitionInClass_of. -/
61@[simp]
63 (C : ProCGroups.FiniteGroupClass.{u})
64 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j)
65 (q : CompletedGroupAlgebraQuotientInClass G C j.2) :
66 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
67 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1)) _ q) =
68 MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
69 ((OpenNormalSubgroupInClass.map
70 (C := C) (G := G)
71 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) := by
72 rw [primePowerCompletedGroupAlgebraTransitionInClass, RingHom.comp_apply,
74 simpa using
76 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
77 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
78 ((OpenNormalSubgroupInClass.map
79 (C := C) (G := G)
80 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q))
82omit [Fact (0 < ℓ)] in
83/-- 素冪係数で定めた 有限群クラスを固定した 遷移写像が群環の単項基底元を有限商段階の対応する単項基底元へ送ることを述べる。 -/
84@[simp]
86 (C : ProCGroups.FiniteGroupClass.{u})
87 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j)
88 (q : CompletedGroupAlgebraQuotientInClass G C j.2)
89 (a : ModNCompletedCoeff (ℓ ^ j.1)) :
90 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
91 (MonoidAlgebra.single q a) =
92 MonoidAlgebra.single
93 ((OpenNormalSubgroupInClass.map
94 (C := C) (G := G)
95 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
97 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
98 (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) := by
99 rw [primePowerCompletedGroupAlgebraTransitionInClass, RingHom.comp_apply,
103omit [Fact (0 < ℓ)] in
104/-- 素冪係数で定めた 有限群クラスを固定した 遷移写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
105@[simp]
107 (C : ProCGroups.FiniteGroupClass.{u})
108 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
109 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij =
111 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
112 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
113 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hij.2) := by
114 rfl
116omit [Fact (0 < ℓ)] in
117/-- 有限群クラスを固定した素冪係数段階で、遷移写像の値を商写像の代表元計算として記述する。 -/
119 (C : ProCGroups.FiniteGroupClass.{u})
120 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
121 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij =
122 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ i.1) G C hij.2).comp
124 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C j.2
125 (primePow_dvd_primePow (ℓ := ℓ) hij.1)) := by
128 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C
129 (U := i.2) (V := j.2) hij.2
130 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
132omit [Fact (0 < ℓ)] in
133/-- Identity case for primePowerCompletedGroupAlgebraTransitionInClass_id. -/
134@[simp]
136 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
137 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C
138 (le_rfl : i ≤ i) =
139 RingHom.id _ := by
143 simp only [RingHomCompTriple.comp_eq]
145omit [Fact (0 < ℓ)] in
146/-- Composition lemma primePowerCompletedGroupAlgebraTransitionInClass_comp. -/
147@[simp 900]
149 (C : ProCGroups.FiniteGroupClass.{u})
150 {i j k : PrimePowerCompletedGroupAlgebraIndexInClass G C}
151 (hij : i ≤ j) (hjk : j ≤ k) :
152 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij).comp
153 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hjk) =
154 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C
155 (hij.trans hjk) := by
156 calc
157 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij).comp
158 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hjk)
159 =
161 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
162 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
163 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hij.2)).comp
164 ((modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hjk.2).comp
166 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
167 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
170 _ =
172 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
173 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
174 (((modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hij.2).comp
175 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hjk.2)).comp
177 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
178 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
179 apply RingHom.ext
180 intro x
181 rfl
182 _ =
184 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
185 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
186 ((modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C
187 (hij.2.trans hjk.2)).comp
189 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
190 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
192 _ =
194 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
195 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
196 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C
197 (hij.2.trans hjk.2))).comp
199 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
200 (primePow_dvd_primePow (ℓ := ℓ) hjk.1)) := by
201 rw [← RingHom.comp_assoc]
202 _ =
203 ((modNCompletedGroupAlgebraTransitionInClass (ℓ ^ i.1) G C
204 (hij.2.trans hjk.2)).comp
206 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C k.2
207 (primePow_dvd_primePow (ℓ := ℓ) hij.1))).comp
209 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
210 (primePow_dvd_primePow (ℓ := ℓ) hjk.1)) := by
212 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C
213 (U := i.2) (V := k.2) (hUV := hij.2.trans hjk.2)
214 (hnm := primePow_dvd_primePow (ℓ := ℓ) hij.1)]
215 _ =
216 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ i.1) G C
217 (hij.2.trans hjk.2)).comp
219 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C k.2
220 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
222 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
223 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
224 rw [RingHom.comp_assoc]
225 _ =
226 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ i.1) G C
227 (hij.2.trans hjk.2)).comp
229 (n := ℓ ^ i.1) (m := ℓ ^ k.1) (G := G) C k.2
230 (primePow_dvd_primePow (ℓ := ℓ) (hij.trans hjk).1)) := by
232 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (k := ℓ ^ k.1) (G := G) C
233 (U := k.2)
234 (hnm := primePow_dvd_primePow (ℓ := ℓ) hij.1)
235 (hmk := primePow_dvd_primePow (ℓ := ℓ) hjk.1)]
236 _ =
237 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C
238 (hij.trans hjk) := by
240 (ℓ := ℓ) (G := G) C (hij := hij.trans hjk)]
242omit [Fact (0 < ℓ)] in
243/-- Composition lemma primePowerCompletedGroupAlgebraStageAugmentationInClass_comp_transition. -/
244@[simp]
246 (C : ProCGroups.FiniteGroupClass.{u})
247 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
248 (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2).comp
249 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij) =
251 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
252 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
253 (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ j.1) G C j.2) := by
255 rw [← RingHom.comp_assoc]
257 rw [RingHom.comp_assoc]
260omit [Fact (0 < ℓ)] in
261/-- The class-restricted inverse system indexed by prime powers and `C`-quotients. -/
263 (C : ProCGroups.FiniteGroupClass.{u}) :
264 InverseSystem (I := PrimePowerCompletedGroupAlgebraIndexInClass G C) where
265 X := PrimePowerCompletedGroupAlgebraStageInClass ℓ G C
266 topologicalSpace := fun _ => ⊥
267 map := fun {i j} hij =>
268 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
269 continuous_map := by
270 intro i j hij
271 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) := ⊥
272 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) := ⊥
273 letI : DiscreteTopology (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) := ⟨rfl⟩
274 exact continuous_of_discreteTopology
275 map_id := by
276 intro i
277 funext x
278 exact congrFun
279 (congrArg DFunLike.coe
281 (ℓ := ℓ) (G := G) C i)) x
282 map_comp := by
283 intro i j k hij hjk
284 funext x
285 exact congrFun
286 (congrArg DFunLike.coe
288 (ℓ := ℓ) (G := G) C hij hjk)) x
290omit [IsTopologicalGroup G] in
291/-- The class-restricted prime-power group-algebra index family is directed under componentwise
292order when `C` is a formation. -/
294 (C : ProCGroups.FiniteGroupClass.{u}) (hForm : ProCGroups.FiniteGroupClass.Formation C) :
295 Directed (· ≤ ·) (id : PrimePowerCompletedGroupAlgebraIndexInClass G C →
296 PrimePowerCompletedGroupAlgebraIndexInClass G C) := by
297 intro i j
299 (C := C) (G := G) hForm i.2 j.2 with
300 ⟨U, hiU, hjU⟩
301 refine ⟨(max i.1 j.1, U), ?_, ?_⟩
302 · exact ⟨le_max_left _ _, hiU⟩
303 · exact ⟨le_max_right _ _, hjU⟩
305omit [Fact (0 < ℓ)] in
306/-- Every transition in the class-restricted prime-power completed group-algebra system is
307surjective. -/
309 (C : ProCGroups.FiniteGroupClass.{u})
310 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
311 Function.Surjective
312 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij) := by
313 intro x
315 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
316 (primePow_dvd_primePow (ℓ := ℓ) hij.1) x with
317 ⟨y, hy⟩
319 (n := ℓ ^ j.1) (G := G) C hij.2 y with
320 ⟨z, hz⟩
321 refine ⟨z, ?_⟩
322 rw [primePowerCompletedGroupAlgebraTransitionInClass_eq, RingHom.comp_apply, hz, hy]
324omit [Fact (0 < ℓ)] in
325/-- Compatibility for a class-restricted prime-power completed group algebra family. -/
327 (C : ProCGroups.FiniteGroupClass.{u})
328 (x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
329 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) : Prop :=
332omit [Fact (0 < ℓ)] in
333/-- The class-restricted prime-power completed group algebra as an inverse-limit subtype.
335The all-finite `PrimePowerCompletedGroupAlgebra` below remains the ringed concrete API; this type
336is the class-indexed completed object that later Fox layers should target. -/
337abbrev PrimePowerCompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
338 {x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
339 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i //
340 PrimePowerCompletedGroupAlgebraCompatibleInClass (ℓ := ℓ) (G := G) C x}
342omit [Fact (0 < ℓ)] in
343/-- Projection from the class-restricted completed group algebra to a prime-power stage. -/
345 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
347 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i :=
348 (primePowerCompletedGroupAlgebraSystemInClass ℓ G C).projection i
350/-- Every finite-stage projection from the class-restricted prime-power completed group algebra is
353 (C : ProCGroups.FiniteGroupClass.{u})
354 (hForm : ProCGroups.FiniteGroupClass.Formation C)
355 (hFinite : ∀ {Q : Type u} [Group Q], C Q → Finite Q)
356 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
357 Function.Surjective
358 (primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i) := by
359 let S := primePowerCompletedGroupAlgebraSystemInClass ℓ G C
360 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C, TopologicalSpace (S.X i) :=
361 fun i => S.topologicalSpace i
362 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C, DiscreteTopology (S.X i) :=
363 fun _ => ⟨rfl⟩
364 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C, CompactSpace (S.X i) :=
365 fun i => by
366 letI : Finite (S.X i) := by
367 dsimp [S, primePowerCompletedGroupAlgebraSystemInClass]
369 (ℓ := ℓ) (G := G) C hFinite i
370 letI : Fintype (S.X i) := Fintype.ofFinite _
371 infer_instance
372 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C, T2Space (S.X i) :=
373 fun _ => inferInstance
374 change Function.Surjective (S.projection i)
375 exact
376 S.surjective_π
377 (directed_primePowerCompletedGroupAlgebraIndexInClass (G := G) C hForm)
378 (fun {i j} hij =>
379 primePowerCompletedGroupAlgebraTransitionInClass_surjective (ℓ := ℓ) (G := G) C hij)
380 i
382end
384end FoxDifferential