Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.LimitEquiv
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Module
3/-!
4# Fox differential: completed — coefficient rings — prime-power augmentation ideal — limit equiv
6The principal declarations in this module are:
8- `toPrimePowerCompletedGroupAlgebraAugmentationIdeal`
9 A prime-power augmentation-kernel point determines a compatible family in the finite-stage
10 augmentation ideals.
11- `ofPrimePowerCompletedGroupAlgebraAugmentationIdeal`
12 A compatible family of prime-power finite-stage augmentation-ideal elements determines a
13 prime-power augmentation-kernel point.
14- `primePowerCompletedGroupAlgebraAugmentationIdealProjection_zero`
15 The finite-stage augmentation-ideal projection is compatible with zero.
16- `primePowerCompletedGroupAlgebraAugmentationIdealProjection_add`
17 The finite-stage augmentation-ideal projection is compatible with addition.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.InverseSystems
26universe u
29variable (ℓ : ℕ) [Fact (0 < ℓ)]
30variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32omit [Fact (0 < ℓ)] in
33/-- The finite-stage augmentation-ideal projection is compatible with zero. -/
34theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_zero
35 (i : PrimePowerCompletedGroupAlgebraIndex G) :
36 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i
37 (0 : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) = 0 := by
38 rfl
40omit [Fact (0 < ℓ)] in
41/-- The finite-stage augmentation-ideal projection is compatible with addition. -/
42@[simp]
43theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_add
44 (i : PrimePowerCompletedGroupAlgebraIndex G)
45 (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
46 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (x + y) =
47 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x +
48 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i y := by
49 rfl
51omit [Fact (0 < ℓ)] in
52/-- The finite-stage augmentation-ideal projection is compatible with negation. -/
53@[simp]
54theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_neg
55 (i : PrimePowerCompletedGroupAlgebraIndex G)
56 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
57 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (-x) =
58 -primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x := by
59 rfl
61omit [Fact (0 < ℓ)] in
62/-- The finite-stage augmentation-ideal projection is compatible with subtraction. -/
63@[simp]
64theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_sub
65 (i : PrimePowerCompletedGroupAlgebraIndex G)
66 (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
67 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (x - y) =
68 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x -
69 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i y := by
70 rfl
72omit [Fact (0 < ℓ)] in
73/--
74The finite-stage augmentation-ideal projection is compatible with natural-number scalar
75multiplication.
76-/
77@[simp]
78theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_nsmul
79 (i : PrimePowerCompletedGroupAlgebraIndex G)
80 (m : ℕ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
81 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (m • x) =
82 m • primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x := by
83 rfl
85omit [Fact (0 < ℓ)] in
86/--
87The finite-stage augmentation-ideal projection is compatible with integer scalar multiplication.
88-/
89@[simp]
90theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_zsmul
91 (i : PrimePowerCompletedGroupAlgebraIndex G)
92 (m : ℤ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
93 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (m • x) =
94 m • primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x := by
95 rfl
97omit [Fact (0 < ℓ)] in
98/-- The finite-stage augmentation-ideal projection is compatible with scalar multiplication. -/
99@[simp]
100theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_smul
101 (i : PrimePowerCompletedGroupAlgebraIndex G)
102 (a : PrimePowerCompletedCoeff ℓ G)
103 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
104 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (a • x) =
105 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
106 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x := by
107 rfl
109/--
110A prime-power augmentation-kernel point determines a compatible family in the finite-stage
111augmentation ideals.
112-/
113def toPrimePowerCompletedGroupAlgebraAugmentationIdeal :
114 PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) →
115 PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G := by
116 intro x
117 refine ⟨fun i => ⟨primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1, ?_⟩, ?_⟩
118 · exact (mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff
119 (ℓ := ℓ) (G := G) (i := i)
120 (x := primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1)).2
121 ((mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff_forall
122 (ℓ := ℓ) (G := G) (x := x.1)).1 x.2 i)
123 · intro i j hij
124 apply Subtype.ext
125 exact (primePowerCompletedGroupAlgebraSystem ℓ G).projection_compatible x.1 i j hij
127omit [Fact (0 < ℓ)] in
128/--
129The projection-to-stage map is one direction of the completed augmentation-ideal stage
130equivalence.
131-/
132@[simp]
133theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_to
134 (x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G))
135 (i : PrimePowerCompletedGroupAlgebraIndex G) :
136 ((primePowerCompletedGroupAlgebraAugmentationIdealProjection
137 (ℓ := ℓ) (G := G) i
138 (toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x)) :
139 PrimePowerCompletedGroupAlgebraStage ℓ G i) =
140 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1 := rfl
142/--
143A compatible family of prime-power finite-stage augmentation-ideal elements determines a
144prime-power augmentation-kernel point.
145-/
146def ofPrimePowerCompletedGroupAlgebraAugmentationIdeal :
147 PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G →
148 PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) := by
149 intro x
150 let y : PrimePowerCompletedGroupAlgebra ℓ G := ⟨fun i => (x.1 i).1, by
151 intro i j hij
152 exact congrArg Subtype.val (x.2 i j hij)⟩
153 refine ⟨y, ?_⟩
154 exact (mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff_forall
155 (ℓ := ℓ) (G := G) (x := y)).2 (fun i =>
156 (mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff
157 (ℓ := ℓ) (G := G) (i := i) (x := (x.1 i).1)).1 (x.1 i).2)
159omit [Fact (0 < ℓ)] in
160/--
161Projecting an element of the completed augmentation ideal gives its corresponding finite-stage
162augmentation-ideal coordinate.
163-/
164@[simp]
165theorem primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal
166 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G)
167 (i : PrimePowerCompletedGroupAlgebraIndex G) :
168 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
169 (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
170 (ℓ := ℓ) (G := G) x).1 =
171 ((primePowerCompletedGroupAlgebraAugmentationIdealProjection
172 (ℓ := ℓ) (G := G) i x) :
173 PrimePowerCompletedGroupAlgebraStage ℓ G i) := rfl
175omit [Fact (0 < ℓ)] in
176/--
177The completion-to-stage map is one direction of the completed augmentation-ideal stage
178equivalence.
179-/
180@[simp]
181theorem ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to
182 (x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)) :
183 ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
184 (toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x) = x := by
185 apply Subtype.ext
186 apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
187 intro i
188 rfl
190omit [Fact (0 < ℓ)] in
191/--
192The stage-to-completion map is one direction of the completed augmentation-ideal stage
193equivalence.
194-/
195@[simp]
196theorem toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of
197 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
198 toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
199 (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x) = x := by
200 apply (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).ext
201 intro i
202 apply Subtype.ext
203 rfl
205/--
206The prime-power completed augmentation kernel is canonically equivalent to the inverse limit of
207the prime-power finite-stage augmentation ideals.
208-/
209def primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit :
210 PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) ≃
211 PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G where
212 toFun := toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
213 invFun := ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
214 left_inv := ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to (ℓ := ℓ) (G := G)
215 right_inv := toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of (ℓ := ℓ) (G := G)
217omit [Fact (0 < ℓ)] in
218/--
219The forward augmentation-kernel equivalence is the canonical map to the inverse-limit augmentation
220ideal.
221-/
222@[simp]
223theorem primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply
224 (x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)) :
225 primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit
226 (ℓ := ℓ) (G := G) x =
227 toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x := rfl
229omit [Fact (0 < ℓ)] in
230/--
231The inverse augmentation-kernel equivalence reconstructs a kernel element from an inverse-limit
232augmentation-ideal element.
233-/
234@[simp]
235theorem primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply
236 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
237 (primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit
238 (ℓ := ℓ) (G := G)).symm x =
239 ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x := rfl
241end
243end FoxDifferential