FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/AugmentationIdeal.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/AugmentationIdeal.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]
29section AugmentationIdeal
31variable (n : ℕ) [Fact (0 < n)]
32variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
34/-- The augmentation ideal on one residue-coefficient finite stage. -/
35def modNCompletedGroupAlgebraStageAugmentationIdeal (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
36 Ideal (ModNCompletedGroupAlgebraStage n G U) :=
37 RingHom.ker (modNCompletedGroupAlgebraStageAugmentation n G U)
39/-- The kernel of the canonical augmentation on the residue-coefficient completed group algebra. -/
41 Set (ModNCompletedGroupAlgebra n G) :=
42 {x | modNCompletedGroupAlgebraAugmentation n G x = 0}
44/-- The kernel of the canonical augmentation, viewed as a subtype. -/
46 {x : ModNCompletedGroupAlgebra n G // x ∈ modNCompletedGroupAlgebraAugmentationKernel n G}
48omit [Fact (0 < n)] in
49variable {n G} in
50/-- 法 n 係数で定めた augmentation または augmentation ideal への標準写像が所属条件を対応する augmentation または射影の消滅条件として特徴づけることを述べる。 -/
51@[simp]
53 {U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} {x : ModNCompletedGroupAlgebraStage n G U} :
54 x ∈ modNCompletedGroupAlgebraStageAugmentationIdeal n G U ↔
55 modNCompletedGroupAlgebraStageAugmentation n G U x = 0 := by
56 rw [modNCompletedGroupAlgebraStageAugmentationIdeal, RingHom.mem_ker]
58omit [Fact (0 < n)] in
59variable {n G} in
60/-- 法 n 係数で定めた augmentation または augmentation ideal への標準写像が所属条件を対応する augmentation または射影の消滅条件として特徴づけることを述べる。 -/
61@[simp]
63 {x : ModNCompletedGroupAlgebra n G} :
65 modNCompletedGroupAlgebraAugmentation n G x = 0 := by
66 rfl
68omit [Fact (0 < n)] in
69variable {n G} in
70/-- 法 n 係数で定めた 有限段階射影が所属条件を対応する augmentation または射影の消滅条件として特徴づけることを述べる。 -/
71@[simp]
73 {U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} {x : ModNCompletedGroupAlgebra n G} :
74 modNCompletedGroupAlgebraProjection n G U x ∈
76 x ∈ modNCompletedGroupAlgebraAugmentationKernel n G := by
79 change modNCompletedGroupAlgebraAugmentationAt n G U x = 0 ↔
80 modNCompletedGroupAlgebraAugmentation n G x = 0
81 rw [modNCompletedGroupAlgebraAugmentation_eq_at (n := n) (G := G) U x]
83/-- The transition maps on the residue-coefficient finite-stage augmentation ideals. -/
85 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
88 fun x => ⟨modNCompletedGroupAlgebraTransition n G hUV x.1, by
90 have hcomp := congrFun
91 (congrArg DFunLike.coe
93 (n := n) (G := G) (U := U) (V := V) hUV))
94 x.1
95 rw [RingHom.comp_apply] at hcomp
96 exact hcomp.trans
98 (n := n) (G := G) (U := V) (x := x.1)).1 x.2)⟩
100omit [Fact (0 < n)] in
101/-- 法 n 係数で定めた 遷移写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
102@[simp]
104 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
105 (x : modNCompletedGroupAlgebraStageAugmentationIdeal n G V) :
107 (n := n) (G := G) hUV x : modNCompletedGroupAlgebraStageAugmentationIdeal n G U) :
108 ModNCompletedGroupAlgebraStage n G U) =
109 modNCompletedGroupAlgebraTransition n G hUV x.1 := rfl
111/-- The inverse system of residue-coefficient finite-stage augmentation ideals. -/
113 InverseSystem (I := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) where
114 X := fun U => ↥(modNCompletedGroupAlgebraStageAugmentationIdeal n G U)
115 topologicalSpace := fun _ => ⊥
116 map := fun {U V} hUV => modNCompletedGroupAlgebraStageAugmentationIdealTransition
117 (n := n) (G := G) hUV
118 continuous_map := by
119 intro U V hUV
120 letI : TopologicalSpace (modNCompletedGroupAlgebraStageAugmentationIdeal n G U) := ⊥
121 letI : TopologicalSpace (modNCompletedGroupAlgebraStageAugmentationIdeal n G V) := ⊥
122 letI : DiscreteTopology (modNCompletedGroupAlgebraStageAugmentationIdeal n G V) := ⟨rfl⟩
123 exact continuous_of_discreteTopology
124 map_id := by
125 intro U
126 funext x
127 apply Subtype.ext
128 exact congrFun
129 (congrArg DFunLike.coe (modNCompletedGroupAlgebraTransition_id (n := n) (G := G) U))
130 x.1
131 map_comp := by
132 intro U V W hUV hVW
133 funext x
134 apply Subtype.ext
135 exact congrFun
136 (congrArg DFunLike.coe
137 (modNCompletedGroupAlgebraTransition_comp (n := n) (G := G) hUV hVW))
138 x.1
140/-- The inverse-limit object of the residue-coefficient finite-stage augmentation ideals. -/
142 (modNCompletedGroupAlgebraAugmentationIdealSystem n G).inverseLimit
144/-- The projection from the residue-coefficient augmentation-ideal inverse limit to one stage. -/
145abbrev modNCompletedGroupAlgebraAugmentationIdealProjection (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
148 (modNCompletedGroupAlgebraAugmentationIdealSystem n G).projection U
150/-- A residue-coefficient augmentation-kernel point determines a compatible family in the
151finite-stage augmentation ideals. -/
155 intro x
156 refine ⟨fun U => ⟨modNCompletedGroupAlgebraProjection n G U x.1, ?_⟩, ?_⟩
158 (n := n) (G := G) (U := U) (x := x.1)).2
160 (n := n) (G := G) (x := x.1)).1 x.2)
161 · intro U V hUV
162 apply Subtype.ext
163 exact (modNCompletedGroupAlgebraSystem n G).projection_compatible x.1 U V hUV
165omit [Fact (0 < n)] in
166/-- 法 n 係数で定めた 有限段階射影がaugmentation ideal の元を基礎にある完備群環へ戻す写像の値を記述することを述べる。 -/
167@[simp]
169 (x : ModNCompletedGroupAlgebraAugmentationKernel n G) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
170 ((modNCompletedGroupAlgebraAugmentationIdealProjection (n := n) (G := G) U
171 (toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x)) :
172 ModNCompletedGroupAlgebraStage n G U) =
173 modNCompletedGroupAlgebraProjection n G U x.1 := rfl
175/-- A compatible family of finite-stage augmentation-ideal elements determines a residue-coefficient
176completed augmentation-kernel point. -/
180 intro x
181 let y : ModNCompletedGroupAlgebra n G := ⟨fun U => (x.1 U).1, by
182 intro U V hUV
183 exact congrArg Subtype.val (x.2 U V hUV)⟩
184 refine ⟨y, ?_⟩
185 have hterm :
186 modNCompletedGroupAlgebraProjection n G (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) y ∈
188 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) := by
189 change (x.1 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)).1 ∈
191 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)
192 exact (x.1 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)).2
193 exact (mem_modNCompletedGroupAlgebraAugmentationKernel_iff (n := n) (G := G) (x := y)).2
195 (n := n) (G := G) (U := _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) (x := y)).1 hterm)
197omit [Fact (0 < n)] in
198/-- 法 n 係数で定めた 有限段階射影が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
199@[simp]
201 (x : ModNCompletedGroupAlgebraAugmentationIdeal n G) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
203 (ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x).1 =
204 ((modNCompletedGroupAlgebraAugmentationIdealProjection (n := n) (G := G) U x) :
205 ModNCompletedGroupAlgebraStage n G U) := rfl
207omit [Fact (0 < n)] in
208/-- 法 n 係数で定めた augmentation または augmentation ideal への標準写像がaugmentation ideal の元を基礎にある完備群環へ戻す写像の値を記述することを述べる。 -/
209@[simp]
211 (x : ModNCompletedGroupAlgebraAugmentationKernel n G) :
212 ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
213 (toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x) = x := by
214 apply Subtype.ext
215 apply (modNCompletedGroupAlgebraSystem n G).ext
216 intro U
217 rfl
219omit [Fact (0 < n)] in
220/-- Evaluation formula for toModNCompletedGroupAlgebraAugmentationIdeal_of. -/
221@[simp]
223 (x : ModNCompletedGroupAlgebraAugmentationIdeal n G) :
224 toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
225 (ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x) = x := by
226 apply (modNCompletedGroupAlgebraAugmentationIdealSystem n G).ext
227 intro U
228 apply Subtype.ext
229 rfl
231/-- The residue-coefficient completed augmentation kernel is canonically equivalent to the inverse
232limit of the finite-stage augmentation ideals. -/
236 toFun := toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
237 invFun := ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
238 left_inv := ofModNCompletedGroupAlgebraAugmentationIdeal_to (n := n) (G := G)
239 right_inv := toModNCompletedGroupAlgebraAugmentationIdeal_of (n := n) (G := G)
241omit [Fact (0 < n)] in
242/-- Evaluation formula for modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply. -/
243@[simp]
245 (x : ModNCompletedGroupAlgebraAugmentationKernel n G) :
246 modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit (n := n) (G := G) x =
247 toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x := rfl
249omit [Fact (0 < n)] in
250/-- Evaluation formula for modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply. -/
251@[simp]
253 (x : ModNCompletedGroupAlgebraAugmentationIdeal n G) :
254 (modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit (n := n) (G := G)).symm x =
255 ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x := rfl
257end AugmentationIdeal
259end
261end FoxDifferential