Yamaguchi Lean 4 Library
FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/InClass/AddCommGroup.lean
FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/InClass/AddCommGroup/Source

FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/InClass/AddCommGroup.lean

1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/InClass/AddCommGroup.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 (n : ℕ) [Fact (0 < n)]
26variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29 (C : ProCGroups.FiniteGroupClass.{u}) :
31 zero := ⟨fun U => (0 : ModNCompletedGroupAlgebraStageInClass n G C U), by
32 intro U V hUV
35 exact map_zero _⟩
38 (C : ProCGroups.FiniteGroupClass.{u}) :
40 add x y := ⟨fun U =>
41 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
42 (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U), by
43 intro U V hUV
44 calc
46 ((show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) +
47 (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V))
48 =
50 (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) +
52 (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V) := by
53 rw [map_add]
54 _ =
55 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
56 (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U) := by
57 exact congrArg₂ HAdd.hAdd (x.2 U V hUV) (y.2 U V hUV)⟩
60 (C : ProCGroups.FiniteGroupClass.{u}) :
61 AddZeroClass (ModNCompletedGroupAlgebraInClass n G C) where
62 zero := 0
63 add := (· + ·)
64 zero_add x := by
65 apply Subtype.ext
66 funext U
68 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) =
69 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
70 simp only [zero_add]
71 add_zero x := by
72 apply Subtype.ext
73 funext U
74 change (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
76 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
77 simp only [add_zero]
80 (C : ProCGroups.FiniteGroupClass.{u}) :
82 neg x := ⟨fun U => -(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
83 intro U V hUV
85 (-(show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
86 -(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
87 rw [map_neg]
88 exact congrArg Neg.neg (x.2 U V hUV)⟩
91 (C : ProCGroups.FiniteGroupClass.{u}) :
93 sub x y := ⟨fun U =>
94 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) -
95 (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U), by
96 intro U V hUV
98 ((show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) -
99 (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V)) =
100 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) -
101 (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U)
102 rw [map_sub]
103 exact congrArg₂ HSub.hSub (x.2 U V hUV) (y.2 U V hUV)⟩
106 (C : ProCGroups.FiniteGroupClass.{u}) :
107 SMul ℕ (ModNCompletedGroupAlgebraInClass n G C) where
108 smul m x := ⟨fun U =>
109 m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
110 intro U V hUV
112 (m • (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
113 m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
114 rw [map_nsmul]
115 exact congrArg (m • ·) (x.2 U V hUV)⟩
118 (C : ProCGroups.FiniteGroupClass.{u}) :
119 SMul ℤ (ModNCompletedGroupAlgebraInClass n G C) where
120 smul m x := ⟨fun U =>
121 m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
122 intro U V hUV
124 (m • (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
125 m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
126 rw [map_zsmul]
127 exact congrArg (m • ·) (x.2 U V hUV)⟩
129omit [Fact (0 < n)] in
130/-- 法 n 係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
131@[simp]
133 (C : ProCGroups.FiniteGroupClass.{u}) :
135 (U : CompletedGroupAlgebraIndexInClass G C) →
137 funext U
138 rfl
140omit [Fact (0 < n)] in
141/-- 法 n 係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
142@[simp]
144 (C : ProCGroups.FiniteGroupClass.{u})
147 (U : CompletedGroupAlgebraIndexInClass G C) →
149 funext U
150 rfl
152omit [Fact (0 < n)] in
153/-- 法 n 係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
154@[simp]
156 (C : ProCGroups.FiniteGroupClass.{u})
159 (U : CompletedGroupAlgebraIndexInClass G C) →
161 funext U
162 rfl
164omit [Fact (0 < n)] in
165/-- 法 n 係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
166@[simp]
168 (C : ProCGroups.FiniteGroupClass.{u})
171 (U : CompletedGroupAlgebraIndexInClass G C) →
173 funext U
174 rfl
176omit [Fact (0 < n)] in
177/-- 法 n 係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
178@[simp]
180 (C : ProCGroups.FiniteGroupClass.{u})
181 (m : ℕ) (x : ModNCompletedGroupAlgebraInClass n G C) :
183 (U : CompletedGroupAlgebraIndexInClass G C) →
185 funext U
186 rfl
188omit [Fact (0 < n)] in
189/-- 法 n 係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
190@[simp]
192 (C : ProCGroups.FiniteGroupClass.{u})
193 (m : ℤ) (x : ModNCompletedGroupAlgebraInClass n G C) :
195 (U : CompletedGroupAlgebraIndexInClass G C) →
197 funext U
198 rfl
201 (C : ProCGroups.FiniteGroupClass.{u}) :
202 AddCommGroup (ModNCompletedGroupAlgebraInClass n G C) :=
203 Function.Injective.addCommGroup
205 (x :
206 (U : CompletedGroupAlgebraIndexInClass G C) →
208 Subtype.val_injective
213 (fun x m => coe_nsmul_modNCompletedGroupAlgebraInClass (n := n) (G := G) C m x)
214 (fun x m => coe_zsmul_modNCompletedGroupAlgebraInClass (n := n) (G := G) C m x)
216omit [Fact (0 < n)] in
217/-- 法 n の係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は零元を零元へ送る。 -/
218@[simp]
220 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
223 rfl
225omit [Fact (0 < n)] in
226/-- 法 n の係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は和を和へ送る。 -/
227@[simp]
229 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
234 rfl
236omit [Fact (0 < n)] in
237/-- 法 n の係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は負元を負元へ送る。 -/
238@[simp]
240 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
244 rfl
246omit [Fact (0 < n)] in
247/-- 法 n の係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は差を差へ送る。 -/
248@[simp]
250 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
255 rfl
257omit [Fact (0 < n)] in
258/-- 法 n の係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は自然数倍と両立する。 -/
259@[simp]
261 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
262 (m : ℕ) (x : ModNCompletedGroupAlgebraInClass n G C) :
265 rfl
267omit [Fact (0 < n)] in
268/-- 法 n の係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は整数倍と両立する。 -/
269@[simp]
271 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
272 (m : ℤ) (x : ModNCompletedGroupAlgebraInClass n G C) :
275 rfl
277end
279end FoxDifferential