Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module
3/-!
4# Fox differential: completed — coefficient rings — prime-power completed group algebra — augmentation
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraAugmentation`
9 The prime-power completed group algebra carries a canonical augmentation to the corresponding
10 coefficient inverse limit.
11- `primePowerCompletedCoeffProjection_augmentation`
12 Projecting the prime-power completed augmentation to a coefficient stage agrees with the
13 corresponding finite-stage augmentation.
14- `primePowerCompletedGroupAlgebraStageAugmentation_eq_of_same_exponent`
15 Stagewise augmentations of a completed group-algebra element are independent of the
16 finite-quotient component once the prime-power exponent is fixed.
17-/
19namespace FoxDifferential
21noncomputable section
23open ProCGroups.InverseSystems
24open ProCGroups.ProC
26universe u
28variable (ℓ : ℕ) [Fact (0 < ℓ)]
29variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31/--
32The prime-power completed group algebra carries a canonical augmentation to the corresponding
33coefficient inverse limit.
34-/
35def primePowerCompletedGroupAlgebraAugmentation :
36 PrimePowerCompletedGroupAlgebra ℓ G → PrimePowerCompletedCoeff ℓ G := by
37 intro x
38 refine ⟨fun i => ?_, ?_⟩
39 · letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
40 exact modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2 (x.1 i)
41 · intro i j hij
42 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
43 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
44 calc
45 modNCompletedCoeffMap
46 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
47 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
48 (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ j.1) G j.2 (x.1 j))
49 =
50 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
51 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij (x.1 j)) := by
52 symm
53 exact congrFun
54 (congrArg DFunLike.coe
55 (primePowerCompletedGroupAlgebraStageAugmentation_comp_transition
56 (ℓ := ℓ) (G := G) hij)) (x.1 j)
57 _ =
58 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2 (x.1 i) := by
59 have hx :
60 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij (x.1 j) = x.1 i :=
61 x.2 i j hij
62 exact congrArg (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2) hx
64omit [Fact (0 < ℓ)] in
65/--
66Projecting the prime-power completed augmentation to a coefficient stage agrees with the
67corresponding finite-stage augmentation.
68-/
69@[simp]
70theorem primePowerCompletedCoeffProjection_augmentation
71 (i : PrimePowerCompletedGroupAlgebraIndex G)
72 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
73 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
74 (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x) =
75 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
76 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x) := rfl
78omit [Fact (0 < ℓ)] in
79/--
80Stagewise augmentations of a completed group-algebra element are independent of the
81finite-quotient component once the prime-power exponent is fixed.
82-/
83theorem primePowerCompletedGroupAlgebraStageAugmentation_eq_of_same_exponent
84 (a : ℕ) (U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
85 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
86 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ a) G U
87 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) (a, U) x) =
88 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ a) G V
89 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) (a, V) x) := by
90 change
91 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, U)
92 (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x) =
93 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, V)
94 (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x)
95 exact primePowerCompletedCoeffProjection_eq_of_same_exponent
96 (ℓ := ℓ) (G := G) a U V
97 (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x)
99end
101end FoxDifferential