FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Coeff/AddCommGroup.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.System
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Coeff/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 (ℓ : ℕ) [Fact (0 < ℓ)]
26variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28instance instZeroPrimePowerCompletedCoeff : Zero (PrimePowerCompletedCoeff ℓ G) where
30 intro i j hij
31 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
32 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
35 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
36 (primePow_dvd_primePow (ℓ := ℓ) hij.1))⟩
38instance instAddPrimePowerCompletedCoeff : Add (PrimePowerCompletedCoeff ℓ G) where
40 (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i), by
41 intro i j hij
42 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
43 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
44 change modNCompletedCoeffMap
45 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
46 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
47 ((show ZMod (ℓ ^ j.1) from x.1 j) + (show ZMod (ℓ ^ j.1) from y.1 j)) =
48 (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i)
50 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
52instance instAddZeroClassPrimePowerCompletedCoeff :
53 AddZeroClass (PrimePowerCompletedCoeff ℓ G) where
56 zero_add x := by
57 apply Subtype.ext
58 funext i
59 change (0 : ZMod (ℓ ^ i.1)) + (show ZMod (ℓ ^ i.1) from x.1 i) =
60 (show ZMod (ℓ ^ i.1) from x.1 i)
61 simp only [zero_add]
62 add_zero x := by
63 apply Subtype.ext
64 funext i
65 change (show ZMod (ℓ ^ i.1) from x.1 i) + (0 : ZMod (ℓ ^ i.1)) =
66 (show ZMod (ℓ ^ i.1) from x.1 i)
67 simp only [add_zero]
69instance instNegPrimePowerCompletedCoeff : Neg (PrimePowerCompletedCoeff ℓ G) where
71 intro i j hij
72 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
73 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
74 change modNCompletedCoeffMap
75 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
76 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
77 (-(show ZMod (ℓ ^ j.1) from x.1 j)) =
78 -(show ZMod (ℓ ^ i.1) from x.1 i)
79 rw [map_neg]
80 exact congrArg Neg.neg (x.2 i j hij)⟩
82instance instSubPrimePowerCompletedCoeff : Sub (PrimePowerCompletedCoeff ℓ G) where
84 (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i), by
85 intro i j hij
86 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
87 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
88 change modNCompletedCoeffMap
89 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
90 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
91 ((show ZMod (ℓ ^ j.1) from x.1 j) - (show ZMod (ℓ ^ j.1) from y.1 j)) =
92 (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i)
93 rw [map_sub]
94 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
96instance instSMulNatPrimePowerCompletedCoeff : SMul ℕ (PrimePowerCompletedCoeff ℓ G) where
97 smul m x := ⟨fun i => m • (show ZMod (ℓ ^ i.1) from x.1 i), by
98 intro i j hij
99 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
100 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
101 change modNCompletedCoeffMap
102 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
103 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
104 (m • (show ZMod (ℓ ^ j.1) from x.1 j)) =
105 m • (show ZMod (ℓ ^ i.1) from x.1 i)
106 rw [map_nsmul]
107 exact congrArg (m • ·) (x.2 i j hij)⟩
109instance instSMulIntPrimePowerCompletedCoeff : SMul ℤ (PrimePowerCompletedCoeff ℓ G) where
110 smul m x := ⟨fun i => m • (show ZMod (ℓ ^ i.1) from x.1 i), by
111 intro i j hij
112 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
113 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
114 change modNCompletedCoeffMap
115 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
116 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
117 (m • (show ZMod (ℓ ^ j.1) from x.1 j)) =
118 m • (show ZMod (ℓ ^ i.1) from x.1 i)
119 rw [map_zsmul]
120 exact congrArg (m • ·) (x.2 i j hij)⟩
123 (i : PrimePowerCompletedGroupAlgebraIndex G) :
124 AddCommGroup ((primePowerCompletedCoeffSystem ℓ G).X i) := by
125 dsimp [primePowerCompletedCoeffSystem]
126 infer_instance
129 AddCommGroup
130 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
131 (primePowerCompletedCoeffSystem ℓ G).X i) :=
132 inferInstance
134omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
135/-- 素冪係数で定めた 係数側の射影または係数変更写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
136@[simp]
137theorem coe_zero_primePowerCompletedCoeff :
138 ((0 : PrimePowerCompletedCoeff ℓ G) :
139 (i : PrimePowerCompletedGroupAlgebraIndex G) →
140 (primePowerCompletedCoeffSystem ℓ G).X i) = 0 := by
141 funext i
142 rfl
144omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
145/-- 素冪係数で定めた 係数側の射影または係数変更写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
146@[simp]
148 (x y : PrimePowerCompletedCoeff ℓ G) :
149 ((x + y : PrimePowerCompletedCoeff ℓ G) :
150 (i : PrimePowerCompletedGroupAlgebraIndex G) →
151 (primePowerCompletedCoeffSystem ℓ G).X i) = x + y := by
152 funext i
153 rfl
155omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
156/-- 素冪係数で定めた 係数側の射影または係数変更写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
157@[simp]
159 (x : PrimePowerCompletedCoeff ℓ G) :
160 ((-x : PrimePowerCompletedCoeff ℓ G) :
161 (i : PrimePowerCompletedGroupAlgebraIndex G) →
162 (primePowerCompletedCoeffSystem ℓ G).X i) = -x := by
163 funext i
164 rfl
166omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
167/-- 素冪係数で定めた 係数側の射影または係数変更写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
168@[simp]
170 (x y : PrimePowerCompletedCoeff ℓ G) :
171 ((x - y : PrimePowerCompletedCoeff ℓ G) :
172 (i : PrimePowerCompletedGroupAlgebraIndex G) →
173 (primePowerCompletedCoeffSystem ℓ G).X i) = x - y := by
174 funext i
175 rfl
177omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
178/-- 素冪係数で定めた 係数側の射影または係数変更写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
179@[simp]
181 (m : ℕ) (x : PrimePowerCompletedCoeff ℓ G) :
182 ((m • x : PrimePowerCompletedCoeff ℓ G) :
183 (i : PrimePowerCompletedGroupAlgebraIndex G) →
184 (primePowerCompletedCoeffSystem ℓ G).X i) = m • x := by
185 funext i
186 rfl
188omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
189/-- 素冪係数で定めた 係数側の射影または係数変更写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
190@[simp]
192 (m : ℤ) (x : PrimePowerCompletedCoeff ℓ G) :
193 ((m • x : PrimePowerCompletedCoeff ℓ G) :
194 (i : PrimePowerCompletedGroupAlgebraIndex G) →
195 (primePowerCompletedCoeffSystem ℓ G).X i) = m • x := by
196 funext i
197 rfl
199instance instAddCommGroupPrimePowerCompletedCoeff :
200 AddCommGroup (PrimePowerCompletedCoeff ℓ G) :=
201 Function.Injective.addCommGroup
202 (fun x : PrimePowerCompletedCoeff ℓ G =>
203 (x :
204 (i : PrimePowerCompletedGroupAlgebraIndex G) →
205 (primePowerCompletedCoeffSystem ℓ G).X i))
206 Subtype.val_injective
207 (coe_zero_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
208 (coe_add_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
209 (coe_neg_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
210 (coe_sub_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
211 (fun x m => coe_nsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) m x)
212 (fun x m => coe_zsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) m x)
214end
216end FoxDifferential