FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/Multiplicative.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.AddCommGroup
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/Multiplicative.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}) :
30 One (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
31 one := ⟨fun i => (1 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i), by
32 intro i j hij
33 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
34 (1 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) = 1
38 (C : ProCGroups.FiniteGroupClass.{u}) :
39 Mul (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
40 mul 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
45 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
46 ((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) *
47 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j))
48 =
49 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
50 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) *
51 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
52 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j) := by
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₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩
60 (C : ProCGroups.FiniteGroupClass.{u}) :
61 NatCast (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
62 natCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i), by
63 intro i j hij
64 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
65 (n : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) = n
66 exact map_natCast _ _⟩
69 (C : ProCGroups.FiniteGroupClass.{u}) :
70 IntCast (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
71 intCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i), by
72 intro i j hij
73 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
74 (n : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) = n
75 exact map_intCast _ _⟩
78 (C : ProCGroups.FiniteGroupClass.{u}) :
79 Pow (PrimePowerCompletedGroupAlgebraInClass ℓ G C) ℕ where
80 pow x n := ⟨fun i =>
81 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) ^ n, by
82 intro i j hij
83 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
84 ((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) ^ n) =
85 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) ^ n
86 rw [map_pow]
87 exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩
89omit [Fact (0 < ℓ)] in
90/-- 素冪係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
91@[simp]
93 (C : ProCGroups.FiniteGroupClass.{u}) :
94 ((1 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
95 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
96 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
97 (1 :
98 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
99 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) := by
100 funext i
101 rfl
103omit [Fact (0 < ℓ)] in
104/-- 素冪係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
105@[simp]
107 (C : ProCGroups.FiniteGroupClass.{u})
108 (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
109 ((x * y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
110 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
111 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
112 (x * y :
113 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
114 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) := by
115 funext i
116 rfl
118omit [Fact (0 < ℓ)] in
119/-- 素冪係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
120@[simp]
122 (C : ProCGroups.FiniteGroupClass.{u}) (n : ℕ) :
123 ((n : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
124 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
125 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
126 (n :
127 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
128 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) := by
129 funext i
130 rfl
132omit [Fact (0 < ℓ)] in
133/-- 素冪係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
134@[simp]
136 (C : ProCGroups.FiniteGroupClass.{u}) (n : ℤ) :
137 ((n : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
138 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
139 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
140 (n :
141 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
142 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) := by
143 funext i
144 rfl
146omit [Fact (0 < ℓ)] in
147/-- 素冪係数で定めた 有限群クラスを固定した 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
148@[simp]
150 (C : ProCGroups.FiniteGroupClass.{u})
151 (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) (n : ℕ) :
152 ((x ^ n : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
153 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
154 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
155 (x ^ n :
156 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
157 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) := by
158 funext i
159 rfl
162 (C : ProCGroups.FiniteGroupClass.{u}) :
163 Ring (PrimePowerCompletedGroupAlgebraInClass ℓ G C) :=
164 Function.Injective.ring
165 (fun x : PrimePowerCompletedGroupAlgebraInClass ℓ G C =>
166 (x :
167 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
169 Subtype.val_injective
170 (coe_zero_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
171 (coe_one_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
172 (coe_add_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
173 (coe_mul_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
174 (coe_neg_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
175 (coe_sub_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
176 (fun n x => coe_nsmul_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C n x)
177 (fun n x => coe_zsmul_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C n x)
178 (fun x n => coe_pow_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C x n)
179 (by
180 intro n
181 exact coe_natCast_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C n)
182 (by
183 intro z
184 exact coe_intCast_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C z)
186end
188end FoxDifferential