FoxDifferential/Completed/CoefficientRings/AugmentationIdealPrimePower/Augmentation.lean
1import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.LimitEquiv
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/AugmentationIdealPrimePower/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
22universe u
25variable (ℓ : ℕ) [Fact (0 < ℓ)]
26variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28omit [Fact (0 < ℓ)] in
29/-- Composition lemma primePowerCompletedGroupAlgebraAugmentation_comp_coeffToGroupAlgebra. -/
30@[simp]
32 (x : PrimePowerCompletedCoeff ℓ G) :
33 primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)
34 (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) x) = x := by
35 apply (primePowerCompletedCoeffSystem ℓ G).ext
36 intro i
37 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
38 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
39 (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) x)) = x.1 i
40 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
41 (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i) (x.1 i)) = x.1 i
42 exact primePowerCompletedGroupAlgebraStageAugmentation_algebraMap (ℓ := ℓ) (G := G) i (x.1 i)
44/-- The canonical prime-power augmentation as an additive homomorphism. -/
46 PrimePowerCompletedGroupAlgebra ℓ G →+ PrimePowerCompletedCoeff ℓ G where
47 toFun := primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)
48 map_zero' := by
49 apply (primePowerCompletedCoeffSystem ℓ G).ext
50 intro i
51 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
52 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i 0) = 0
55 (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)
56 map_add' x y := by
57 apply (primePowerCompletedCoeffSystem ℓ G).ext
58 intro i
59 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
60 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x + y)) =
61 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
62 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x) +
63 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
64 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i y)
67 (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)
68 _ _
70/-- Definition of primePowerCompletedGroupAlgebraAugmentationRingHom. -/
72 PrimePowerCompletedGroupAlgebra ℓ G →+* PrimePowerCompletedCoeff ℓ G where
73 toFun := primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)
74 map_one' := by
75 apply (primePowerCompletedCoeffSystem ℓ G).ext
76 intro i
77 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
78 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i 1) =
79 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i 1
82 exact map_one (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)
83 map_mul' := by
84 intro x y
85 apply (primePowerCompletedCoeffSystem ℓ G).ext
86 intro i
87 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
88 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x * y)) =
89 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
90 (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x *
91 primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) y)
94 exact map_mul (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)
95 _ _
96 map_zero' := by
97 exact map_zero (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))
98 map_add' := by
99 intro x y
100 exact map_add (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) x y
103 Ideal (PrimePowerCompletedGroupAlgebra ℓ G) :=
104 RingHom.ker (primePowerCompletedGroupAlgebraAugmentationRingHom (ℓ := ℓ) (G := G))
106variable {ℓ G} in
107omit [Fact (0 < ℓ)] in
108/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が所属条件を対応する augmentation または射影の消滅条件として特徴づけることを述べる。 -/
109@[simp]
111 {x : PrimePowerCompletedGroupAlgebra ℓ G} :
112 x ∈ primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal (ℓ := ℓ) (G := G) ↔
113 primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x =
114 (0 : PrimePowerCompletedCoeff ℓ G) := by
115 rw [primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal, RingHom.mem_ker]
116 rfl
118variable {ℓ G} in
119omit [Fact (0 < ℓ)] in
120/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
122 {x : PrimePowerCompletedGroupAlgebra ℓ G} :
123 x ∈ primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal (ℓ := ℓ) (G := G) ↔
124 ∀ i : PrimePowerCompletedGroupAlgebraIndex G,
125 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
126 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x) = 0 := by
129 rfl
131/-- The additive kernel of the prime-power augmentation. -/
133 AddSubgroup (PrimePowerCompletedGroupAlgebra ℓ G) :=
134 { carrier := {x |
135 primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G) x = 0}
136 zero_mem' := by
137 exact map_zero (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))
138 add_mem' := by
139 intro x y hx hy
140 change primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G) (x + y) = 0
142 simp only [add_zero]
143 neg_mem' := by
144 intro x hx
145 change primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G) (-x) = 0
146 rw [map_neg, hx]
147 simp only [neg_zero]}
149omit [Fact (0 < ℓ)] in
150/-- Surjectivity lemma primePowerCompletedGroupAlgebraAugmentation_surjective. -/
152 Function.Surjective (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)) := by
153 intro x
154 refine ⟨primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) x, ?_⟩
156 (ℓ := ℓ) (G := G) x
158omit [Fact (0 < ℓ)] in
159/-- Surjectivity lemma primePowerCompletedGroupAlgebraAugmentationAddHom_surjective. -/
161 Function.Surjective (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) := by
162 simpa [primePowerCompletedGroupAlgebraAugmentationAddHom] using
163 primePowerCompletedGroupAlgebraAugmentation_surjective (ℓ := ℓ) (G := G)
165omit [Fact (0 < ℓ)] in
166/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
168 Function.Exact
169 (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype
170 (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) := by
171 intro x
172 constructor
173 · intro hx
174 exact ⟨⟨x, hx⟩, rfl⟩
175 · rintro ⟨y, rfl⟩
176 exact y.2
178omit [Fact (0 < ℓ)] in
179/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が標準包含または係数写像が単射であることを述べる。 -/
181 Function.Injective
182 (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype := by
183 intro x y hxy
184 exact Subtype.ext hxy
186omit [Fact (0 < ℓ)] in
187/-- Injectivity, kernel identification, and surjectivity for the additive prime-power
188augmentation map. -/
190 Function.Injective
191 (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype ∧
192 Function.Exact
193 (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype
194 (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) ∧
195 Function.Surjective
196 (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) := by
198 (ℓ := ℓ) (G := G), ?_, ?_⟩
200 (ℓ := ℓ) (G := G)
201 · exact primePowerCompletedGroupAlgebraAugmentationAddHom_surjective (ℓ := ℓ) (G := G)
203/-- The canonical prime-power augmentation viewed as a `ℤ`-linear map. -/
205 PrimePowerCompletedGroupAlgebra ℓ G →ₗ[ℤ] PrimePowerCompletedCoeff ℓ G :=
206 (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)).toIntLinearMap
208/-- The canonical prime-power augmentation viewed as a
209`PrimePowerCompletedCoeff ℓ G`-linear map. -/
212 PrimePowerCompletedCoeff ℓ G where
213 toFun := primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)
214 map_add' := by
215 intro x y
216 exact map_add (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) x y
217 map_smul' := by
218 intro a x
219 apply (primePowerCompletedCoeffSystem ℓ G).ext
220 intro i
221 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
222 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (a • x)) =
223 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a *
224 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
225 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x)
226 rw [primePowerCompletedGroupAlgebraProjection_smul, Algebra.smul_def, map_mul,
229/-- Evaluation formula for primePowerCompletedGroupAlgebraAugmentationCoeffLinear_of. -/
230@[simp]
232 (ell : Nat)
233 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (h : H) :
234 primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H)
235 (primePowerCompletedGroupAlgebraOf (ell := ell) h) =
236 1 := by
237 apply (primePowerCompletedCoeffSystem ell H).ext
238 intro i
239 change modNCompletedGroupAlgebraStageAugmentation (ell ^ i.1) H i.2
240 (primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
241 (primePowerCompletedGroupAlgebraOf (ell := ell) h)) =
242 primePowerCompletedCoeffProjection (ℓ := ell) (G := H) i
243 (1 : PrimePowerCompletedCoeff ell H)
246 exact modNCompletedGroupAlgebraStageAugmentation_of (n := ell ^ i.1) (G := H) i.2
247 (QuotientGroup.mk h)
249/-- 素冪係数段階で、係数側の線形射影は単位元を単位元へ送る。 -/
250@[simp]
252 (ell : Nat)
253 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
254 primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H)
255 (1 : PrimePowerCompletedGroupAlgebra ell H) =
256 1 := by
257 change primePowerCompletedGroupAlgebraAugmentation (ℓ := ell) (G := H)
258 (1 : PrimePowerCompletedGroupAlgebra ell H) = 1
259 exact map_one (primePowerCompletedGroupAlgebraAugmentationRingHom (ℓ := ell) (G := H))
261/-- 素冪係数段階で、係数側の線形射影は積を積へ送る。 -/
262@[simp]
264 (ell : Nat)
265 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
266 (x y : PrimePowerCompletedGroupAlgebra ell H) :
267 primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H) (x * y) =
268 primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H) x *
269 primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H) y := by
270 change primePowerCompletedGroupAlgebraAugmentation (ℓ := ell) (G := H) (x * y) =
271 primePowerCompletedGroupAlgebraAugmentation (ℓ := ell) (G := H) x *
272 primePowerCompletedGroupAlgebraAugmentation (ℓ := ell) (G := H) y
273 exact map_mul (primePowerCompletedGroupAlgebraAugmentationRingHom (ℓ := ell) (G := H)) x y
275/-- The kernel inclusion of the prime-power augmentation, viewed as a `ℤ`-linear map. -/
277 primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G) →ₗ[ℤ]
280 (ℓ := ℓ) (G := G)).subtype.toIntLinearMap
282omit [Fact (0 < ℓ)] in
283/-- Surjectivity lemma primePowerCompletedGroupAlgebraAugmentationLinear_surjective. -/
285 Function.Surjective
286 (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) := by
287 simpa [primePowerCompletedGroupAlgebraAugmentationLinear, AddMonoidHom.coe_toIntLinearMap] using
288 primePowerCompletedGroupAlgebraAugmentationAddHom_surjective (ℓ := ℓ) (G := G)
290omit [Fact (0 < ℓ)] in
291/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が標準包含または係数写像が単射であることを述べる。 -/
293 Function.Injective
295 (ℓ := ℓ) (G := G)) := by
297 (ℓ := ℓ) (G := G)
299omit [Fact (0 < ℓ)] in
300/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
302 Function.Exact
304 (ℓ := ℓ) (G := G))
305 (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) := by
307 primePowerCompletedGroupAlgebraAugmentationLinear, AddMonoidHom.coe_toIntLinearMap] using
309 (ℓ := ℓ) (G := G)
311omit [Fact (0 < ℓ)] in
312/-- Injectivity, kernel identification, and surjectivity for the prime-power augmentation map in
313`ℤ`-linear form. -/
315 Function.Injective
317 (ℓ := ℓ) (G := G)) ∧
318 Function.Exact
320 (ℓ := ℓ) (G := G))
321 (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) ∧
322 Function.Surjective
323 (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) := by
325 (ℓ := ℓ) (G := G), ?_, ?_⟩
327 (ℓ := ℓ) (G := G)
328 · exact primePowerCompletedGroupAlgebraAugmentationLinear_surjective (ℓ := ℓ) (G := G)
331end
333end FoxDifferential