FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System/Basic.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation
2import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.Coeff
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Completed coefficient algebras
15Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.
16-/
17namespace FoxDifferential
19noncomputable section
21open ProCGroups.InverseSystems
22open ProCGroups.ProC
24universe u
26variable (ℓ : ℕ) [Fact (0 < ℓ)]
27variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29omit [Fact (0 < ℓ)] in
30/-- The stage at index `(a, U)`, namely `(ZMod (ℓ^a))[G/U]`. -/
32 (i : PrimePowerCompletedGroupAlgebraIndex G) : Type _ :=
33 ModNCompletedGroupAlgebraStage (ℓ ^ i.1) G i.2
36 (i : PrimePowerCompletedGroupAlgebraIndex G) :
37 Finite (PrimePowerCompletedGroupAlgebraStage ℓ G i) := by
38 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
39 exact instFiniteModNCompletedGroupAlgebraStage (n := ℓ ^ i.1) (G := G) i.2
41omit [Fact (0 < ℓ)] in
42/-- The combined transition map for the two-parameter prime-power stage calculus. -/
44 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
45 PrimePowerCompletedGroupAlgebraStage ℓ G j →+* PrimePowerCompletedGroupAlgebraStage ℓ G i := by
46 exact
48 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
49 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
50 (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hij.2)
52omit [Fact (0 < ℓ)] in
53/-- Evaluation formula for primePowerCompletedGroupAlgebraTransition_of. -/
54@[simp]
56 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
57 (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G j.2) :
58 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
59 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1)) _ q) =
60 MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
61 ((OpenNormalSubgroupInClass.map
62 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
63 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) := by
64 rw [primePowerCompletedGroupAlgebraTransition, RingHom.comp_apply,
66 simpa using
68 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) (U := i.2)
69 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
70 ((OpenNormalSubgroupInClass.map
71 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
72 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q))
74omit [Fact (0 < ℓ)] in
75/-- The combined transition first follows the quotient-direction map at the larger modulus and then
76reduces coefficients. -/
77@[simp]
79 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
80 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij =
82 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
83 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
84 (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hij.2) := by
85 rfl
87omit [Fact (0 < ℓ)] in
88/-- The same combined transition can also be read as coefficient reduction at the source stage
89followed by the quotient-direction transition at the smaller modulus. -/
91 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
92 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij =
93 (modNCompletedGroupAlgebraTransition (ℓ ^ i.1) G hij.2).comp
95 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) j.2
96 (primePow_dvd_primePow (ℓ := ℓ) hij.1)) := by
99 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) (U := i.2) (V := j.2)
100 hij.2 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
102omit [Fact (0 < ℓ)] in
103/-- Identity case for primePowerCompletedGroupAlgebraTransition_id. -/
104@[simp]
106 (i : PrimePowerCompletedGroupAlgebraIndex G) :
107 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) (le_rfl : i ≤ i) =
108 RingHom.id _ := by
111 simp only [RingHomCompTriple.comp_eq]
113omit [Fact (0 < ℓ)] in
114/-- Composition lemma primePowerCompletedGroupAlgebraTransition_comp. -/
115@[simp 900]
117 {i j k : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) (hjk : j ≤ k) :
118 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij).comp
119 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hjk) =
120 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) (hij.trans hjk) := by
121 calc
122 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij).comp
123 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hjk)
124 =
126 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
127 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
128 (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hij.2)).comp
129 ((modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hjk.2).comp
131 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
132 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
135 _ =
137 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
138 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
139 (((modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hij.2).comp
140 (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hjk.2)).comp
142 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
143 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
144 apply RingHom.ext
145 intro x
146 rfl
147 _ =
149 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
150 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
151 ((modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G (hij.2.trans hjk.2)).comp
153 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
154 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
156 _ =
158 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
159 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
160 (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G (hij.2.trans hjk.2))).comp
162 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
163 (primePow_dvd_primePow (ℓ := ℓ) hjk.1)) := by
164 rw [← RingHom.comp_assoc]
165 _ =
166 ((modNCompletedGroupAlgebraTransition (ℓ ^ i.1) G (hij.2.trans hjk.2)).comp
168 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) k.2
169 (primePow_dvd_primePow (ℓ := ℓ) hij.1))).comp
171 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
172 (primePow_dvd_primePow (ℓ := ℓ) hjk.1)) := by
174 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G)
175 (U := i.2) (V := k.2) (hUV := hij.2.trans hjk.2)
176 (hnm := primePow_dvd_primePow (ℓ := ℓ) hij.1)]
177 _ =
178 (modNCompletedGroupAlgebraTransition (ℓ ^ i.1) G (hij.2.trans hjk.2)).comp
180 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) k.2
181 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
183 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
184 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
185 rw [RingHom.comp_assoc]
186 _ =
187 (modNCompletedGroupAlgebraTransition (ℓ ^ i.1) G (hij.2.trans hjk.2)).comp
189 (n := ℓ ^ i.1) (m := ℓ ^ k.1) (G := G) k.2
190 (primePow_dvd_primePow (ℓ := ℓ) (hij.trans hjk).1)) := by
192 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (k := ℓ ^ k.1) (G := G) (U := k.2)
193 (hnm := primePow_dvd_primePow (ℓ := ℓ) hij.1)
194 (hmk := primePow_dvd_primePow (ℓ := ℓ) hjk.1)]
195 _ =
196 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) (hij.trans hjk) := by
198 (ℓ := ℓ) (G := G) (hij := hij.trans hjk)]
200omit [Fact (0 < ℓ)] in
201/-- The inverse system indexed by prime powers and finite quotients. -/
203 InverseSystem (I := PrimePowerCompletedGroupAlgebraIndex G) where
204 X := PrimePowerCompletedGroupAlgebraStage ℓ G
205 topologicalSpace := fun _ => ⊥
206 map := fun {i j} hij => primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
207 continuous_map := by
208 intro i j hij
209 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ G i) := ⊥
210 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ G j) := ⊥
211 letI : DiscreteTopology (PrimePowerCompletedGroupAlgebraStage ℓ G j) := ⟨rfl⟩
212 exact continuous_of_discreteTopology
213 map_id := by
214 intro i
215 funext x
216 exact congrFun
217 (congrArg DFunLike.coe
218 (primePowerCompletedGroupAlgebraTransition_id (ℓ := ℓ) (G := G) i)) x
219 map_comp := by
220 intro i j k hij hjk
221 funext x
222 exact congrFun
223 (congrArg DFunLike.coe
224 (primePowerCompletedGroupAlgebraTransition_comp (ℓ := ℓ) (G := G) hij hjk)) x
226omit [Fact (0 < ℓ)] in
227/-- The inverse-limit object of the prime-power finite-stage system. -/
228abbrev PrimePowerCompletedGroupAlgebra :=
229 (primePowerCompletedGroupAlgebraSystem ℓ G).inverseLimit
231omit [Fact (0 < ℓ)] in
232/-- The projection from the prime-power completed group algebra to one finite stage. -/
235 (primePowerCompletedGroupAlgebraSystem ℓ G).projection i
237omit [IsTopologicalGroup G] in
238/-- The prime-power group-algebra index family is directed under the componentwise order. -/
240 Directed (· ≤ ·) (id : PrimePowerCompletedGroupAlgebraIndex G →
241 PrimePowerCompletedGroupAlgebraIndex G) := by
242 intro i j
244 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
245 ProCGroups.FiniteGroupClass.allFinite_formation i.2 j.2 with ⟨U, hiU, hjU⟩
246 refine ⟨(max i.1 j.1, U), ?_, ?_⟩
247 · exact ⟨le_max_left _ _, hiU⟩
248 · exact ⟨le_max_right _ _, hjU⟩
250omit [Fact (0 < ℓ)] in
251/-- Every transition in the prime-power completed group-algebra system is surjective. -/
253 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
254 Function.Surjective
255 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij) := by
256 intro x
258 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
259 (primePow_dvd_primePow (ℓ := ℓ) hij.1) x with
260 ⟨y, hy⟩
262 (n := ℓ ^ j.1) (G := G) hij.2 y with
263 ⟨z, hz⟩
264 refine ⟨z, ?_⟩
265 rw [primePowerCompletedGroupAlgebraTransition_eq, RingHom.comp_apply, hz, hy]
267/-- Every finite-stage projection from the prime-power completed group algebra is surjective. -/
269 (i : PrimePowerCompletedGroupAlgebraIndex G) :
270 Function.Surjective (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i) := by
271 let S := primePowerCompletedGroupAlgebraSystem ℓ G
272 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, TopologicalSpace (S.X i) :=
273 fun i => S.topologicalSpace i
274 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, DiscreteTopology (S.X i) :=
275 fun _ => ⟨rfl⟩
276 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, CompactSpace (S.X i) :=
277 fun i => by
278 letI : Finite (S.X i) := by
279 dsimp [S, primePowerCompletedGroupAlgebraSystem]
280 infer_instance
281 letI : Fintype (S.X i) := Fintype.ofFinite _
282 infer_instance
283 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, T2Space (S.X i) :=
284 fun _ => inferInstance
285 change Function.Surjective (S.projection i)
286 exact
287 S.surjective_π
288 (directed_primePowerCompletedGroupAlgebraIndex (G := G))
289 (fun {i j} hij =>
290 primePowerCompletedGroupAlgebraTransition_surjective (ℓ := ℓ) (G := G) hij)
291 i
293end
295end FoxDifferential