FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System/Ring/Multiplicative.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.AddCommGroup
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/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]
28instance instOnePrimePowerCompletedGroupAlgebra : One (PrimePowerCompletedGroupAlgebra ℓ G) where
29 one := ⟨fun i => (1 : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
30 intro i j hij
31 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
32 (1 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 1
35instance instMulPrimePowerCompletedGroupAlgebra : Mul (PrimePowerCompletedGroupAlgebra ℓ G) where
36 mul x y := ⟨fun i =>
37 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) *
38 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i), by
39 intro i j hij
40 calc
41 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
42 ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) *
43 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j))
44 =
45 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
46 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) *
47 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
48 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j) := by
50 _ =
51 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) *
52 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i) := by
53 exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩
55instance instNatCastPrimePowerCompletedGroupAlgebra :
56 NatCast (PrimePowerCompletedGroupAlgebra ℓ G) where
57 natCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
58 intro i j hij
59 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
60 (n : PrimePowerCompletedGroupAlgebraStage ℓ G j) = n
61 exact map_natCast _ _⟩
63instance instIntCastPrimePowerCompletedGroupAlgebra :
64 IntCast (PrimePowerCompletedGroupAlgebra ℓ G) where
65 intCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
66 intro i j hij
67 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
68 (n : PrimePowerCompletedGroupAlgebraStage ℓ G j) = n
69 exact map_intCast _ _⟩
72 (i : PrimePowerCompletedGroupAlgebraIndex G) :
73 Ring ((primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
75 infer_instance
78 Ring
79 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
80 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) :=
81 inferInstance
83instance instPowPrimePowerCompletedGroupAlgebra : Pow (PrimePowerCompletedGroupAlgebra ℓ G) ℕ where
84 pow x n := ⟨fun i => (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) ^ n, by
85 intro i j hij
86 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
87 ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) ^ n) =
88 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) ^ n
89 rw [map_pow]
90 exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩
92omit [Fact (0 < ℓ)] in
93/-- 素冪係数で定めた 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
94@[simp]
96 ((1 : PrimePowerCompletedGroupAlgebra ℓ G) :
97 (i : PrimePowerCompletedGroupAlgebraIndex G) →
98 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
99 (1 :
100 (i : PrimePowerCompletedGroupAlgebraIndex G) →
101 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
102 funext i
103 rfl
105omit [Fact (0 < ℓ)] in
106/-- 素冪係数で定めた 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
107@[simp]
109 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
110 ((x * y : PrimePowerCompletedGroupAlgebra ℓ G) :
111 (i : PrimePowerCompletedGroupAlgebraIndex G) →
112 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
113 (x * y :
114 (i : PrimePowerCompletedGroupAlgebraIndex G) →
115 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
116 funext i
117 rfl
119omit [Fact (0 < ℓ)] in
120/-- 素冪係数で定めた 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
121@[simp]
123 (n : ℕ) :
124 ((n : PrimePowerCompletedGroupAlgebra ℓ G) :
125 (i : PrimePowerCompletedGroupAlgebraIndex G) →
126 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
127 (n :
128 (i : PrimePowerCompletedGroupAlgebraIndex G) →
129 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
130 funext i
131 rfl
133omit [Fact (0 < ℓ)] in
134/-- 素冪係数で定めた 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
135@[simp]
137 (n : ℤ) :
138 ((n : PrimePowerCompletedGroupAlgebra ℓ G) :
139 (i : PrimePowerCompletedGroupAlgebraIndex G) →
140 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
141 (n :
142 (i : PrimePowerCompletedGroupAlgebraIndex G) →
143 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
144 funext i
145 rfl
147omit [Fact (0 < ℓ)] in
148/-- 素冪係数で定めた 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
149@[simp]
151 (x : PrimePowerCompletedGroupAlgebra ℓ G) (n : ℕ) :
152 ((x ^ n : PrimePowerCompletedGroupAlgebra ℓ G) :
153 (i : PrimePowerCompletedGroupAlgebraIndex G) →
154 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
155 (x ^ n :
156 (i : PrimePowerCompletedGroupAlgebraIndex G) →
157 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
158 funext i
159 rfl
161instance instRingPrimePowerCompletedGroupAlgebra :
162 Ring (PrimePowerCompletedGroupAlgebra ℓ G) :=
163 Function.Injective.ring
164 (fun x : PrimePowerCompletedGroupAlgebra ℓ G =>
165 (x :
166 (i : PrimePowerCompletedGroupAlgebraIndex G) →
167 (primePowerCompletedGroupAlgebraSystem ℓ G).X i))
168 Subtype.val_injective
169 (coe_zero_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
170 (coe_one_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
171 (coe_add_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
172 (coe_mul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
173 (coe_neg_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
174 (coe_sub_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
175 (fun n x => coe_nsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) n x)
176 (fun n x => coe_zsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) n x)
177 (fun x n => coe_pow_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) x n)
178 (by
179 intro n
180 exact coe_natCast_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) n)
181 (by
182 intro z
183 exact coe_intCast_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) z)
185end
187end FoxDifferential