Yamaguchi Lean 4 Library
FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/AddCommGroup.lean
FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/AddCommGroup/Source

FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/AddCommGroup.lean

1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/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]
29 (C : ProCGroups.FiniteGroupClass.{u}) :
31 zero := ⟨fun i => (0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i), by
32 intro i j hij
33 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
35 exact map_zero _⟩
38 (C : ProCGroups.FiniteGroupClass.{u}) :
40 add x y := ⟨fun i =>
41 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
42 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i), by
43 intro i j hij
44 calc
46 ((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) +
47 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j))
48 =
50 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) +
52 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j) := by
53 rw [map_add]
54 _ =
55 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
56 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i) := by
57 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
60 (C : ProCGroups.FiniteGroupClass.{u}) :
61 AddZeroClass (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
62 zero := 0
63 add := (· + ·)
64 zero_add x := by
65 apply Subtype.ext
66 funext i
68 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) =
70 simp only [zero_add]
71 add_zero x := by
72 apply Subtype.ext
73 funext i
74 change (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
77 simp only [add_zero]
80 (C : ProCGroups.FiniteGroupClass.{u}) :
82 neg x := ⟨fun i => -(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
83 intro i j hij
84 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
85 (-(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
86 -(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
87 rw [map_neg]
88 exact congrArg Neg.neg (x.2 i j hij)⟩
91 (C : ProCGroups.FiniteGroupClass.{u}) :
93 sub x y := ⟨fun i =>
94 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) -
95 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i), by
96 intro i j hij
97 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
98 ((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) -
99 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j)) =
100 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) -
102 rw [map_sub]
103 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
106 (C : ProCGroups.FiniteGroupClass.{u}) :
108 smul m x := ⟨fun i =>
109 m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
110 intro i j hij
111 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
112 (m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
113 m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
114 rw [map_nsmul]
115 exact congrArg (m • ·) (x.2 i j hij)⟩
118 (C : ProCGroups.FiniteGroupClass.{u}) :
120 smul m x := ⟨fun i =>
121 m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
122 intro i j hij
123 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
124 (m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
125 m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
126 rw [map_zsmul]
127 exact congrArg (m • ·) (x.2 i j hij)⟩
129omit [Fact (0 < ℓ)] in
130/-- 素冪係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
131@[simp]
133 (C : ProCGroups.FiniteGroupClass.{u}) :
137 funext i
138 rfl
140omit [Fact (0 < ℓ)] in
141/-- 素冪係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
142@[simp]
144 (C : ProCGroups.FiniteGroupClass.{u})
149 funext i
150 rfl
152omit [Fact (0 < ℓ)] in
153/-- 素冪係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
154@[simp]
156 (C : ProCGroups.FiniteGroupClass.{u})
161 funext i
162 rfl
164omit [Fact (0 < ℓ)] in
165/-- 素冪係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
166@[simp]
168 (C : ProCGroups.FiniteGroupClass.{u})
173 funext i
174 rfl
176omit [Fact (0 < ℓ)] in
177/-- 素冪係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
178@[simp]
180 (C : ProCGroups.FiniteGroupClass.{u})
185 funext i
186 rfl
188omit [Fact (0 < ℓ)] in
189/-- 素冪係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
190@[simp]
192 (C : ProCGroups.FiniteGroupClass.{u})
197 funext i
198 rfl
201 (C : ProCGroups.FiniteGroupClass.{u}) :
203 Function.Injective.addCommGroup
205 (x :
208 Subtype.val_injective
213 (fun x m => coe_nsmul_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C m x)
214 (fun x m => coe_zsmul_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C m x)
216end
218end FoxDifferential