FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Coeff/Ring.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Coeff/Ring.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 instOnePrimePowerCompletedCoeff : One (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 instMulPrimePowerCompletedCoeff : Mul (PrimePowerCompletedCoeff ℓ G) where
39 mul x y := ⟨fun i =>
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₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩
52instance instNatCastPrimePowerCompletedCoeff : NatCast (PrimePowerCompletedCoeff ℓ G) where
53 natCast n := ⟨fun i => (n : ZMod (ℓ ^ i.1)), by
54 intro i j hij
55 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
56 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
57 exact map_natCast
59 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
60 (primePow_dvd_primePow (ℓ := ℓ) hij.1)) n⟩
62instance instIntCastPrimePowerCompletedCoeff : IntCast (PrimePowerCompletedCoeff ℓ G) where
63 intCast n := ⟨fun i => (n : ZMod (ℓ ^ i.1)), by
64 intro i j hij
65 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
66 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
67 exact map_intCast
69 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
70 (primePow_dvd_primePow (ℓ := ℓ) hij.1)) n⟩
73 (i : PrimePowerCompletedGroupAlgebraIndex G) :
74 CommRing ((primePowerCompletedCoeffSystem ℓ G).X i) := by
75 dsimp [primePowerCompletedCoeffSystem]
76 infer_instance
78instance instCommRingPrimePowerCompletedCoeffFamily :
79 CommRing
80 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
81 (primePowerCompletedCoeffSystem ℓ G).X i) :=
82 inferInstance
84instance instPowPrimePowerCompletedCoeff : Pow (PrimePowerCompletedCoeff ℓ G) ℕ where
85 pow x n := ⟨fun i => (show ZMod (ℓ ^ i.1) from x.1 i) ^ n, by
86 intro i j hij
87 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
88 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
89 change modNCompletedCoeffMap
90 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
91 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
92 ((show ZMod (ℓ ^ j.1) from x.1 j) ^ n) =
93 (show ZMod (ℓ ^ i.1) from x.1 i) ^ n
94 rw [map_pow]
95 exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩
97omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
98/-- 素冪係数で定めた 係数側の射影または係数変更写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
99@[simp]
100theorem coe_one_primePowerCompletedCoeff :
101 ((1 : PrimePowerCompletedCoeff ℓ G) :
102 (i : PrimePowerCompletedGroupAlgebraIndex G) →
103 (primePowerCompletedCoeffSystem ℓ G).X i) =
104 (1 :
105 (i : PrimePowerCompletedGroupAlgebraIndex G) →
106 (primePowerCompletedCoeffSystem ℓ G).X i) := by
107 funext i
108 rfl
110omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
111/-- 素冪係数で定めた 係数側の射影または係数変更写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
112@[simp]
114 (x y : PrimePowerCompletedCoeff ℓ G) :
115 ((x * y : PrimePowerCompletedCoeff ℓ G) :
116 (i : PrimePowerCompletedGroupAlgebraIndex G) →
117 (primePowerCompletedCoeffSystem ℓ G).X i) =
118 (x * y :
119 (i : PrimePowerCompletedGroupAlgebraIndex G) →
120 (primePowerCompletedCoeffSystem ℓ G).X i) := by
121 funext i
122 rfl
124omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
125/-- 素冪係数で定めた 係数側の射影または係数変更写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
126@[simp]
128 (n : ℕ) :
129 ((n : PrimePowerCompletedCoeff ℓ G) :
130 (i : PrimePowerCompletedGroupAlgebraIndex G) →
131 (primePowerCompletedCoeffSystem ℓ G).X i) =
132 (n :
133 (i : PrimePowerCompletedGroupAlgebraIndex G) →
134 (primePowerCompletedCoeffSystem ℓ G).X i) := by
135 funext i
136 rfl
138omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
139/-- 素冪係数で定めた 係数側の射影または係数変更写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
140@[simp]
142 (n : ℤ) :
143 ((n : PrimePowerCompletedCoeff ℓ G) :
144 (i : PrimePowerCompletedGroupAlgebraIndex G) →
145 (primePowerCompletedCoeffSystem ℓ G).X i) =
146 (n :
147 (i : PrimePowerCompletedGroupAlgebraIndex G) →
148 (primePowerCompletedCoeffSystem ℓ G).X i) := by
149 funext i
150 rfl
152omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
153/-- 素冪係数で定めた 係数側の射影または係数変更写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
154@[simp]
156 (x : PrimePowerCompletedCoeff ℓ G) (n : ℕ) :
157 ((x ^ n : PrimePowerCompletedCoeff ℓ G) :
158 (i : PrimePowerCompletedGroupAlgebraIndex G) →
159 (primePowerCompletedCoeffSystem ℓ G).X i) =
160 (x ^ n :
161 (i : PrimePowerCompletedGroupAlgebraIndex G) →
162 (primePowerCompletedCoeffSystem ℓ G).X i) := by
163 funext i
164 rfl
166instance instCommRingPrimePowerCompletedCoeff :
167 CommRing (PrimePowerCompletedCoeff ℓ G) :=
168 Function.Injective.commRing
169 (fun x : PrimePowerCompletedCoeff ℓ G =>
170 (x :
171 (i : PrimePowerCompletedGroupAlgebraIndex G) →
172 (primePowerCompletedCoeffSystem ℓ G).X i))
173 Subtype.val_injective
174 (coe_zero_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
175 (coe_one_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
176 (coe_add_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
177 (coe_mul_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
178 (coe_neg_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
179 (coe_sub_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
180 (fun n x => coe_nsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) n x)
181 (fun n x => coe_zsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) n x)
182 (fun x n => coe_pow_primePowerCompletedCoeff (ℓ := ℓ) (G := G) x n)
183 (by
184 intro n
185 exact coe_natCast_primePowerCompletedCoeff (ℓ := ℓ) (G := G) n)
186 (by
187 intro z
188 exact coe_intCast_primePowerCompletedCoeff (ℓ := ℓ) (G := G) z)
190end
192end FoxDifferential