Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.AugmentationIdeal
2import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.AllFinite
4/-!
5# Fox differential: coefficient rings — prime-power completed group algebra — basic — augmentation
7The principal declarations in this module are:
9- `modNCompletedGroupAlgebraCoeffMap`
10 The modulus-direction map on residue-coefficient completed group algebras.
11- `modNCompletedGroupAlgebraAugmentationKernelCoeffMap`
12 Coefficient change is performed stagewise: supports are unchanged and coefficients are transported
13 by the given ring homomorphism.
14- `modNCompletedGroupAlgebraProjection_coeffMap`
15 The mod-\(n\) completed group-algebra projection commutes with the coefficient map.
16- `modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap`
17 Finite-stage augmentation commutes with coefficient reduction.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.InverseSystems
25open ProCGroups.ProC
27universe u
30variable {n m k : ℕ}
31variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
32variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
34/-- The modulus-direction map on residue-coefficient completed group algebras. -/
35def modNCompletedGroupAlgebraCoeffMap (hnm : n ∣ m) :
36 ModNCompletedGroupAlgebra m G → ModNCompletedGroupAlgebra n G := by
37 intro x
38 refine ⟨fun U =>
39 modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm (x.1 U), ?_⟩
40 intro U V hUV
41 calc
42 modNCompletedGroupAlgebraTransition n G hUV
43 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) V hnm (x.1 V))
44 =
45 modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm
46 (modNCompletedGroupAlgebraTransition m G hUV (x.1 V)) := by
47 symm
48 exact congrFun
49 (congrArg DFunLike.coe
50 (modNCompletedGroupAlgebraStageCoeffMap_compatible
51 (n := n) (m := m) (G := G) hUV hnm)) (x.1 V)
52 _ =
53 modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm (x.1 U) := by
54 exact congrArg
55 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm)
56 (x.2 U V hUV)
58omit [Fact (0 < n)] [Fact (0 < m)] in
59/-- The mod-\(n\) completed group-algebra projection commutes with the coefficient map. -/
60@[simp]
61theorem modNCompletedGroupAlgebraProjection_coeffMap
62 (hnm : n ∣ m) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
63 (x : ModNCompletedGroupAlgebra m G) :
64 modNCompletedGroupAlgebraProjection n G U
65 (modNCompletedGroupAlgebraCoeffMap (n := n) (m := m) (G := G) hnm x) =
66 modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm
67 (modNCompletedGroupAlgebraProjection m G U x) := by
68 unfold modNCompletedGroupAlgebraProjection modNCompletedGroupAlgebraCoeffMap
69 rfl
71omit [Fact (0 < n)] [Fact (0 < m)] in
72/-- Finite-stage augmentation commutes with coefficient reduction. -/
73@[simp 900]
74theorem modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap
75 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (hnm : n ∣ m) :
76 (modNCompletedGroupAlgebraStageAugmentation n G U).comp
77 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm) =
78 (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
79 (modNCompletedGroupAlgebraStageAugmentation m G U) := by
80 apply RingHom.ext
81 intro x
82 refine MonoidAlgebra.induction_on
83 (p := fun x =>
84 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
85 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm)) x =
86 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp
87 (modNCompletedGroupAlgebraStageAugmentation m G U)) x)
88 x ?_ ?_ ?_
89 · intro q
90 rw [RingHom.comp_apply, RingHom.comp_apply, modNCompletedGroupAlgebraStageCoeffMap_of,
91 modNCompletedGroupAlgebraStageAugmentation_of,
92 modNCompletedGroupAlgebraStageAugmentation_of]
93 simpa [modNCompletedCoeffMap] using
94 (map_one (modNCompletedCoeffMap (n := n) (m := m) hnm)).symm
95 · intro x y hx hy
96 simp only [RingHom.map_add, hx, RingHom.coe_comp, Function.comp_apply, hy]
97 · intro a x hx
98 letI : Algebra (ModNCompletedCoeff m) (ModNCompletedCoeff n) :=
99 ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := m) hnm
100 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
101 have hcoeff :
102 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
103 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm))
104 (algebraMap (ModNCompletedCoeff m) (ModNCompletedGroupAlgebraStage m G U) a) =
105 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp
106 (modNCompletedGroupAlgebraStageAugmentation m G U))
107 (algebraMap (ModNCompletedCoeff m) (ModNCompletedGroupAlgebraStage m G U) a) := by
108 have hleft :
109 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp
110 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm))
111 (algebraMap (ModNCompletedCoeff m) (ModNCompletedGroupAlgebraStage m G U) a) =
112 algebraMap (ModNCompletedCoeff m) (ModNCompletedCoeff n) a := by
113 simp only [modNCompletedGroupAlgebraStageAugmentation,
114 modNCompletedGroupAlgebraStageCoeffMap,
115 modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, MonoidAlgebra.coe_algebraMap,
116 Algebra.algebraMap_self,
117 RingHom.coe_id, Function.comp_apply, id_eq, RingHom.comp_apply, RingHom.coe_coe,
118 MonoidAlgebra.lift_single,
119 MonoidAlgebra.of_apply, Algebra.smul_def, MonoidAlgebra.single_mul_single, mul_one,
120 MonoidHom.one_apply]
121 have hright :
122 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp
123 (modNCompletedGroupAlgebraStageAugmentation m G U))
124 (algebraMap (ModNCompletedCoeff m) (ModNCompletedGroupAlgebraStage m G U) a) =
125 algebraMap (ModNCompletedCoeff m) (ModNCompletedCoeff n) a := by
126 simp only [modNCompletedGroupAlgebraStageAugmentation, MonoidAlgebra.coe_algebraMap,
127 Algebra.algebraMap_self,
128 RingHom.coe_id, Function.comp_apply, id_eq, RingHom.comp_apply, RingHom.coe_coe,
129 MonoidAlgebra.lift_single,
130 MonoidHom.one_apply, smul_eq_mul, mul_one]
131 rfl
132 exact hleft.trans hright.symm
133 rw [hcoeff]
135omit [Fact (0 < n)] [Fact (0 < m)] in
136/-- Class-indexed finite-stage augmentation commutes with coefficient reduction. -/
137@[simp 900]
138theorem modNCompletedGroupAlgebraStageAugmentationInClass_comp_coeffMap
139 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (hnm : n ∣
140 m) :
141 (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
142 (modNCompletedGroupAlgebraStageCoeffMapInClass
143 (n := n) (m := m) (G := G) C U hnm) =
144 (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
145 (modNCompletedGroupAlgebraStageAugmentationInClass m G C U) := by
146 apply RingHom.ext
147 intro x
148 refine MonoidAlgebra.induction_on
149 (p := fun x =>
150 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
151 (modNCompletedGroupAlgebraStageCoeffMapInClass
152 (n := n) (m := m) (G := G) C U hnm)) x =
153 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp
154 (modNCompletedGroupAlgebraStageAugmentationInClass m G C U)) x)
155 x ?_ ?_ ?_
156 · intro q
157 rw [RingHom.comp_apply, RingHom.comp_apply, modNCompletedGroupAlgebraStageCoeffMapInClass_of,
158 modNCompletedGroupAlgebraStageAugmentationInClass_of,
159 modNCompletedGroupAlgebraStageAugmentationInClass_of]
160 simpa [modNCompletedCoeffMap] using
161 (map_one (modNCompletedCoeffMap (n := n) (m := m) hnm)).symm
162 · intro x y hx hy
163 simp only [RingHom.map_add, hx, RingHom.coe_comp, Function.comp_apply, hy]
164 · intro a x hx
165 letI : Algebra (ModNCompletedCoeff m) (ModNCompletedCoeff n) :=
166 ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := m) hnm
167 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
168 have hcoeff :
169 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
170 (modNCompletedGroupAlgebraStageCoeffMapInClass
171 (n := n) (m := m) (G := G) C U hnm))
172 (algebraMap (ModNCompletedCoeff m)
173 (ModNCompletedGroupAlgebraStageInClass m G C U) a) =
174 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp
175 (modNCompletedGroupAlgebraStageAugmentationInClass m G C U))
176 (algebraMap (ModNCompletedCoeff m)
177 (ModNCompletedGroupAlgebraStageInClass m G C U) a) := by
178 have hleft :
179 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
180 (modNCompletedGroupAlgebraStageCoeffMapInClass
181 (n := n) (m := m) (G := G) C U hnm))
182 (algebraMap (ModNCompletedCoeff m)
183 (ModNCompletedGroupAlgebraStageInClass m G C U) a) =
184 algebraMap (ModNCompletedCoeff m) (ModNCompletedCoeff n) a := by
185 simp only [modNCompletedGroupAlgebraStageAugmentationInClass,
186 modNCompletedGroupAlgebraStageCoeffMapInClass,
187 modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, MonoidAlgebra.coe_algebraMap,
188 Algebra.algebraMap_self,
189 RingHom.coe_id, Function.comp_apply, id_eq, RingHom.comp_apply, RingHom.coe_coe,
190 MonoidAlgebra.lift_single,
191 MonoidAlgebra.of_apply, Algebra.smul_def, MonoidAlgebra.single_mul_single, mul_one,
192 MonoidHom.one_apply]
193 have hright :
194 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp
195 (modNCompletedGroupAlgebraStageAugmentationInClass m G C U))
196 (algebraMap (ModNCompletedCoeff m)
197 (ModNCompletedGroupAlgebraStageInClass m G C U) a) =
198 algebraMap (ModNCompletedCoeff m) (ModNCompletedCoeff n) a := by
199 simp only [modNCompletedGroupAlgebraStageAugmentationInClass, MonoidAlgebra.coe_algebraMap,
200 Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq, RingHom.comp_apply,
201 RingHom.coe_coe,
202 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]
203 rfl
204 exact hleft.trans hright.symm
205 rw [hcoeff]
207omit [Fact (0 < n)] [Fact (0 < m)] in
208/-- Completed augmentation commutes with the coefficient-reduction map between moduli. -/
209@[simp]
210theorem modNCompletedGroupAlgebraAugmentation_coeffMap
211 (hnm : n ∣ m) (x : ModNCompletedGroupAlgebra m G) :
212 modNCompletedGroupAlgebraAugmentation n G
213 (modNCompletedGroupAlgebraCoeffMap (n := n) (m := m) (G := G) hnm x) =
214 modNCompletedCoeffMap (n := n) (m := m) hnm
215 (modNCompletedGroupAlgebraAugmentation m G x) := by
216 unfold modNCompletedGroupAlgebraAugmentation modNCompletedGroupAlgebraAugmentationAt
217 rw [modNCompletedGroupAlgebraProjection_coeffMap]
218 exact congrFun
219 (congrArg DFunLike.coe
220 (modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap
221 (n := n) (m := m) (G := G)
222 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) hnm))
223 (modNCompletedGroupAlgebraProjection m G
224 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) x)
226/--
227Coefficient change is performed stagewise: supports are unchanged and coefficients are
228transported by the given ring homomorphism.
229-/
230def modNCompletedGroupAlgebraAugmentationKernelCoeffMap
231 (hnm : n ∣ m) :
232 ModNCompletedGroupAlgebraAugmentationKernel m G →
233 ModNCompletedGroupAlgebraAugmentationKernel n G := by
234 intro x
235 refine ⟨modNCompletedGroupAlgebraCoeffMap (n := n) (m := m) (G := G) hnm x.1, ?_⟩
236 rw [mem_modNCompletedGroupAlgebraAugmentationKernel_iff,
237 modNCompletedGroupAlgebraAugmentation_coeffMap]
238 simpa [map_zero, modNCompletedCoeffMap] using
239 congrArg (modNCompletedCoeffMap (n := n) (m := m) hnm) x.2
241/-- The standard divisibility relation between prime powers with the same base. -/
242theorem primePow_dvd_primePow
243 (ℓ : ℕ) {a b : ℕ} (hab : a ≤ b) :
244 ℓ ^ a ∣ ℓ ^ b := by
245 exact Nat.pow_dvd_pow ℓ hab
247/-- The modulus-direction completed map specialized to prime-power stages. -/
248def primePowCompletedGroupAlgebraCoeffMap
249 (ℓ : ℕ) {a b : ℕ}
250 (hab : a ≤ b) :
251 ModNCompletedGroupAlgebra (ℓ ^ b) G → ModNCompletedGroupAlgebra (ℓ ^ a) G :=
252 modNCompletedGroupAlgebraCoeffMap (n := ℓ ^ a) (m := ℓ ^ b) (G := G)
253 (primePow_dvd_primePow (ℓ := ℓ) hab)
255/-- The coefficient map between prime-power stages restricts to a map on augmentation kernels. -/
256def primePowCompletedGroupAlgebraAugmentationKernelCoeffMap
257 (ℓ : ℕ) {a b : ℕ}
258 (hab : a ≤ b) :
259 ModNCompletedGroupAlgebraAugmentationKernel (ℓ ^ b) G →
260 ModNCompletedGroupAlgebraAugmentationKernel (ℓ ^ a) G :=
261 modNCompletedGroupAlgebraAugmentationKernelCoeffMap
262 (n := ℓ ^ a) (m := ℓ ^ b) (G := G)
263 (primePow_dvd_primePow (ℓ := ℓ) hab)
266variable (ℓ : ℕ) [Fact (0 < ℓ)]
267variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
269/-- The two-parameter index \((a,U)\) for the prime-power residue-coefficient stages. -/
270abbrev PrimePowerCompletedGroupAlgebraIndex :=
271 ℕ × _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G
273/-- The two-parameter index \((a,U)\) for prime-power stages over a quotient class \(C\). -/
274abbrev PrimePowerCompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{u}) :=
275 ℕ × CompletedGroupAlgebraIndexInClass G C
276end
278end FoxDifferential