FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Augmentation.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Augmentation.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
25variable (ℓ : ℕ) [Fact (0 < ℓ)]
26variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28/-- The prime-power completed group algebra carries a canonical augmentation to the corresponding
29coefficient inverse limit. -/
31 PrimePowerCompletedGroupAlgebra ℓ G → PrimePowerCompletedCoeff ℓ G := by
32 intro x
33 refine ⟨fun i => ?_, ?_⟩
34 · letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
35 exact modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2 (x.1 i)
36 · intro i j hij
37 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
38 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
39 calc
41 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
42 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
43 (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ j.1) G j.2 (x.1 j))
44 =
45 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
46 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij (x.1 j)) := by
47 symm
48 exact congrFun
49 (congrArg DFunLike.coe
51 (ℓ := ℓ) (G := G) hij)) (x.1 j)
52 _ =
53 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2 (x.1 i) := by
54 have hx :
55 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij (x.1 j) = x.1 i :=
56 x.2 i j hij
57 exact congrArg (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2) hx
59omit [Fact (0 < ℓ)] in
60/-- 素冪係数で定めた 有限段階射影が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
61@[simp]
64 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
65 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
66 (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x) =
67 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
68 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x) := rfl
70omit [Fact (0 < ℓ)] in
71/-- Stagewise augmentations of a completed group-algebra element are independent of the
74 (a : ℕ) (U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
75 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
76 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ a) G U
77 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) (a, U) x) =
78 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ a) G V
79 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) (a, V) x) := by
80 simpa [primePowerCompletedCoeffProjection_augmentation] using
82 (ℓ := ℓ) (G := G) a U V
83 (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x)
85end
87end FoxDifferential