FoxDifferential/Completed/CoefficientRings/AugmentationIdealPrimePower/Additive.lean
1import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Stage
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/AugmentationIdealPrimePower/Additive.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]
29 Zero (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
31 (0 : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i), by
32 intro i j hij
33 apply Subtype.ext
34 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
35 (0 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 0
39 Add (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
41 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
42 from x.1 i) +
43 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
44 from y.1 i), by
45 intro i j hij
46 apply Subtype.ext
47 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
48 (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
49 from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j) +
50 ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
51 from y.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j)) =
52 (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
53 from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i) +
54 ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
55 from y.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
57 exact congrArg₂ HAdd.hAdd
58 (congrArg Subtype.val (x.2 i j hij))
59 (congrArg Subtype.val (y.2 i j hij))⟩
62 AddZeroClass (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
65 zero_add x := by
66 apply Subtype.ext
67 funext i
68 apply Subtype.ext
69 change (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) +
70 ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
71 PrimePowerCompletedGroupAlgebraStage ℓ G i) =
72 ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
74 simp only [zero_add]
75 add_zero x := by
76 apply Subtype.ext
77 funext i
78 apply Subtype.ext
79 change ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal
80 (ℓ := ℓ) (G := G) i from x.1 i) :
81 PrimePowerCompletedGroupAlgebraStage ℓ G i) +
82 (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) =
83 ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
85 simp only [add_zero]
88 Neg (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
90 -(show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
91 from x.1 i), by
92 intro i j hij
93 apply Subtype.ext
94 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
95 (-(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
96 from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
97 -(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
98 from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
99 rw [map_neg]
100 exact congrArg Neg.neg (congrArg Subtype.val (x.2 i j hij))⟩
103 Sub (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
105 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
106 from x.1 i) -
107 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
108 from y.1 i), by
109 intro i j hij
110 apply Subtype.ext
111 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
112 ((((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
113 from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j)) -
114 (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
115 from y.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
116 ((((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
117 from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i)) -
118 (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
119 from y.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i)))
120 rw [map_sub]
121 exact congrArg₂ HSub.hSub
122 (congrArg Subtype.val (x.2 i j hij))
123 (congrArg Subtype.val (y.2 i j hij))⟩
126 SMul ℕ (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
127 smul m x := ⟨fun i =>
128 m • (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
129 from x.1 i), by
130 intro i j hij
131 apply Subtype.ext
132 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
133 (m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
134 from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
135 m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
136 from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
137 rw [map_nsmul]
138 exact congrArg (m • ·) (congrArg Subtype.val (x.2 i j hij))⟩
141 SMul ℤ (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
142 smul m x := ⟨fun i =>
143 m • (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
144 from x.1 i), by
145 intro i j hij
146 apply Subtype.ext
147 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
148 (m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
149 from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
150 m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
151 from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
152 rw [map_zsmul]
153 exact congrArg (m • ·) (congrArg Subtype.val (x.2 i j hij))⟩
156 (i : PrimePowerCompletedGroupAlgebraIndex G) :
157 AddCommGroup ((primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) := by
159 infer_instance
162 AddCommGroup
163 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
164 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) :=
165 inferInstance
167omit [Fact (0 < ℓ)] in
168/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
169@[simp]
171 ((0 : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
172 (i : PrimePowerCompletedGroupAlgebraIndex G) →
173 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = 0 := by
174 funext i
175 rfl
177omit [Fact (0 < ℓ)] in
178/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
179@[simp]
181 (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
182 ((x + y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
183 (i : PrimePowerCompletedGroupAlgebraIndex G) →
184 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = x + y := by
185 funext i
186 rfl
188omit [Fact (0 < ℓ)] in
189/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
190@[simp]
192 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
193 ((-x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
194 (i : PrimePowerCompletedGroupAlgebraIndex G) →
195 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = -x := by
196 funext i
197 rfl
199omit [Fact (0 < ℓ)] in
200/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
201@[simp]
203 (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
204 ((x - y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
205 (i : PrimePowerCompletedGroupAlgebraIndex G) →
206 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = x - y := by
207 funext i
208 rfl
210omit [Fact (0 < ℓ)] in
211/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
212@[simp]
214 (m : ℕ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
215 ((m • x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
216 (i : PrimePowerCompletedGroupAlgebraIndex G) →
217 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = m • x := by
218 funext i
219 rfl
221omit [Fact (0 < ℓ)] in
222/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
223@[simp]
225 (m : ℤ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
226 ((m • x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
227 (i : PrimePowerCompletedGroupAlgebraIndex G) →
228 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = m • x := by
229 funext i
230 rfl
233 AddCommGroup (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :=
234 Function.Injective.addCommGroup
235 (fun x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G =>
236 (x :
237 (i : PrimePowerCompletedGroupAlgebraIndex G) →
239 Subtype.val_injective
240 (coe_zero_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
241 (coe_add_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
242 (coe_neg_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
243 (coe_sub_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
244 (fun x m => coe_nsmul_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) m x)
245 (fun x m => coe_zsmul_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) m x)
248end
250end FoxDifferential