Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.System
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Projection
3/-!
4# Fox differential: coefficient rings — prime-power completed group algebra — coeff — system
6The principal declarations in this module are:
8- `primePowerCompletedCoeffSystem`
9 The coefficient inverse system over prime-power group-algebra indices; at index \((a, U)\), its
10 coefficient ring is \(\mathbb{Z}/\ell^a\mathbb{Z}\).
11- `PrimePowerCompletedCoeff`
12 The inverse-limit object of the coefficient tower indexed by prime powers and quotients.
13- `primePowerCompletedCoeffProjection`
14 The projection from the prime-power coefficient limit to one finite stage.
15-/
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]
29/--
30The coefficient inverse system over prime-power group-algebra indices; at index \((a, U)\), its
31coefficient ring is \(\mathbb{Z}/\ell^a\mathbb{Z}\).
32-/
33def primePowerCompletedCoeffSystem :
34 InverseSystem (I := PrimePowerCompletedGroupAlgebraIndex G) where
35 X := fun i => ZMod (ℓ ^ i.1)
36 topologicalSpace := fun _ => ⊥
37 map := fun {i j} hij =>
38 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
39 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
40 modNCompletedCoeffMap (n := ℓ ^ i.1) (m := ℓ ^ j.1)
41 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
42 continuous_map := by
43 intro i j hij
44 letI : TopologicalSpace (ZMod (ℓ ^ i.1)) := ⊥
45 letI : TopologicalSpace (ZMod (ℓ ^ j.1)) := ⊥
46 letI : DiscreteTopology (ZMod (ℓ ^ j.1)) := ⟨rfl⟩
47 exact continuous_of_discreteTopology
48 map_id := by
49 intro i
50 funext x
51 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
52 exact congrFun
53 (congrArg DFunLike.coe
54 (modNCompletedCoeffMap_rfl (n := ℓ ^ i.1))) x
55 map_comp := by
56 intro i j k hij hjk
57 funext x
58 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
59 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
60 letI : Fact (0 < ℓ ^ k.1) := ⟨primePower_pos ℓ k.1⟩
61 exact congrFun
62 (congrArg DFunLike.coe
63 (modNCompletedCoeffMap_comp
64 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (k := ℓ ^ k.1)
65 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
66 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) x
68/-- The inverse-limit object of the coefficient tower indexed by prime powers and quotients. -/
69abbrev PrimePowerCompletedCoeff :=
70 (primePowerCompletedCoeffSystem ℓ G).inverseLimit
72/-- The projection from the prime-power coefficient limit to one finite stage. -/
73abbrev primePowerCompletedCoeffProjection (i : PrimePowerCompletedGroupAlgebraIndex G) :
74 PrimePowerCompletedCoeff ℓ G →
75 ModNCompletedCoeff (ℓ ^ i.1) :=
76 (primePowerCompletedCoeffSystem ℓ G).projection i
78end
80end FoxDifferential