Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Module
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Additive
3/-!
4# Fox differential: completed — coefficient rings — prime-power augmentation ideal — module
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraStageAugmentationIdealTransition_smul`
9 The transition map between finite-stage augmentation ideals is compatible with scalar
10 multiplication.
11- `coe_smul_primePowerCompletedGroupAlgebraAugmentationIdeal`
12 The inclusion of the completed augmentation ideal preserves scalar multiplication.
13- `instSMulPrimePowerCompletedCoeffPrimePowerCompletedGAAugmentationIdealFamily`
14 The family-level prime-power completed group-algebra augmentation ideal carries scalar
15 multiplication by the prime-power completed coefficient ring.
16- `instModulePpCoeffPpGAAugIdealFamily`
17 The prime-power completed augmentation-ideal family is a module over the completed coefficient
18 ring.
19-/
21namespace FoxDifferential
23noncomputable section
25open ProCGroups.InverseSystems
27universe u
30variable (ℓ : ℕ) [Fact (0 < ℓ)]
31variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
34attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
36@[reducible] private def addCommGroupAugmentationIdealStage
37 (i : PrimePowerCompletedGroupAlgebraIndex G) :
38 AddCommGroup ((primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) := by
39 dsimp [primePowerCompletedGroupAlgebraAugmentationIdealSystem]
40 infer_instance
42attribute [local instance] addCommGroupAugmentationIdealStage
44@[reducible] private def addCommGroupAugmentationIdealFamily :
45 AddCommGroup
46 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
47 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) :=
48 inferInstance
50attribute [local instance] addCommGroupAugmentationIdealFamily
52omit [Fact (0 < ℓ)] in
53/--
54The transition map between finite-stage augmentation ideals is compatible with scalar
55multiplication.
56-/
57@[simp 900]
58theorem primePowerCompletedGroupAlgebraStageAugmentationIdealTransition_smul
59 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
60 (a : ZMod (ℓ ^ j.1))
61 (x : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) :
62 primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
63 (ℓ := ℓ) (G := G) hij (a • x) =
64 (modNCompletedCoeffMap
65 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
66 (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) •
67 primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
68 (ℓ := ℓ) (G := G) hij x := by
69 apply Subtype.ext
70 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
71 ((a • x : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) :
72 PrimePowerCompletedGroupAlgebraStage ℓ G j) =
73 (((modNCompletedCoeffMap
74 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
75 (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) •
76 primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
77 (ℓ := ℓ) (G := G) hij x :
78 primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i) :
79 PrimePowerCompletedGroupAlgebraStage ℓ G i)
80 simpa using
81 primePowerCompletedGroupAlgebraTransition_smul
82 (ℓ := ℓ) (G := G) hij a
83 ((x : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) :
84 PrimePowerCompletedGroupAlgebraStage ℓ G j)
86/--
87The family-level prime-power completed group-algebra augmentation ideal carries scalar
88multiplication by the prime-power completed coefficient ring.
89-/
90instance instSMulPrimePowerCompletedCoeffPrimePowerCompletedGAAugmentationIdealFamily :
91 SMul (PrimePowerCompletedCoeff ℓ G)
92 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
93 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) where
94 smul a x := fun i =>
95 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
96 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x i)
98/--
99The prime-power completed augmentation-ideal family is a module over the completed coefficient
100ring.
101-/
102instance instModulePpCoeffPpGAAugIdealFamily :
103 Module (PrimePowerCompletedCoeff ℓ G)
104 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
105 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) where
106 one_smul x := by
107 funext i
108 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
109 (1 : PrimePowerCompletedCoeff ℓ G)) •
110 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
111 (ℓ := ℓ) (G := G) i from x i) =
112 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
113 (ℓ := ℓ) (G := G) i from x i)
114 rw [primePowerCompletedCoeffProjection_one, one_smul]
115 mul_smul a b x := by
116 funext i
117 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a * b)) •
118 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
119 (ℓ := ℓ) (G := G) i from x i) =
120 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
121 ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
122 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
123 (ℓ := ℓ) (G := G) i from x i))
124 rw [primePowerCompletedCoeffProjection_mul, mul_smul]
125 smul_zero a := by
126 funext i
127 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
128 (0 : primePowerCompletedGroupAlgebraStageAugmentationIdeal
129 (ℓ := ℓ) (G := G) i) = 0
130 rw [smul_zero]
131 smul_add a x y := by
132 funext i
133 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
134 ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal
135 (ℓ := ℓ) (G := G) i from x i) +
136 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
137 (ℓ := ℓ) (G := G) i from y i)) =
138 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
139 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
140 (ℓ := ℓ) (G := G) i from x i) +
141 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
142 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
143 (ℓ := ℓ) (G := G) i from y i)
144 rw [smul_add]
145 add_smul a b x := by
146 funext i
147 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a + b)) •
148 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
149 (ℓ := ℓ) (G := G) i from x i) =
150 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
151 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
152 (ℓ := ℓ) (G := G) i from x i) +
153 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
154 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
155 (ℓ := ℓ) (G := G) i from x i)
156 rw [primePowerCompletedCoeffProjection_add, add_smul]
157 zero_smul x := by
158 funext i
159 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
160 (0 : PrimePowerCompletedCoeff ℓ G)) •
161 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
162 (ℓ := ℓ) (G := G) i from x i) = 0
163 rw [primePowerCompletedCoeffProjection_zero, zero_smul]
165/--
166The prime-power completed group-algebra augmentation ideal carries scalar multiplication by the
167prime-power completed coefficient ring.
168-/
169instance instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraAugmentationIdeal :
170 SMul (PrimePowerCompletedCoeff ℓ G)
171 (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
172 smul a x := ⟨fun i =>
173 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
174 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
175 (ℓ := ℓ) (G := G) i from x.1 i), by
176 intro i j hij
177 calc
178 primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
179 (ℓ := ℓ) (G := G) hij
180 ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a) •
181 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
182 from x.1 j)) =
183 (modNCompletedCoeffMap
184 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
185 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
186 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)) •
187 primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
188 (ℓ := ℓ) (G := G) hij
189 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
190 from x.1 j) := by
191 exact
192 primePowerCompletedGroupAlgebraStageAugmentationIdealTransition_smul
193 (ℓ := ℓ) (G := G) hij
194 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)
195 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
196 (ℓ := ℓ) (G := G) j from x.1 j)
197 _ =
198 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
199 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
200 (ℓ := ℓ) (G := G) i from x.1 i) := by
201 exact congrArg₂ HSMul.hSMul (a.2 i j hij) (x.2 i j hij)⟩
203omit [Fact (0 < ℓ)] in
204/-- The inclusion of the completed augmentation ideal preserves scalar multiplication. -/
205@[simp]
206theorem coe_smul_primePowerCompletedGroupAlgebraAugmentationIdeal
207 (a : PrimePowerCompletedCoeff ℓ G)
208 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
209 letI := instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraAugmentationIdeal
210 (ℓ := ℓ) (G := G)
211 ((a • x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
212 (i : PrimePowerCompletedGroupAlgebraIndex G) →
213 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) =
214 a • (x :
215 (i : PrimePowerCompletedGroupAlgebraIndex G) →
216 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) := by
217 funext i
218 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
219 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) =
220 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
221 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i)
222 rfl
224/-- The prime-power completed augmentation ideal is a module over the completed coefficient ring. -/
225instance instModulePpCoeffPpGAAugIdeal :
226 Module (PrimePowerCompletedCoeff ℓ G)
227 (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :=
228 Function.Injective.module (PrimePowerCompletedCoeff ℓ G)
229 { toFun := Subtype.val
230 map_zero' := rfl
231 map_add' := fun _ _ => rfl }
232 Subtype.val_injective
233 (coe_smul_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
236end
238end FoxDifferential