FoxDifferential/Completed/FreeProC/ProCIntegerStageCoeffProjection.lean
1import FoxDifferential.Completed.FreeProC.BifilteredCoefficientStageProjection
2import FoxDifferential.Completed.ProCIntegerCoefficients.Core
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/FreeProC/ProCIntegerStageCoeffProjection.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Finite Fox stage maps from actual `Z_C[[H]]` projections
15This file constructs the coefficient map
17`Z_C[[H]] -> (Z/nZ)[F/N]`
21maps feed the coefficient-level bifiltered density API.
22-/
24namespace FoxDifferential
26noncomputable section
28open ProCGroups.ProC
29open ProCGroups.InverseSystems
31universe u v
33section OneStageToFiniteFox
35variable {ProC : ProCGroups.ProC.ProCGroupPredicate}
36variable {X H : Type u}
37variable [DecidableEq X]
38variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
39variable (N : Subgroup (FreeGroup X)) [N.Normal]
40variable (n : ℕ) [Fact (0 < n)]
41variable (i : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H)
43/-- A finite stage of `Z_C[[H]]` maps to a finite Fox target group algebra once its coefficient
46 (hmod : n ∣ i.1.modulus)
47 (qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
48 finiteFoxStageTargetQuotient (X := X) N) :
49 ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H i →+*
50 finiteFoxStageTargetGroupAlgebra (X := X) N n := by
51 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
52 letI : Algebra (ModNCompletedCoeff i.1.modulus) (ModNCompletedCoeff n) :=
53 ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := i.1.modulus) hmod
54 letI : Algebra (ModNCompletedCoeff i.1.modulus)
55 (finiteFoxStageTargetGroupAlgebra (X := X) N n) := inferInstance
56 exact
57 (MonoidAlgebra.lift (ModNCompletedCoeff i.1.modulus)
58 (finiteFoxStageTargetGroupAlgebra (X := X) N n)
59 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2)
60 ((MonoidAlgebra.of (ModNCompletedCoeff n)
61 (finiteFoxStageTargetQuotient (X := X) N)).comp qmap)).toRingHom
63omit [DecidableEq X] [Fact (0 < n)] in
64/-- Evaluation on a completed group-algebra stage basis element. -/
65@[simp]
67 (hmod : n ∣ i.1.modulus)
68 (qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
69 finiteFoxStageTargetQuotient (X := X) N)
70 (q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2) :
72 (ProC := ProC) (X := X) (H := H) N n i hmod qmap
73 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
74 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2) q) =
75 MonoidAlgebra.of (ModNCompletedCoeff n)
76 (finiteFoxStageTargetQuotient (X := X) N) (qmap q) := by
77 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
78 simp only [zcCompletedGroupAlgebraStageToFiniteFoxStage, AlgHom.toRingHom_eq_coe, MonoidAlgebra.of_apply,
79 RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.coe_comp, Function.comp_apply, MonoidAlgebra.smul_single,
80 one_smul]
82omit [DecidableEq X] [Fact (0 < n)] in
83/-- Evaluation on a single coefficient at a stage quotient element. -/
85 (hmod : n ∣ i.1.modulus)
86 (qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
87 finiteFoxStageTargetQuotient (X := X) N)
88 (q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2)
89 (a : ModNCompletedCoeff i.1.modulus) :
91 (ProC := ProC) (X := X) (H := H) N n i hmod qmap
92 (MonoidAlgebra.single q a) =
93 MonoidAlgebra.single (qmap q)
94 (modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod a) := by
95 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
96 letI : Algebra (ModNCompletedCoeff i.1.modulus) (ModNCompletedCoeff n) :=
97 ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := i.1.modulus) hmod
98 have hcoeff :
99 algebraMap (ModNCompletedCoeff i.1.modulus) (ModNCompletedCoeff n) a =
100 modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod a := by
101 rfl
103 ext q'
104 simp only [AlgHom.toRingHom_eq_coe, MonoidAlgebra.single, RingHom.coe_coe, MonoidAlgebra.lift_single,
105 MonoidHom.coe_comp, Function.comp_apply, MonoidAlgebra.of_apply, Algebra.smul_def, MonoidAlgebra.coe_algebraMap,
106 hcoeff, MonoidAlgebra.single_mul_single, one_mul, mul_one]
108omit [DecidableEq X] in
109/-- If no coefficient reduction is taken and the target quotient comparison is injective, then the
110finite-stage map from the completed group-algebra stage to the finite Fox target group algebra is
111injective. -/
113 (qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
114 finiteFoxStageTargetQuotient (X := X) N)
115 (hqmap : Function.Injective qmap) :
116 Function.Injective
118 (ProC := ProC) (X := X) (H := H) N i.1.modulus i dvd_rfl qmap) := by
119 classical
120 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
121 have hstage :
123 (ProC := ProC) (X := X) (H := H) N i.1.modulus i dvd_rfl qmap =
124 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus) qmap := by
125 apply MonoidAlgebra.ringHom_ext
126 · intro r
128 simp only [map_one, modNCompletedCoeffMap_rfl, RingHom.id_apply, MonoidAlgebra.mapDomainRingHom_apply,
129 Finsupp.mapDomain_single]
130 · intro q
131 rw [← MonoidAlgebra.of_apply,
133 simp only [MonoidAlgebra.of_apply, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
134 rw [hstage]
135 intro x y hxy
136 exact (MonoidAlgebra.mapDomain_injective
137 (R := ModNCompletedCoeff i.1.modulus) hqmap) (by
138 simpa [MonoidAlgebra.mapDomainRingHom_apply] using hxy)
140/-- The resulting completed-to-finite coefficient map. -/
142 (hmod : n ∣ i.1.modulus)
143 (qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
144 finiteFoxStageTargetQuotient (X := X) N) :
145 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+*
146 finiteFoxStageTargetGroupAlgebra (X := X) N n :=
148 (ProC := ProC) (X := X) (H := H) N n i hmod qmap).comp
149 (zcCompletedGroupAlgebraProjectionRingHom ProC.finiteQuotientClass H i)
151omit [DecidableEq X] [Fact (0 < n)] in
152@[simp]
154 (hmod : n ∣ i.1.modulus)
155 (qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
156 finiteFoxStageTargetQuotient (X := X) N)
157 (a : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) :
159 (ProC := ProC) (X := X) (H := H) N n i hmod qmap a =
161 (ProC := ProC) (X := X) (H := H) N n i hmod qmap
162 (zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass H i a) :=
163 rfl
165omit [DecidableEq X] [Fact (0 < n)] in
166/-- Group-like formula for the completed-to-finite coefficient map. -/
168 (hmod : n ∣ i.1.modulus)
169 (qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
170 finiteFoxStageTargetQuotient (X := X) N)
171 (h : H) :
173 (ProC := ProC) (X := X) (H := H) N n i hmod qmap
174 (zcGroupLike ProC.finiteQuotientClass H h) =
175 MonoidAlgebra.of (ModNCompletedCoeff n)
176 (finiteFoxStageTargetQuotient (X := X) N)
177 (qmap (QuotientGroup.mk h)) := by
182omit [DecidableEq X] [Fact (0 < n)] in
183/-- Group-like formula rewritten through a named finite right quotient map. -/
185 (hmod : n ∣ i.1.modulus)
186 (qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
187 finiteFoxStageTargetQuotient (X := X) N)
188 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
189 (hqmap : ∀ h : H, qmap (QuotientGroup.mk h) = stageRight h)
190 (h : H) :
192 (ProC := ProC) (X := X) (H := H) N n i hmod qmap
193 (zcGroupLike ProC.finiteQuotientClass H h) =
194 MonoidAlgebra.of (ModNCompletedCoeff n)
195 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h) := by
197 rw [hqmap h]
199end OneStageToFiniteFox
201section SingleCoefficientTransitions
203variable {X : Type u} [DecidableEq X]
204variable {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
205variable (hNM : N ≤ M)
206variable {n m : ℕ} [Fact (0 < n)] [Fact (0 < m)]
207variable (hnm : n ∣ m)
209omit [DecidableEq X] [Fact (0 < n)] in
210/-- Target quotient maps send a single group-algebra coefficient to the mapped basis element. -/
212 (q : finiteFoxStageTargetQuotient (X := X) N)
213 (a : ModNCompletedCoeff n) :
214 finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n
215 (MonoidAlgebra.single q a) =
216 MonoidAlgebra.single (finiteFoxStageTargetQuotientMap (X := X) hNM q) a := by
218 rw [MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single]
220omit [DecidableEq X] [Fact (0 < n)] [Fact (0 < m)] in
221/-- The bifiltered target transition on a single group-algebra coefficient. -/
223 (q : finiteFoxStageTargetQuotient (X := X) N)
224 (a : ModNCompletedCoeff m) :
225 finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
226 (MonoidAlgebra.single q a) =
227 MonoidAlgebra.single (finiteFoxStageTargetQuotientMap (X := X) hNM q)
228 (modNCompletedCoeffMap (n := n) (m := m) hnm a) := by
233end SingleCoefficientTransitions
235section Transition
237variable {ProC : ProCGroups.ProC.ProCGroupPredicate}
238variable {X H : Type u}
239variable [DecidableEq X]
240variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
241variable {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
242variable (hNM : N ≤ M)
243variable {n m : ℕ} [Fact (0 < n)] [Fact (0 < m)]
244variable (hnm : n ∣ m)
245variable {i j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H}
246variable (hij : i ≤ j)
248omit [DecidableEq X] [Fact (0 < n)] [Fact (0 < m)] in
249/-- Stage-to-finite maps commute with completed-group-algebra transitions when the coefficient
250reductions and quotient maps commute. -/
252 (hmod_i : n ∣ i.1.modulus)
253 (hmod_j : m ∣ j.1.modulus)
254 (hcoeff : ∀ a : ModNCompletedCoeff j.1.modulus,
255 modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod_i
256 (modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a) =
257 modNCompletedCoeffMap (n := n) (m := m) hnm
258 (modNCompletedCoeffMap (n := m) (m := j.1.modulus) hmod_j a))
259 (qmap_i : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
260 finiteFoxStageTargetQuotient (X := X) M)
261 (qmap_j : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2 →*
262 finiteFoxStageTargetQuotient (X := X) N)
263 (hqmap : ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2,
264 qmap_i
265 ((OpenNormalSubgroupInClass.map
266 (C := ProC.finiteQuotientClass) (G := H)
267 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) =
268 finiteFoxStageTargetQuotientMap (X := X) hNM (qmap_j q))
269 (x : ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H j) :
270 finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
272 (ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j x) =
274 (ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
275 (zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij x) := by
276 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
277 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
278 refine MonoidAlgebra.induction_on
279 (p := fun x : ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H j =>
280 finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
282 (ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j x) =
284 (ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
285 (zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij x))
286 x ?_ ?_ ?_
287 · intro q
288 calc
289 finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
291 (ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j
292 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
293 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2) q)) =
294 finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
295 (MonoidAlgebra.of (ModNCompletedCoeff m)
296 (finiteFoxStageTargetQuotient (X := X) N) (qmap_j q)) := by
298 _ = MonoidAlgebra.of (ModNCompletedCoeff n)
299 (finiteFoxStageTargetQuotient (X := X) M)
300 (finiteFoxStageTargetQuotientMap (X := X) hNM (qmap_j q)) := by
304 _ = MonoidAlgebra.of (ModNCompletedCoeff n)
305 (finiteFoxStageTargetQuotient (X := X) M)
306 (qmap_i
307 ((OpenNormalSubgroupInClass.map
308 (C := ProC.finiteQuotientClass) (G := H)
309 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)) := by
310 rw [← hqmap q]
312 (ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
313 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
314 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2)
315 ((OpenNormalSubgroupInClass.map
316 (C := ProC.finiteQuotientClass) (G := H)
317 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)) := by
320 (ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
321 (zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij
322 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
323 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2) q)) := by
325 rfl
326 · intro x y hx hy
330 (ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i)
331 ((zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij) x)
332 ((zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij) y)).symm
333 · intro a x hx
334 have hscalar :
335 finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
337 (ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j
338 (algebraMap (ModNCompletedCoeff j.1.modulus)
339 (ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H j) a)) =
341 (ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
342 (zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij
343 (algebraMap (ModNCompletedCoeff j.1.modulus)
344 (ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H j) a)) := by
345 change
346 finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
348 (ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j
349 (MonoidAlgebra.single
350 (1 : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2)
351 a)) =
353 (ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
354 (zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij
355 (MonoidAlgebra.single
356 (1 : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2)
357 a))
362 rw [← hqmap 1]
363 rw [hcoeff a]
364 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul,
365 RingHom.map_mul, RingHom.map_mul, hx]
366 rw [hscalar]
368omit [DecidableEq X] [Fact (0 < n)] [Fact (0 < m)] in
369/-- The completed coefficient maps built from stage projections are compatible on completed
372 (hmod_i : n ∣ i.1.modulus)
373 (hmod_j : m ∣ j.1.modulus)
374 (hcoeff : ∀ a : ModNCompletedCoeff j.1.modulus,
375 modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod_i
376 (modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a) =
377 modNCompletedCoeffMap (n := n) (m := m) hnm
378 (modNCompletedCoeffMap (n := m) (m := j.1.modulus) hmod_j a))
379 (qmap_i : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
380 finiteFoxStageTargetQuotient (X := X) M)
381 (qmap_j : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2 →*
382 finiteFoxStageTargetQuotient (X := X) N)
383 (hqmap : ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2,
384 qmap_i
385 ((OpenNormalSubgroupInClass.map
386 (C := ProC.finiteQuotientClass) (G := H)
387 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) =
388 finiteFoxStageTargetQuotientMap (X := X) hNM (qmap_j q))
389 (a : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) :
390 finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
392 (ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j a) =
394 (ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i a := by
397 change finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
399 (ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j (a.1 j)) =
401 (ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i (a.1 i)
402 rw [← a.2 i j hij]
404 (ProC := ProC) (X := X) (H := H) hNM hnm hij hmod_i hmod_j hcoeff
405 qmap_i qmap_j hqmap
406 (a.1 j)
408end Transition
410end
412end FoxDifferential