FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/System/CompletionMap.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.AddCommGroup
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/System/CompletionMap.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 coefficient algebras
14Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups.InverseSystems
21open ProCGroups.ProC
23universe u
26variable (n : ℕ) [Fact (0 < n)]
27variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29omit [Fact (0 < n)] in
30/-- Compatibility lemma modNCompletedGroupAlgebraStageMap_compatibleMaps. -/
33 (fun U => modNCompletedGroupAlgebraStageMap n G U) := by
34 intro U V hUV
35 funext x
36 exact congrFun
37 (congrArg DFunLike.coe
38 (modNCompletedGroupAlgebraStageMap_compatible (n := n) (G := G) (U := U) (V := V) hUV))
39 x
41/-- The canonical map `(ZMod n)[G] → lim_U (ZMod n)[G/U]`. -/
43 ModNCompletedGroupRing n G → ModNCompletedGroupAlgebra n G := by
44 letI : TopologicalSpace (ModNCompletedGroupRing n G) := ⊥
45 exact
47 (fun U => modNCompletedGroupAlgebraStageMap n G U)
48 (modNCompletedGroupAlgebraStageMap_compatibleMaps (n := n) (G := G))
50omit [Fact (0 < n)] in
51/-- 法 n 係数で定めた 有限段階射影が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
52@[simp]
54 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (x : ModNCompletedGroupRing n G) :
55 modNCompletedGroupAlgebraProjection n G U (toModNCompletedGroupAlgebra n G x) =
56 modNCompletedGroupAlgebraStageMap n G U x := by
57 rfl
59end
61end FoxDifferential