FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Coeff/System.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Projection
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Coeff/System.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]
28/-- The coefficient inverse system `i = (a, U) ↦ ZMod (ℓ^a)`. -/
30 InverseSystem (I := PrimePowerCompletedGroupAlgebraIndex G) where
31 X := fun i => ZMod (ℓ ^ i.1)
32 topologicalSpace := fun _ => ⊥
33 map := fun {i j} hij =>
34 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
35 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
36 modNCompletedCoeffMap (n := ℓ ^ i.1) (m := ℓ ^ j.1)
37 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
38 continuous_map := by
39 intro i j hij
40 letI : TopologicalSpace (ZMod (ℓ ^ i.1)) := ⊥
41 letI : TopologicalSpace (ZMod (ℓ ^ j.1)) := ⊥
42 letI : DiscreteTopology (ZMod (ℓ ^ j.1)) := ⟨rfl⟩
43 exact continuous_of_discreteTopology
44 map_id := by
45 intro i
46 funext x
47 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
48 exact congrFun
49 (congrArg DFunLike.coe
50 (modNCompletedCoeffMap_rfl (n := ℓ ^ i.1))) x
51 map_comp := by
52 intro i j k hij hjk
53 funext x
54 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
55 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
56 letI : Fact (0 < ℓ ^ k.1) := ⟨primePower_pos ℓ k.1⟩
57 exact congrFun
58 (congrArg DFunLike.coe
60 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (k := ℓ ^ k.1)
61 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
62 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) x
64/-- The inverse-limit object of the coefficient tower indexed by prime powers and quotients. -/
65abbrev PrimePowerCompletedCoeff :=
66 (primePowerCompletedCoeffSystem ℓ G).inverseLimit
68/-- The projection from the prime-power coefficient limit to one finite stage. -/
69abbrev primePowerCompletedCoeffProjection (i : PrimePowerCompletedGroupAlgebraIndex G) :
70 PrimePowerCompletedCoeff ℓ G →
71 ModNCompletedCoeff (ℓ ^ i.1) :=
72 (primePowerCompletedCoeffSystem ℓ G).projection i
74end
76end FoxDifferential