FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/Augmentation.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/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
26variable (n : ℕ) [Fact (0 < n)]
27variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29/-- The augmentation on one residue-coefficient finite stage. -/
30def modNCompletedGroupAlgebraStageAugmentation (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
31 ModNCompletedGroupAlgebraStage n G U →+* ModNCompletedCoeff n :=
32 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
33 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)
34 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →* ModNCompletedCoeff n)
36omit [Fact (0 < n)] in
37/-- Evaluation formula for modNCompletedGroupAlgebraStageAugmentation_of. -/
38@[simp]
40 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) :
42 (MonoidAlgebra.of (ModNCompletedCoeff n) _ q) = 1 := by
43 classical
44 simp only [modNCompletedGroupAlgebraStageAugmentation, MonoidAlgebra.of, MonoidAlgebra.single,
45 MonoidHom.coe_mk, OneHom.coe_mk, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul,
46 mul_one]
48omit [Fact (0 < n)] in
49/-- Compatibility lemma modNCompletedGroupAlgebraStageAugmentation_compatible. -/
50@[simp 900]
52 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
53 (modNCompletedGroupAlgebraStageAugmentation n G U).comp
54 (modNCompletedGroupAlgebraTransition n G hUV) =
55 modNCompletedGroupAlgebraStageAugmentation n G V := by
56 apply RingHom.ext
57 intro x
58 refine MonoidAlgebra.induction_on
59 (p := fun x =>
60 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
61 (modNCompletedGroupAlgebraTransition n G hUV)) x =
63 x ?_ ?_ ?_
64 · intro q
65 rw [RingHom.comp_apply, modNCompletedGroupAlgebraTransition_of]
66 simp only [modNCompletedGroupAlgebraStageAugmentation, MonoidAlgebra.single, RingHom.coe_coe,
67 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one, MonoidAlgebra.of, MonoidHom.coe_mk,
68 OneHom.coe_mk]
69 · intro x y hx hy
70 simp only [RingHom.map_add, hx, hy]
71 · intro a x hx
72 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
73 have hcoeff :
74 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
75 (modNCompletedGroupAlgebraTransition n G hUV))
76 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupAlgebraStage n G V) a) =
78 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupAlgebraStage n G V) a) := by
80 MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
81 RingHom.comp_apply, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one, RingHom.coe_coe,
82 MonoidAlgebra.lift_single, smul_eq_mul, mul_one]
83 rw [hcoeff]
85omit [Fact (0 < n)] in
86/-- Composition lemma modNCompletedGroupAlgebraStageAugmentation_comp_stageMap. -/
87@[simp 900]
89 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
90 (modNCompletedGroupAlgebraStageAugmentation n G U).comp
91 (modNCompletedGroupAlgebraStageMap n G U) =
92 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
93 (1 : G →* ModNCompletedCoeff n) := by
94 apply RingHom.ext
95 intro x
96 refine MonoidAlgebra.induction_on
97 (p := fun x =>
98 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
99 (modNCompletedGroupAlgebraStageMap n G U)) x =
100 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
101 (1 : G →* ModNCompletedCoeff n)) x)
102 x ?_ ?_ ?_
103 · intro g
104 rw [RingHom.comp_apply, modNCompletedGroupAlgebraStageMap_of]
105 simp only [modNCompletedGroupAlgebraStageAugmentation, MonoidAlgebra.of_apply,
106 RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul,
107 mul_one]
108 · intro x y hx hy
110 · intro a x hx
111 have hcoeff :
112 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
113 (modNCompletedGroupAlgebraStageMap n G U))
114 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) = a := by
116 MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
117 RingHom.comp_apply, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one, RingHom.coe_coe,
118 MonoidAlgebra.lift_single, smul_eq_mul, mul_one]
119 have hcoeff' :
120 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
121 (modNCompletedGroupAlgebraStageMap n G U))
122 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) =
123 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
124 (1 : G →* ModNCompletedCoeff n))
125 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) := by
126 rw [hcoeff]
127 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
128 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]
129 rw [Algebra.smul_def]
130 calc
131 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
132 (modNCompletedGroupAlgebraStageMap n G U))
133 ((algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) * x)
134 =
135 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
136 (modNCompletedGroupAlgebraStageMap n G U))
137 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) *
138 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
139 (modNCompletedGroupAlgebraStageMap n G U)) x := by
140 rw [RingHom.map_mul]
141 _ =
142 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
143 (modNCompletedGroupAlgebraStageMap n G U))
144 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) *
145 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
146 (1 : G →* ModNCompletedCoeff n)) x := by
147 rw [hx]
148 _ =
149 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
150 (1 : G →* ModNCompletedCoeff n))
151 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) *
152 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
153 (1 : G →* ModNCompletedCoeff n)) x := by
154 rw [hcoeff']
155 _ =
156 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
157 (1 : G →* ModNCompletedCoeff n))
158 ((algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) * x) := by
159 exact
161 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
162 (1 : G →* ModNCompletedCoeff n))
163 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) x).symm
165/-- The augmentation value of a residue-coefficient completed point, read at one finite stage. -/
166def modNCompletedGroupAlgebraAugmentationAt (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
167 ModNCompletedGroupAlgebra n G → ModNCompletedCoeff n :=
168 fun x => modNCompletedGroupAlgebraStageAugmentation n G U
169 (modNCompletedGroupAlgebraProjection n G U x)
171omit [Fact (0 < n)] in
172/-- 法 n 係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
173@[simp 900]
175 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (x : ModNCompletedGroupAlgebra n G) :
176 modNCompletedGroupAlgebraAugmentationAt n G U x =
177 modNCompletedGroupAlgebraAugmentationAt n G V x := by
179 have hcomp := congrFun
180 (congrArg DFunLike.coe
182 (n := n) (G := G) (U := U) (V := V) hUV))
183 (modNCompletedGroupAlgebraProjection n G V x)
184 calc
186 (modNCompletedGroupAlgebraProjection n G U x)
187 =
189 (modNCompletedGroupAlgebraTransition n G hUV
190 (modNCompletedGroupAlgebraProjection n G V x)) := by
191 simpa [modNCompletedGroupAlgebraProjection] using
192 congrArg (modNCompletedGroupAlgebraStageAugmentation n G U)
193 ((modNCompletedGroupAlgebraSystem n G).projection_compatible x U V hUV).symm
195 (modNCompletedGroupAlgebraProjection n G V x) := by
196 exact hcomp
198/-- The canonical augmentation on the residue-coefficient completed group algebra. -/
200 ModNCompletedGroupAlgebra n G → ModNCompletedCoeff n :=
201 modNCompletedGroupAlgebraAugmentationAt n G (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)
203omit [Fact (0 < n)] in
204/-- 法 n 係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
205@[simp]
207 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (x : ModNCompletedGroupAlgebra n G) :
209 modNCompletedGroupAlgebraAugmentationAt n G U x := by
211 (n := n) (G := G)
212 (U := _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) (V := U)
213 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex_le (G := G) U) x
215omit [Fact (0 < n)] in
216/-- 法 n 係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
217@[simp]
219 (x : ModNCompletedGroupRing n G) :
221 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
222 (1 : G →* ModNCompletedCoeff n) x := by
225 exact congrFun
226 (congrArg DFunLike.coe
228 (n := n) (G := G) (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)))
229 x
231end
233end FoxDifferential