FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/Augmentation.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/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 class-restricted coefficient inverse system `i = (a, U) ↦ ZMod (ℓ^a)`. -/
30 (C : ProCGroups.FiniteGroupClass.{u}) :
31 InverseSystem (I := PrimePowerCompletedGroupAlgebraIndexInClass G C) where
32 X := fun i => ModNCompletedCoeff (ℓ ^ i.1)
33 topologicalSpace := fun _ => ⊥
34 map := fun {i j} hij =>
35 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
36 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
38 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
39 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
40 continuous_map := by
41 intro i j hij
42 letI : TopologicalSpace (ModNCompletedCoeff (ℓ ^ i.1)) := ⊥
43 letI : TopologicalSpace (ModNCompletedCoeff (ℓ ^ j.1)) := ⊥
44 letI : DiscreteTopology (ModNCompletedCoeff (ℓ ^ j.1)) := ⟨rfl⟩
45 exact continuous_of_discreteTopology
46 map_id := by
47 intro i
48 funext x
49 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
50 exact congrFun
51 (congrArg DFunLike.coe
52 (modNCompletedCoeffMap_rfl (n := ℓ ^ i.1))) x
53 map_comp := by
54 intro i j k hij hjk
55 funext x
56 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
57 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
58 letI : Fact (0 < ℓ ^ k.1) := ⟨primePower_pos ℓ k.1⟩
59 exact congrFun
60 (congrArg DFunLike.coe
62 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (k := ℓ ^ k.1)
63 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
64 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) x
66/-- Compatibility for the coefficient tower indexed by a finite quotient class. The finite
67quotient component is retained so the augmentation target has the same pro-`C` index shape as the
68class-restricted completed group algebra. -/
70 (C : ProCGroups.FiniteGroupClass.{u})
71 (x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
72 ModNCompletedCoeff (ℓ ^ i.1)) : Prop :=
75/-- The pro-`C`-indexed coefficient inverse limit attached to the class-restricted
76prime-power completed group algebra. -/
77abbrev PrimePowerCompletedCoeffInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
78 {x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
79 ModNCompletedCoeff (ℓ ^ i.1) //
80 PrimePowerCompletedCoeffCompatibleInClass (ℓ := ℓ) (G := G) C x}
82/-- Projection from the pro-`C`-indexed coefficient limit to one finite stage. -/
84 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
85 PrimePowerCompletedCoeffInClass ℓ G C → ModNCompletedCoeff (ℓ ^ i.1) :=
86 (primePowerCompletedCoeffSystemInClass ℓ G C).projection i
89 (C : ProCGroups.FiniteGroupClass.{u}) :
90 Zero (PrimePowerCompletedCoeffInClass ℓ G C) where
93 intro i j hij
94 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
95 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
98 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
99 (primePow_dvd_primePow (ℓ := ℓ) hij.1))⟩
102 (C : ProCGroups.FiniteGroupClass.{u}) :
103 Add (PrimePowerCompletedCoeffInClass ℓ G C) where
105 (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i), by
107 intro i j hij
108 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
109 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
110 change modNCompletedCoeffMap
111 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
112 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
113 ((show ZMod (ℓ ^ j.1) from x.1 j) + (show ZMod (ℓ ^ j.1) from y.1 j)) =
114 (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i)
116 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
119 (C : ProCGroups.FiniteGroupClass.{u}) :
120 Neg (PrimePowerCompletedCoeffInClass ℓ G C) where
123 intro i j hij
124 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
125 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
126 change modNCompletedCoeffMap
127 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
128 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
129 (-(show ZMod (ℓ ^ j.1) from x.1 j)) =
130 -(show ZMod (ℓ ^ i.1) from x.1 i)
131 rw [map_neg]
132 exact congrArg Neg.neg (x.2 i j hij)⟩
135 (C : ProCGroups.FiniteGroupClass.{u}) :
136 Sub (PrimePowerCompletedCoeffInClass ℓ G C) where
138 (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i), by
140 intro i j hij
141 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
142 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
143 change modNCompletedCoeffMap
144 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
145 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
146 ((show ZMod (ℓ ^ j.1) from x.1 j) - (show ZMod (ℓ ^ j.1) from y.1 j)) =
147 (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i)
148 rw [map_sub]
149 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
151omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
152/-- 素冪係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は零元を零元へ送る。 -/
153@[simp]
155 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
156 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i
157 (0 : PrimePowerCompletedCoeffInClass ℓ G C) = 0 := by
158 rfl
160omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
161/-- 素冪係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は和を和へ送る。 -/
162@[simp]
164 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
165 (x y : PrimePowerCompletedCoeffInClass ℓ G C) :
166 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (x + y) =
167 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i x +
168 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i y := by
169 rfl
171omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
172/-- 素冪係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は負元を負元へ送る。 -/
173@[simp]
175 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
176 (x : PrimePowerCompletedCoeffInClass ℓ G C) :
177 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (-x) =
178 -primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i x := by
179 rfl
181omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
182/-- 素冪係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は差を差へ送る。 -/
183@[simp]
185 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
186 (x y : PrimePowerCompletedCoeffInClass ℓ G C) :
187 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (x - y) =
188 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i x -
189 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i y := by
190 rfl
192/-- The class-restricted prime-power completed group algebra carries a canonical augmentation to
193the pro-`C`-indexed coefficient limit. -/
195 (C : ProCGroups.FiniteGroupClass.{u}) :
197 PrimePowerCompletedCoeffInClass ℓ G C := by
198 intro x
199 refine ⟨fun i => ?_, ?_⟩
200 · letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
201 exact modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2 (x.1 i)
202 · dsimp [PrimePowerCompletedCoeffCompatibleInClass]
203 intro i j hij
204 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
205 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
206 calc
208 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
209 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
210 (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ j.1) G C j.2 (x.1 j))
211 =
212 modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2
213 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij (x.1 j)) := by
214 symm
215 exact congrFun
216 (congrArg DFunLike.coe
218 (ℓ := ℓ) (G := G) C hij)) (x.1 j)
219 _ =
220 modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2 (x.1 i) := by
221 have hx :
222 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
223 (x.1 j) = x.1 i :=
224 x.2 i j hij
225 exact congrArg
226 (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2) hx
228omit [Fact (0 < ℓ)] in
229/-- 素冪係数で定めた 有限群クラスを固定した 有限段階射影が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
230@[simp]
232 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
233 (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
234 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i
235 (primePowerCompletedGroupAlgebraAugmentationInClass (ℓ := ℓ) (G := G) C x) =
236 modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2
237 (primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x) := rfl
239omit [Fact (0 < ℓ)] in
240/-- The class-indexed completed group-algebra augmentation has a canonical section, obtained by
241placing each compatible coefficient system on the identity monomial at every finite stage. -/
243 (C : ProCGroups.FiniteGroupClass.{u}) :
244 Function.Surjective
245 (primePowerCompletedGroupAlgebraAugmentationInClass (ℓ := ℓ) (G := G) C) := by
246 intro x
247 refine ⟨⟨fun i => ?_, ?_⟩, ?_⟩
248 · exact MonoidAlgebra.single
249 (1 : CompletedGroupAlgebraQuotientInClass G C i.2) (x.1 i)
250 · intro i j hij
251 change
252 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
253 (MonoidAlgebra.single
254 (1 : CompletedGroupAlgebraQuotientInClass G C j.2) (x.1 j)) =
255 MonoidAlgebra.single
256 (1 : CompletedGroupAlgebraQuotientInClass G C i.2) (x.1 i)
258 have hxcoeff :
260 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
261 (primePow_dvd_primePow (ℓ := ℓ) hij.1) (x.1 j) = x.1 i := by
262 simpa [primePowerCompletedCoeffSystemInClass] using x.2 i j hij
263 simpa using congrArg
264 (fun a : ModNCompletedCoeff (ℓ ^ i.1) =>
265 MonoidAlgebra.single
266 (1 : CompletedGroupAlgebraQuotientInClass G C i.2) a)
267 hxcoeff
268 · apply Subtype.ext
269 funext i
270 change
271 modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2
272 (MonoidAlgebra.single
273 (1 : CompletedGroupAlgebraQuotientInClass G C i.2) (x.1 i)) =
274 x.1 i
278end
280end FoxDifferential