Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Basic
ProCGroups/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System/Basic/Source

Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Basic

1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation
2import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.Coeff
4/-!
5# Fox differential: coefficient rings — prime-power completed group algebra — system — basic
7The principal declarations in this module are:
9- `PrimePowerCompletedGroupAlgebraStage`
10 The stage at index \((a,U)\), namely \((\mathrm{ZMod}\,\ell^a)[G/U]\).
11- `primePowerCompletedGroupAlgebraTransition`
12 The combined transition map for the two-parameter prime-power stage calculus.
13- `primePowerCompletedGroupAlgebraTransition_of`
14 The transition map sends a group-like basis element to the basis element supported at its image in
15 the coarser quotient in the Fox differential construction.
16- `primePowerCompletedGroupAlgebraTransition_eq`
17 The transition map for the prime-power completed group algebra commutes with the finite-stage
18 coordinate maps.
19-/
21namespace FoxDifferential
23noncomputable section
25open ProCGroups.InverseSystems
26open ProCGroups.ProC
28universe u
30variable (ℓ : ℕ) [Fact (0 < ℓ)]
31variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33omit [Fact (0 < ℓ)] in
34/-- The stage at index \((a,U)\), namely \((\mathrm{ZMod}\,\ell^a)[G/U]\). -/
35abbrev PrimePowerCompletedGroupAlgebraStage
36 (i : PrimePowerCompletedGroupAlgebraIndex G) : Type _ :=
37 ModNCompletedGroupAlgebraStage (ℓ ^ i.1) G i.2
39/-- Each prime-power completed group-algebra stage is finite. -/
40instance instFinitePrimePowerCompletedGroupAlgebraStage
41 (i : PrimePowerCompletedGroupAlgebraIndex G) :
42 Finite (PrimePowerCompletedGroupAlgebraStage ℓ G i) := by
43 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
44 exact instFiniteModNCompletedGroupAlgebraStage (n := ℓ ^ i.1) (G := G) i.2
46omit [Fact (0 < ℓ)] in
47/-- The combined transition map for the two-parameter prime-power stage calculus. -/
48def primePowerCompletedGroupAlgebraTransition
49 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
50 PrimePowerCompletedGroupAlgebraStage ℓ G j →+* PrimePowerCompletedGroupAlgebraStage ℓ G i := by
51 exact
52 (modNCompletedGroupAlgebraStageCoeffMap
53 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
54 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
55 (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hij.2)
57omit [Fact (0 < ℓ)] in
58/--
59The transition map sends a group-like basis element to the basis element supported at its image
60in the coarser quotient in the Fox differential construction.
61-/
62@[simp]
63theorem primePowerCompletedGroupAlgebraTransition_of
64 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
65 (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G j.2) :
66 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
67 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1)) _ q) =
68 MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
69 ((OpenNormalSubgroupInClass.map
71 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) := by
72 rw [primePowerCompletedGroupAlgebraTransition, RingHom.comp_apply,
73 modNCompletedGroupAlgebraTransition_of]
74 change
75 (modNCompletedGroupAlgebraStageCoeffMap
76 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
77 (primePow_dvd_primePow (ℓ := ℓ) hij.1))
78 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1)) _
79 ((OpenNormalSubgroupInClass.map
81 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)) =
82 MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
83 ((OpenNormalSubgroupInClass.map
85 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
86 exact modNCompletedGroupAlgebraStageCoeffMap_of
87 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) (U := i.2)
88 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
89 ((OpenNormalSubgroupInClass.map
91 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
93omit [Fact (0 < ℓ)] in
94/--
95The transition map for the prime-power completed group algebra commutes with the finite-stage
96coordinate maps.
97-/
98@[simp]
99theorem primePowerCompletedGroupAlgebraTransition_eq
100 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
101 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij =
102 (modNCompletedGroupAlgebraStageCoeffMap
103 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
104 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
105 (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hij.2) := by
106 rfl
108omit [Fact (0 < ℓ)] in
109/--
110The same combined transition can also be read as coefficient reduction at the source stage
111followed by the quotient-direction transition at the smaller modulus.
112-/
113theorem primePowerCompletedGroupAlgebraTransition_eq'
114 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
115 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij =
116 (modNCompletedGroupAlgebraTransition (ℓ ^ i.1) G hij.2).comp
117 (modNCompletedGroupAlgebraStageCoeffMap
118 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) j.2
119 (primePow_dvd_primePow (ℓ := ℓ) hij.1)) := by
120 rw [primePowerCompletedGroupAlgebraTransition_eq]
121 exact modNCompletedGroupAlgebraStageCoeffMap_compatible
122 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) (U := i.2) (V := j.2)
123 hij.2 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
125omit [Fact (0 < ℓ)] in
126/--
127The transition map attached to the identity refinement is the identity homomorphism in the Fox
128differential construction.
129-/
130@[simp]
131theorem primePowerCompletedGroupAlgebraTransition_id
132 (i : PrimePowerCompletedGroupAlgebraIndex G) :
133 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) (le_rfl : i ≤ i) =
134 RingHom.id _ := by
135 rw [primePowerCompletedGroupAlgebraTransition_eq]
136 rw [modNCompletedGroupAlgebraTransition_id, modNCompletedGroupAlgebraStageCoeffMap_rfl]
137 simp only [RingHomCompTriple.comp_eq]
139omit [Fact (0 < ℓ)] in
140/--
141Prime-power completed group-algebra transitions compose along a chain of quotient refinements.
142-/
143@[simp 900]
144theorem primePowerCompletedGroupAlgebraTransition_comp
145 {i j k : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) (hjk : j ≤ k) :
146 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij).comp
147 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hjk) =
148 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) (hij.trans hjk) := by
149 calc
150 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij).comp
151 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hjk)
152 =
153 ((modNCompletedGroupAlgebraStageCoeffMap
154 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
155 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
156 (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hij.2)).comp
157 ((modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hjk.2).comp
158 (modNCompletedGroupAlgebraStageCoeffMap
159 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
160 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
161 rw [primePowerCompletedGroupAlgebraTransition_eq,
162 primePowerCompletedGroupAlgebraTransition_eq']
163 _ =
164 (modNCompletedGroupAlgebraStageCoeffMap
165 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
166 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
167 (((modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hij.2).comp
168 (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hjk.2)).comp
169 (modNCompletedGroupAlgebraStageCoeffMap
170 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
171 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
172 apply RingHom.ext
173 intro x
174 rfl
175 _ =
176 (modNCompletedGroupAlgebraStageCoeffMap
177 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
178 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
179 ((modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G (hij.2.trans hjk.2)).comp
180 (modNCompletedGroupAlgebraStageCoeffMap
181 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
182 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
183 rw [modNCompletedGroupAlgebraTransition_comp]
184 _ =
185 ((modNCompletedGroupAlgebraStageCoeffMap
186 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
187 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
188 (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G (hij.2.trans hjk.2))).comp
189 (modNCompletedGroupAlgebraStageCoeffMap
190 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
191 (primePow_dvd_primePow (ℓ := ℓ) hjk.1)) := by
192 rw [← RingHom.comp_assoc]
193 _ =
194 ((modNCompletedGroupAlgebraTransition (ℓ ^ i.1) G (hij.2.trans hjk.2)).comp
195 (modNCompletedGroupAlgebraStageCoeffMap
196 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) k.2
197 (primePow_dvd_primePow (ℓ := ℓ) hij.1))).comp
198 (modNCompletedGroupAlgebraStageCoeffMap
199 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
200 (primePow_dvd_primePow (ℓ := ℓ) hjk.1)) := by
201 rw [modNCompletedGroupAlgebraStageCoeffMap_compatible
202 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G)
203 (U := i.2) (V := k.2) (hUV := hij.2.trans hjk.2)
204 (hnm := primePow_dvd_primePow (ℓ := ℓ) hij.1)]
205 _ =
206 (modNCompletedGroupAlgebraTransition (ℓ ^ i.1) G (hij.2.trans hjk.2)).comp
207 ((modNCompletedGroupAlgebraStageCoeffMap
208 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) k.2
209 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
210 (modNCompletedGroupAlgebraStageCoeffMap
211 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) k.2
212 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
213 rw [RingHom.comp_assoc]
214 _ =
215 (modNCompletedGroupAlgebraTransition (ℓ ^ i.1) G (hij.2.trans hjk.2)).comp
216 (modNCompletedGroupAlgebraStageCoeffMap
217 (n := ℓ ^ i.1) (m := ℓ ^ k.1) (G := G) k.2
218 (primePow_dvd_primePow (ℓ := ℓ) (hij.trans hjk).1)) := by
219 rw [modNCompletedGroupAlgebraStageCoeffMap_comp
220 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (k := ℓ ^ k.1) (G := G) (U := k.2)
221 (hnm := primePow_dvd_primePow (ℓ := ℓ) hij.1)
222 (hmk := primePow_dvd_primePow (ℓ := ℓ) hjk.1)]
223 _ =
224 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) (hij.trans hjk) := by
225 rw [← primePowerCompletedGroupAlgebraTransition_eq'
226 (ℓ := ℓ) (G := G) (hij := hij.trans hjk)]
228omit [Fact (0 < ℓ)] in
229/-- The inverse system indexed by prime powers and finite quotients. -/
230def primePowerCompletedGroupAlgebraSystem :
231 InverseSystem (I := PrimePowerCompletedGroupAlgebraIndex G) where
232 X := PrimePowerCompletedGroupAlgebraStage ℓ G
233 topologicalSpace := fun _ => ⊥
234 map := fun {i j} hij => primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
235 continuous_map := by
236 intro i j hij
237 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ G i) := ⊥
238 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ G j) := ⊥
239 letI : DiscreteTopology (PrimePowerCompletedGroupAlgebraStage ℓ G j) := ⟨rfl⟩
240 exact continuous_of_discreteTopology
241 map_id := by
242 intro i
243 funext x
244 exact congrFun
245 (congrArg DFunLike.coe
246 (primePowerCompletedGroupAlgebraTransition_id (ℓ := ℓ) (G := G) i)) x
247 map_comp := by
248 intro i j k hij hjk
249 funext x
250 exact congrFun
251 (congrArg DFunLike.coe
252 (primePowerCompletedGroupAlgebraTransition_comp (ℓ := ℓ) (G := G) hij hjk)) x
254omit [Fact (0 < ℓ)] in
255/-- The inverse-limit object of the prime-power finite-stage system. -/
256abbrev PrimePowerCompletedGroupAlgebra :=
257 (primePowerCompletedGroupAlgebraSystem ℓ G).inverseLimit
259omit [Fact (0 < ℓ)] in
260/-- The projection from the prime-power completed group algebra to one finite stage. -/
261abbrev primePowerCompletedGroupAlgebraProjection (i : PrimePowerCompletedGroupAlgebraIndex G) :
262 PrimePowerCompletedGroupAlgebra ℓ G → PrimePowerCompletedGroupAlgebraStage ℓ G i :=
263 (primePowerCompletedGroupAlgebraSystem ℓ G).projection i
265omit [IsTopologicalGroup G] in
266/-- The prime-power group-algebra index family is directed under the componentwise order. -/
267theorem directed_primePowerCompletedGroupAlgebraIndex :
268 Directed (· ≤ ·) (id : PrimePowerCompletedGroupAlgebraIndex G →
269 PrimePowerCompletedGroupAlgebraIndex G) := by
270 intro i j
271 rcases directed_openNormalSubgroupInClass
274 refine ⟨(max i.1 j.1, U), ?_, ?_⟩
275 · exact ⟨le_max_left _ _, hiU⟩
276 · exact ⟨le_max_right _ _, hjU⟩
278omit [Fact (0 < ℓ)] in
279/-- Every transition in the prime-power completed group-algebra system is surjective. -/
280theorem primePowerCompletedGroupAlgebraTransition_surjective
281 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
282 Function.Surjective
283 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij) := by
284 intro x
285 rcases modNCompletedGroupAlgebraStageCoeffMap_surjective
286 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
287 (primePow_dvd_primePow (ℓ := ℓ) hij.1) x with
288 ⟨y, hy⟩
289 rcases modNCompletedGroupAlgebraTransition_surjective
290 (n := ℓ ^ j.1) (G := G) hij.2 y with
291 ⟨z, hz⟩
292 refine ⟨z, ?_⟩
293 rw [primePowerCompletedGroupAlgebraTransition_eq, RingHom.comp_apply, hz, hy]
295/-- Every finite-stage projection from the prime-power completed group algebra is surjective. -/
296theorem primePowerCompletedGroupAlgebraProjection_surjective
297 (i : PrimePowerCompletedGroupAlgebraIndex G) :
298 Function.Surjective (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i) := by
299 let S := primePowerCompletedGroupAlgebraSystem ℓ G
300 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, TopologicalSpace (S.X i) :=
301 fun i => S.topologicalSpace i
302 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, DiscreteTopology (S.X i) :=
303 fun _ => ⟨rfl⟩
304 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, CompactSpace (S.X i) :=
305 fun i => by
306 letI : Finite (S.X i) := by
307 dsimp [S, primePowerCompletedGroupAlgebraSystem]
308 infer_instance
309 letI : Fintype (S.X i) := Fintype.ofFinite _
310 infer_instance
311 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, T2Space (S.X i) :=
312 fun _ => inferInstance
313 change Function.Surjective (S.projection i)
314 exact
315 S.surjective_π
316 (directed_primePowerCompletedGroupAlgebraIndex (G := G))
317 (fun {i j} hij =>
318 primePowerCompletedGroupAlgebraTransition_surjective (ℓ := ℓ) (G := G) hij)
319 i
321end
323end FoxDifferential