Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Kernel
ProCGroups/FoxDifferential/Completed/ProCIntegerCoefficients/AugmentationIdeal/Kernel/Source

Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Kernel

1import ProCGroups.FoxDifferential.Completed.Continuous.Naturality
2import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Closure
3import ProCGroups.ProC.Kernels
5/-!
6# Fox differential: completed — \(\mathbb{Z}_C\) coefficients — augmentation ideal — kernel
8The principal declarations in this module are:
10- `groupAlgebraMapDomainKernelAugmentationIdeal`
11 The ideal in \(R[A]\) generated by \([k]-1\) for \(k \in \ker f\).
12- `groupAlgebraMapDomainTargetSection`
13 A chosen linear section of the group-algebra map induced by a surjective group homomorphism.
14- `groupAlgebraMapDomainKernelAugmentationGenerator_mem`
15 A kernel augmentation generator lies in the group-algebra kernel-augmentation ideal.
16- `groupAlgebra_mapDomainRingHom_smul`
17 The domain group-algebra map is compatible with scalar multiplication.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.ProC
25open ProCGroups.Completion
26open ProCGroups.InverseSystems
28universe u v w
30section GroupAlgebraMapKernel
32variable {R : Type v} {A : Type u} {B : Type w} [CommRing R] [Group A] [Group B]
34/-- The ideal in \(R[A]\) generated by \([k]-1\) for \(k \in \ker f\). -/
35def groupAlgebraMapDomainKernelAugmentationIdeal (f : A →* B) :
36 Ideal (MonoidAlgebra R A) :=
37 Ideal.span (Set.range fun k : f.ker => MonoidAlgebra.of R A k.1 - 1)
39/-- A kernel augmentation generator lies in the group-algebra kernel-augmentation ideal. -/
40theorem groupAlgebraMapDomainKernelAugmentationGenerator_mem
41 (f : A →* B) (k : f.ker) :
42 MonoidAlgebra.of R A k.1 - 1 ∈
43 groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f :=
44 Ideal.subset_span (Set.mem_range_self k)
46/-- The domain group-algebra map is compatible with scalar multiplication. -/
47theorem groupAlgebra_mapDomainRingHom_smul
48 (f : A →* B) (r : R) (x : MonoidAlgebra R A) :
49 MonoidAlgebra.mapDomainRingHom R f (r • x) =
50 r • MonoidAlgebra.mapDomainRingHom R f x := by
51 rw [Algebra.smul_def, Algebra.smul_def, RingHom.map_mul]
52 simp only [MonoidAlgebra.mapDomainRingHom_apply,
53 MonoidAlgebra.mapDomain_algebraMap]
55/-- A chosen linear section of the group-algebra map induced by a surjective group homomorphism. -/
56def groupAlgebraMapDomainTargetSection
57 (f : A →* B) (hf : Function.Surjective f) :
58 MonoidAlgebra R B →ₗ[R] MonoidAlgebra R A :=
59 (Finsupp.linearCombination R
60 (fun b : B => MonoidAlgebra.of R A (Function.surjInv hf b))).comp
61 (MonoidAlgebra.coeffLinearEquiv R).toLinearMap
63/--
64The domain-target section sends a group element to the corresponding group-algebra basis
65element.
66-/
67@[simp]
68theorem groupAlgebraMapDomainTargetSection_of
69 (f : A →* B) (hf : Function.Surjective f) (b : B) :
70 groupAlgebraMapDomainTargetSection (R := R) f hf
71 (MonoidAlgebra.of R B b) =
72 MonoidAlgebra.of R A (Function.surjInv hf b) := by
73 change
74 Finsupp.linearCombination R
75 (fun b : B => MonoidAlgebra.of R A (Function.surjInv hf b))
76 (MonoidAlgebra.of R B b).coeff =
77 MonoidAlgebra.of R A (Function.surjInv hf b)
78 rw [MonoidAlgebra.of_apply, MonoidAlgebra.coeff_single,
79 Finsupp.linearCombination_single, one_smul]
81/-- The chosen group-algebra section is a right inverse to the map induced by \(f\). -/
82theorem groupAlgebraMapDomain_targetSection
83 (f : A →* B) (hf : Function.Surjective f) (y : MonoidAlgebra R B) :
84 MonoidAlgebra.mapDomainRingHom R f
85 (groupAlgebraMapDomainTargetSection (R := R) f hf y) = y := by
86 classical
87 refine MonoidAlgebra.induction_on
88 (p := fun y : MonoidAlgebra R B =>
89 MonoidAlgebra.mapDomainRingHom R f
90 (groupAlgebraMapDomainTargetSection (R := R) f hf y) = y)
91 y ?single ?add ?smul
92 · intro b
93 rw [groupAlgebraMapDomainTargetSection_of]
94 rw [show MonoidAlgebra.mapDomainRingHom R f
95 (MonoidAlgebra.of R A (Function.surjInv hf b)) =
96 MonoidAlgebra.of R B (f (Function.surjInv hf b)) by
97 simp only [MonoidAlgebra.mapDomainRingHom_apply,
98 MonoidAlgebra.of_apply, MonoidAlgebra.mapDomain_single]]
99 exact congrArg (MonoidAlgebra.of R B) (Function.surjInv_eq hf b)
100 · intro x y hx hy
101 rw [map_add, map_add, hx, hy]
102 · intro a y hy
103 rw [show groupAlgebraMapDomainTargetSection (R := R) f hf (a • y) =
104 a • groupAlgebraMapDomainTargetSection (R := R) f hf y by
105 exact (groupAlgebraMapDomainTargetSection (R := R) f hf).map_smul a y]
106 rw [groupAlgebra_mapDomainRingHom_smul, hy]
108/--
109A source basis element minus the chosen lift of its target image lies in the kernel augmentation
110ideal.
111-/
112theorem groupAlgebraMapDomain_sourceBasis_sub_targetSection_mem_kernelAugmentationIdeal
113 (f : A →* B) (hf : Function.Surjective f) (a : A) :
114 MonoidAlgebra.of R A a -
115 groupAlgebraMapDomainTargetSection (R := R) f hf
116 (MonoidAlgebra.mapDomainRingHom R f (MonoidAlgebra.of R A a)) ∈
117 groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f := by
118 let t : B := f a
119 let lift : A := Function.surjInv hf t
120 let q : f.ker :=
121 ⟨lift⁻¹ * a, by
122 change f (lift⁻¹ * a) = 1
123 rw [map_mul, map_inv]
124 have hlift : f lift = t := Function.surjInv_eq hf t
125 rw [hlift]
126 simp only [inv_mul_cancel, t]⟩
127 have hsection :
128 groupAlgebraMapDomainTargetSection (R := R) f hf
129 (MonoidAlgebra.mapDomainRingHom R f (MonoidAlgebra.of R A a)) =
130 MonoidAlgebra.of R A lift := by
131 rw [show MonoidAlgebra.mapDomainRingHom R f (MonoidAlgebra.of R A a) =
132 MonoidAlgebra.of R B (f a) by
133 simp only [MonoidAlgebra.mapDomainRingHom_apply,
134 MonoidAlgebra.of_apply, MonoidAlgebra.mapDomain_single]]
135 simpa only [t, lift] using
136 groupAlgebraMapDomainTargetSection_of (R := R) f hf (f a)
137 rw [hsection]
138 have hmul :
139 MonoidAlgebra.of R A lift *
140 (MonoidAlgebra.of R A q.1 - 1) =
141 MonoidAlgebra.of R A a - MonoidAlgebra.of R A lift := by
142 simp only [MonoidAlgebra.of_apply]
143 rw [mul_sub, MonoidAlgebra.single_mul_single, mul_one]
144 simp only [mul_inv_cancel_left, mul_one, q]
145 rw [← hmul]
146 exact
147 (groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f).mul_mem_left _
148 (groupAlgebraMapDomainKernelAugmentationGenerator_mem (R := R) f q)
150/--
151Every group-algebra element differs from the chosen lift of its target image by an element of
152the kernel augmentation ideal.
153-/
154theorem groupAlgebraMapDomain_sub_targetSection_map_mem_kernelAugmentationIdeal
155 (f : A →* B) (hf : Function.Surjective f) (x : MonoidAlgebra R A) :
156 x - groupAlgebraMapDomainTargetSection (R := R) f hf
157 (MonoidAlgebra.mapDomainRingHom R f x) ∈
158 groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f := by
159 classical
160 refine MonoidAlgebra.induction_on
161 (p := fun x : MonoidAlgebra R A =>
162 x - groupAlgebraMapDomainTargetSection (R := R) f hf
163 (MonoidAlgebra.mapDomainRingHom R f x) ∈
164 groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f)
165 x ?single ?add ?smul
166 · intro a
167 exact
168 groupAlgebraMapDomain_sourceBasis_sub_targetSection_mem_kernelAugmentationIdeal
169 (R := R) f hf a
170 · intro x y hx hy
171 have hcalc :
172 x + y - groupAlgebraMapDomainTargetSection (R := R) f hf
173 (MonoidAlgebra.mapDomainRingHom R f (x + y)) =
174 (x - groupAlgebraMapDomainTargetSection (R := R) f hf
175 (MonoidAlgebra.mapDomainRingHom R f x)) +
176 (y - groupAlgebraMapDomainTargetSection (R := R) f hf
177 (MonoidAlgebra.mapDomainRingHom R f y)) := by
178 rw [map_add, map_add]
179 abel
180 rw [hcalc]
181 exact (groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f).add_mem hx hy
182 · intro r x hx
183 have hcalc :
184 r • x - groupAlgebraMapDomainTargetSection (R := R) f hf
185 (MonoidAlgebra.mapDomainRingHom R f (r • x)) =
186 r • (x - groupAlgebraMapDomainTargetSection (R := R) f hf
187 (MonoidAlgebra.mapDomainRingHom R f x)) := by
188 rw [groupAlgebra_mapDomainRingHom_smul, map_smul, smul_sub]
189 rw [hcalc]
190 rw [Algebra.smul_def]
191 exact (groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f).mul_mem_left _ hx
193/--
194For a surjective group map, the kernel of R[A] \(\to\) R[B] is generated by the augmentation
195generators attached to kernel f.
196-/
197theorem groupAlgebraMapDomainRingHom_ker_eq_kernelAugmentationIdeal_of_surjective
198 (f : A →* B) (hf : Function.Surjective f) :
199 RingHom.ker (MonoidAlgebra.mapDomainRingHom R f) =
200 groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f := by
201 apply le_antisymm
202 · intro x hx
203 have hxmap : MonoidAlgebra.mapDomainRingHom R f x = 0 :=
204 (RingHom.mem_ker).1 hx
205 have hdiff :=
206 groupAlgebraMapDomain_sub_targetSection_map_mem_kernelAugmentationIdeal
207 (R := R) f hf x
208 rw [hxmap, map_zero, sub_zero] at hdiff
209 exact hdiff
210 · refine Ideal.span_le.2 ?_
211 rintro _ ⟨k, rfl⟩
212 change MonoidAlgebra.mapDomainRingHom R f
213 (MonoidAlgebra.of R A k.1 - 1) = 0
214 rw [map_sub, map_one]
215 have hk : f k.1 = 1 := MonoidHom.mem_ker.mp k.2
216 simp only [MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.of_apply,
217 MonoidAlgebra.mapDomain_single, hk, MonoidAlgebra.one_def, sub_self]
219end GroupAlgebraMapKernel
221section KernelAugmentationIdeal
223variable (C : ProCGroups.FiniteGroupClass.{u})
225variable {G H : Type u}
226variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
227variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
229/--
230The algebraic ideal in \(\mathbb{Z}_C\llbracket G\rrbracket\) generated by completed
231augmentation generators coming from the kernel of \(\psi\).
232-/
233def zcCompletedGroupAlgebraKernelAugmentationIdealMul
234 (psi : ContinuousMonoidHom G H) :
235 Ideal (ZCCompletedGroupAlgebra C G) :=
236 Ideal.span
237 (Set.range fun n : ProfiniteKernelSubgroup psi =>
238 zcGroupLike C G n.1 - 1)
240omit [IsTopologicalGroup H] in
241/-- A kernel augmentation generator lies in the algebraic kernel-augmentation ideal. -/
242theorem zcGroupLike_sub_one_mem_kernelAugmentationIdealMul
243 (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi) :
244 zcGroupLike C G n.1 - 1 ∈
245 zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :=
246 Ideal.subset_span (Set.mem_range_self n)
248omit [IsTopologicalGroup H] in
249/-- The kernel-augmentation ideal is contained in the standard source augmentation ideal. -/
250theorem zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_standardAugmentationIdeal
251 (psi : ContinuousMonoidHom G H) :
252 zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi ≤
253 zcCompletedGroupAlgebraStandardAugmentationIdeal C G := by
254 refine Ideal.span_le.2 ?_
255 rintro _ ⟨n, rfl⟩
256 exact zcGroupLike_sub_one_mem_standardAugmentationIdeal C G n.1
258omit [IsTopologicalGroup H] in
259/--
260Source group-like elements with the same target differ by an element of the algebraic
261kernel-augmentation ideal.
262-/
263theorem zcGroupLike_sub_mem_kernelAugmentationIdealMul_of_map_eq
264 (psi : ContinuousMonoidHom G H) {g₁ g₂ : G} (h : psi g₁ = psi g₂) :
265 zcGroupLike C G g₁ - zcGroupLike C G g₂ ∈
266 zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi := by
267 let n : ProfiniteKernelSubgroup psi :=
268 ⟨g₂⁻¹ * g₁, by
269 change psi (g₂⁻¹ * g₁) = 1
270 rw [map_mul, map_inv, h]
271 simp only [inv_mul_cancel]⟩
272 have hgen :
273 zcGroupLike C G n.1 - 1 ∈
274 zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :=
275 zcGroupLike_sub_one_mem_kernelAugmentationIdealMul C psi n
276 have hmul :
277 zcGroupLike C G g₂ * (zcGroupLike C G n.1 - 1) ∈
278 zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :=
279 (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).mul_mem_left
280 (zcGroupLike C G g₂) hgen
281 have hidentity :
282 zcGroupLike C G g₂ * (zcGroupLike C G n.1 - 1) =
283 zcGroupLike C G g₁ - zcGroupLike C G g₂ := by
284 rw [mul_sub, ← map_mul, mul_one]
285 simp only [mul_inv_cancel_left, n]
286 simpa [hidentity] using hmul
288/-- The algebraic kernel-augmentation ideal maps to zero under the completed target map. -/
289theorem zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
290 (psi : ContinuousMonoidHom G H) :
291 zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi ≤
292 RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) := by
293 refine Ideal.span_le.2 ?_
294 rintro x ⟨n, rfl⟩
295 change zcCompletedGroupAlgebraMap C hC psi (zcGroupLike C G n.1 - 1) = 0
296 rw [map_sub, map_one, zcCompletedGroupAlgebraMap_groupLike]
297 have hn : psi n.1 = 1 := by
298 exact MonoidHom.mem_ker.mp
299 (show n.1 ∈ psi.toMonoidHom.ker from n.2)
300 rw [hn]
301 simp only [map_one, sub_self]
303/-- The kernel of the completed target map is closed in the inverse-limit topology. -/
304theorem isClosed_zcCompletedGroupAlgebraMap_ker
305 (psi : ContinuousMonoidHom G H) :
306 IsClosed
307 ((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
308 Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) := by
309 change IsClosed ((zcCompletedGroupAlgebraMap C hC psi) ⁻¹'
310 ({0} : Set (ZCCompletedGroupAlgebra C H)))
311 exact isClosed_singleton.preimage
312 (continuous_zcCompletedGroupAlgebraMap C hC psi)
314/-- The closure of the algebraic kernel-augmentation ideal is contained in the completed kernel. -/
315theorem closure_zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
316 (psi : ContinuousMonoidHom G H) :
317 closure
318 ((zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :
319 Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) ≤
320 ((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
321 Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) := by
322 exact closure_minimal
323 (by
324 intro x hx
325 exact zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
326 C hC psi hx)
327 (isClosed_zcCompletedGroupAlgebraMap_ker C hC psi)
329/--
330A finite target-stage relation-augmentation generator is the projection of an algebraic
331kernel-augmentation generator in \(\mathbb{Z}_C\llbracket G\rrbracket\).
332-/
333theorem zcCompletedGAMapStageRelationAugmentationGenerator_mem_proj_kernelAugmentationIdealMul
334 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
335 (i : ZCCompletedGroupAlgebraIndex C H)
336 (q :
337 (completedGroupAlgebraComapQuotientMapInClass
338 (G := G) (H := H) C hC psi i.2).ker) :
339 ∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
340 zcCompletedGroupAlgebraProjection C G
341 (i.1, completedGroupAlgebraComapIndexInClass
342 (G := G) (H := H) C hC psi i.2) y =
343 zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC psi i q := by
344 let U : Subgroup H := (((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H)
345 let V : Subgroup G :=
346 ((((OrderDual.ofDual
347 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2)).1 :
348 OpenNormalSubgroup G) : Subgroup G))
349 rcases QuotientGroup.mk'_surjective V q.1 with ⟨g, hg⟩
350 have hmap1 :
351 completedGroupAlgebraComapQuotientMapInClass
352 (G := G) (H := H) C hC psi i.2 q.1 = 1 := by
353 exact MonoidHom.mem_ker.mp
354 (show q.1 ∈ (completedGroupAlgebraComapQuotientMapInClass
355 (G := G) (H := H) C hC psi i.2).ker from q.2)
356 have hpsi_g_U : psi g ∈ U := by
357 rw [← hg, completedGroupAlgebraComapQuotientMapInClass_mk] at hmap1
358 exact (QuotientGroup.eq_one_iff (N := U) (psi g)).1 hmap1
359 rcases hpsi (psi g)⁻¹ with ⟨t, ht⟩
360 have htV : t ∈ V := by
361 change psi t ∈ U
362 rw [ht]
363 exact U.inv_mem hpsi_g_U
364 let n : ProfiniteKernelSubgroup psi := ⟨g * t, by
365 change psi (g * t) = 1
366 rw [map_mul, ht]
367 simp only [mul_inv_cancel]⟩
368 refine ⟨zcGroupLike C G n.1 - 1,
369 zcGroupLike_sub_one_mem_kernelAugmentationIdealMul C psi n, ?_⟩
370 have hqeq :
371 (QuotientGroup.mk' V (g * t) :
372 CompletedGroupAlgebraQuotientInClass G C
373 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2)) =
374 q.1 := by
375 rw [← hg]
376 apply QuotientGroup.eq.2
377 simpa [V, mul_assoc] using V.inv_mem htV
378 change
379 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
380 (CompletedGroupAlgebraQuotientInClass G C
381 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2))
382 (QuotientGroup.mk' V (g * t)) - 1 =
383 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
384 (CompletedGroupAlgebraQuotientInClass G C
385 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2)) q.1 - 1
386 rw [hqeq]
388/--
389Every element of a finite target-stage relation-augmentation ideal is the projection of an
390element of the algebraic completed kernel-augmentation ideal.
391-/
392theorem zcCompletedGAMapStageRelationAugmentationIdeal_mem_proj_kernelAugmentationIdealMul
393 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
394 (i : ZCCompletedGroupAlgebraIndex C H)
395 (x : zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC psi i) :
396 ∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
397 zcCompletedGroupAlgebraProjection C G
398 (i.1, completedGroupAlgebraComapIndexInClass
399 (G := G) (H := H) C hC psi i.2) y =
400 (x :
401 ZCCompletedGroupAlgebraStage C G
402 (i.1, completedGroupAlgebraComapIndexInClass
403 (G := G) (H := H) C hC psi i.2)) := by
404 let sourceIndex : ZCCompletedGroupAlgebraIndex C G :=
405 (i.1, completedGroupAlgebraComapIndexInClass
406 (G := G) (H := H) C hC psi i.2)
407 let R := ZCCompletedGroupAlgebraStage C G sourceIndex
408 let I := zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC psi i
409 let P : R → Prop := fun z =>
410 ∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
411 zcCompletedGroupAlgebraProjection C G sourceIndex y = z
412 have hxSpan :
413 (x : R) ∈ Submodule.span R
414 (Set.range (zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC psi i)) := by
415 change (x : R) ∈ zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC psi i
416 exact x.2
417 refine Submodule.span_induction (p := fun z _ => P z) ?_ ?_ ?_ ?_ hxSpan
418 · rintro _ ⟨q, rfl⟩
419 exact
420 zcCompletedGAMapStageRelationAugmentationGenerator_mem_proj_kernelAugmentationIdealMul
421 C hC psi hpsi i q
422 · exact ⟨0, (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).zero_mem, by simp only
423 [zcCompletedGroupAlgebraProjection_zero]⟩
424 · intro x y _ _ hx hy
425 rcases hx with ⟨x', hx'mem, hx'proj⟩
426 rcases hy with ⟨y', hy'mem, hy'proj⟩
427 refine ⟨x' + y',
428 (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).add_mem hx'mem hy'mem, ?_⟩
429 simp only [zcCompletedGroupAlgebraProjection_add, hx'proj, hy'proj]
430 · intro a x _ hx
431 rcases hx with ⟨x', hx'mem, hx'proj⟩
432 rcases zcCompletedGroupAlgebraProjection_surjective C G sourceIndex a with ⟨a', ha'⟩
433 refine ⟨a' * x',
434 (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).mul_mem_left a' hx'mem, ?_⟩
435 rw [zcCompletedGroupAlgebraProjection_mul, ha', hx'proj]
436 rfl
438omit [IsTopologicalGroup H] in
439/--
440A finite source-stage ideal generated by kernel classes of a quotient map is the projection of
441the algebraic completed kernel-augmentation ideal, provided every finite kernel class has a
442representative in the actual kernel of \(\psi\).
443-/
444theorem zcCompletedGAMapDomainKernelAugmentationIdeal_mem_proj_kernelAugmentationIdealMul
445 (psi : ContinuousMonoidHom G H)
446 (i : ZCCompletedGroupAlgebraIndex C G)
447 {Q : Type u} [Group Q]
448 (qmap : CompletedGroupAlgebraQuotientInClass G C i.2 →* Q)
449 (hkerLift :
450 ∀ q : qmap.ker,
451 ∃ n : ProfiniteKernelSubgroup psi,
452 QuotientGroup.mk'
453 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1 =
454 q.1)
455 (x : ZCCompletedGroupAlgebraStage C G i)
456 (hx :
457 x ∈ groupAlgebraMapDomainKernelAugmentationIdeal
458 (R := ModNCompletedCoeff i.1.modulus) qmap) :
459 ∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
460 zcCompletedGroupAlgebraProjection C G i y =
461 x := by
462 let R := ZCCompletedGroupAlgebraStage C G i
463 let I :=
464 groupAlgebraMapDomainKernelAugmentationIdeal
465 (R := ModNCompletedCoeff i.1.modulus) qmap
466 let P : R → Prop := fun z =>
467 ∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
468 zcCompletedGroupAlgebraProjection C G i y = z
469 have hxSpan :
470 x ∈ Submodule.span R
471 (Set.range fun q : qmap.ker =>
472 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
473 (CompletedGroupAlgebraQuotientInClass G C i.2) q.1 - 1) := by
474 change x ∈ I
475 exact hx
476 refine Submodule.span_induction (p := fun z _ => P z) ?_ ?_ ?_ ?_ hxSpan
477 · rintro _ ⟨q, rfl⟩
478 rcases hkerLift q with ⟨n, hn⟩
479 refine ⟨zcGroupLike C G n.1 - 1,
480 zcGroupLike_sub_one_mem_kernelAugmentationIdealMul C psi n, ?_⟩
481 change
482 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
483 (CompletedGroupAlgebraQuotientInClass G C i.2)
484 (QuotientGroup.mk'
485 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1) - 1 =
486 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
487 (CompletedGroupAlgebraQuotientInClass G C i.2) q.1 - 1
488 rw [hn]
489 · exact ⟨0, (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).zero_mem, by simp only
490 [zcCompletedGroupAlgebraProjection_zero]⟩
491 · intro x y _ _ hx hy
492 rcases hx with ⟨x', hx'mem, hx'proj⟩
493 rcases hy with ⟨y', hy'mem, hy'proj⟩
494 refine ⟨x' + y',
495 (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).add_mem hx'mem hy'mem, ?_⟩
496 simp only [zcCompletedGroupAlgebraProjection_add, hx'proj, hy'proj]
497 · intro a x _ hx
498 rcases hx with ⟨x', hx'mem, hx'proj⟩
499 rcases zcCompletedGroupAlgebraProjection_surjective C G i a with ⟨a', ha'⟩
500 refine ⟨a' * x',
501 (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).mul_mem_left a' hx'mem, ?_⟩
502 rw [zcCompletedGroupAlgebraProjection_mul, ha', hx'proj]
503 rfl
505/--
506The target quotient obtained by pushing a source quotient forward along an open surjective map.
507-/
508def zcCompletedGroupAlgebraOpenImageIndexInClass
510 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
511 (hfopen : IsOpenMap psi)
512 (i : ZCCompletedGroupAlgebraIndex C G) :
513 CompletedGroupAlgebraIndexInClass H C :=
514 OrderDual.toDual
515 (OpenNormalSubgroupInClass.mapOpenNormal_of_formation
516 (C := C) (G := G) hForm psi hfopen hpsi (OrderDual.ofDual i.2))
518/-- The two-parameter target stage whose group quotient is the open image of a source stage. -/
519def zcCompletedGroupAlgebraOpenImageTargetIndex
521 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
522 (hfopen : IsOpenMap psi)
523 (i : ZCCompletedGroupAlgebraIndex C G) :
524 ZCCompletedGroupAlgebraIndex C H :=
525 (i.1, zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)
527omit [IsTopologicalGroup G] in
528/-- The comap of the open image quotient is coarser than the original source quotient. -/
529theorem zcCompletedGroupAlgebraOpenImage_comapIndex_le
531 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
532 (hfopen : IsOpenMap psi)
533 (i : ZCCompletedGroupAlgebraIndex C G) :
534 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
535 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i) ≤
536 i.2 := by
537 let U : OpenNormalSubgroupInClass C G := OrderDual.ofDual i.2
538 let W : OpenNormalSubgroupInClass C H :=
539 OpenNormalSubgroupInClass.mapOpenNormal_of_formation
540 (C := C) (G := G) hForm psi hfopen hpsi U
541 intro g hg
542 change psi g ∈ ((W.1 : OpenNormalSubgroup H) : Subgroup H)
543 change psi g ∈
544 ((OpenNormalSubgroup.map psi hfopen hpsi (U.1 : OpenNormalSubgroup G) :
545 OpenNormalSubgroup H) : Subgroup H)
546 exact ⟨g, hg, rfl⟩
548/-- The source-stage quotient map \(G/U \to H/\psi(U)\) attached to an open surjective map. -/
549def zcCompletedGroupAlgebraOpenImageQuotientMap
551 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
552 (hfopen : IsOpenMap psi)
553 (i : ZCCompletedGroupAlgebraIndex C G) :
554 CompletedGroupAlgebraQuotientInClass G C i.2 →*
555 CompletedGroupAlgebraQuotientInClass H C
556 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i) :=
557 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC psi
558 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).comp
559 (OpenNormalSubgroupInClass.map
560 (C := C) (G := G)
561 (U := OrderDual.ofDual
562 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
563 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)))
564 (V := OrderDual.ofDual i.2)
565 (zcCompletedGroupAlgebraOpenImage_comapIndex_le C hC hForm psi hpsi hfopen i))
567/--
568The open-image quotient map sends a group-like class to its corresponding finite-stage quotient
569representative.
570-/
571@[simp 900]
572theorem zcCompletedGroupAlgebraOpenImageQuotientMap_mk
574 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
575 (hfopen : IsOpenMap psi)
576 (i : ZCCompletedGroupAlgebraIndex C G) (g : G) :
577 zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i
578 (QuotientGroup.mk'
579 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) g) =
580 QuotientGroup.mk'
581 ((((OrderDual.ofDual
582 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
583 OpenNormalSubgroup H) : Subgroup H)) (psi g) := by
584 rw [zcCompletedGroupAlgebraOpenImageQuotientMap]
585 change completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC psi
586 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)
587 (QuotientGroup.mk'
588 ((((OrderDual.ofDual
589 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
590 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i))).1 :
591 OpenNormalSubgroup G) : Subgroup G)) g) =
592 QuotientGroup.mk'
593 ((((OrderDual.ofDual
594 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
595 OpenNormalSubgroup H) : Subgroup H)) (psi g)
596 rw [completedGroupAlgebraComapQuotientMapInClass_mk]
598/-- The source-stage quotient map to the open image quotient is surjective. -/
599theorem zcCompletedGroupAlgebraOpenImageQuotientMap_surjective
601 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
602 (hfopen : IsOpenMap psi)
603 (i : ZCCompletedGroupAlgebraIndex C G) :
604 Function.Surjective
605 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i) := by
606 intro q
607 rcases QuotientGroup.mk'_surjective
608 ((((OrderDual.ofDual
609 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
610 OpenNormalSubgroup H) : Subgroup H)) q with
611 ⟨h, rfl⟩
612 rcases hpsi h with ⟨g, rfl⟩
613 refine ⟨QuotientGroup.mk'
614 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
615 rw [zcCompletedGroupAlgebraOpenImageQuotientMap_mk]
617/--
618Kernel classes of the source-stage quotient map lift to actual elements in the kernel of
619\(\psi\).
620-/
621theorem zcCompletedGroupAlgebraOpenImageQuotientMap_kernel_lift
623 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
624 (hfopen : IsOpenMap psi)
625 (i : ZCCompletedGroupAlgebraIndex C G) :
626 ∀ q : (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i).ker,
627 ∃ n : ProfiniteKernelSubgroup psi,
628 QuotientGroup.mk'
629 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1 =
630 q.1 := by
631 intro q
632 let U : OpenNormalSubgroupInClass C G := OrderDual.ofDual i.2
633 let W : OpenNormalSubgroupInClass C H :=
634 OpenNormalSubgroupInClass.mapOpenNormal_of_formation
635 (C := C) (G := G) hForm psi hfopen hpsi U
636 rcases QuotientGroup.mk'_surjective ((U.1 : OpenNormalSubgroup G) : Subgroup G) q.1 with
637 ⟨g, hg⟩
638 have hmap1 :
639 zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i q.1 = 1 :=
640 MonoidHom.mem_ker.mp q.2
641 have hpsi_g_W : psi g ∈ ((W.1 : OpenNormalSubgroup H) : Subgroup H) := by
642 rw [← hg] at hmap1
643 change
644 QuotientGroup.mk' ((W.1 : OpenNormalSubgroup H) : Subgroup H) (psi g) = 1 at hmap1
645 exact (QuotientGroup.eq_one_iff (N := ((W.1 : OpenNormalSubgroup H) : Subgroup H))
646 (psi g)).1 hmap1
647 rcases hpsi_g_W with ⟨u, hu, hpsi_u⟩
648 change psi u = psi g at hpsi_u
649 let n : ProfiniteKernelSubgroup psi := ⟨g * u⁻¹, by
650 change psi (g * u⁻¹) = 1
651 rw [map_mul, map_inv, hpsi_u]
652 simp only [mul_inv_cancel]⟩
653 refine ⟨n, ?_⟩
654 rw [← hg]
655 apply QuotientGroup.eq.2
656 simpa [n, mul_assoc] using (U.1 : OpenNormalSubgroup G).inv_mem hu
658/--
659The source-stage quotient map is the finite-stage map obtained by first transitioning to the
660comap of the open image and then applying the completed target-map stage.
661-/
662theorem zcCompletedGroupAlgebraOpenImageQuotientMap_stage_eq
664 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
665 (hfopen : IsOpenMap psi)
666 (i : ZCCompletedGroupAlgebraIndex C G) :
667 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
668 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i) =
669 (zcCompletedGroupAlgebraMapStage C hC psi
670 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i)).comp
671 (zcCompletedGroupAlgebraTransition C G
672 (show
673 (i.1,
674 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
675 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)) ≤ i from
676 ⟨le_rfl,
677 zcCompletedGroupAlgebraOpenImage_comapIndex_le C hC hForm psi hpsi hfopen i⟩)) := by
678 rw [zcCompletedGroupAlgebraOpenImageQuotientMap, MonoidAlgebra.mapDomainRingHom_comp]
679 rw [zcCompletedGroupAlgebraMapStage]
680 simp only [zcCompletedGroupAlgebraOpenImageTargetIndex]
681 congr 1
682 rw [zcCompletedGroupAlgebraTransition,
683 modNCompletedGroupAlgebraStageCoeffMapInClass_rfl, RingHom.id_comp]
684 rfl
686/--
687A completed-kernel element projects at any source stage into the finite kernel-augmentation
688ideal for the source-stage quotient map to the open image.
689-/
690theorem zcCompletedGAProj_mem_openImage_kernelAugmentationIdeal_of_mem_ker
692 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
693 (hfopen : IsOpenMap psi)
694 (i : ZCCompletedGroupAlgebraIndex C G)
695 (x : ZCCompletedGroupAlgebra C G)
696 (hx : x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi)) :
697 zcCompletedGroupAlgebraProjection C G i x ∈
698 groupAlgebraMapDomainKernelAugmentationIdeal
699 (R := ModNCompletedCoeff i.1.modulus)
700 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i) := by
701 have hmapzero : zcCompletedGroupAlgebraMap C hC psi x = 0 :=
702 (RingHom.mem_ker).1 hx
703 have htargetzero :
704 zcCompletedGroupAlgebraProjection C H
705 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i)
706 (zcCompletedGroupAlgebraMap C hC psi x) = 0 := by
707 rw [hmapzero]
708 simp only [zcCompletedGroupAlgebraProjection_zero]
709 have hsource :
710 (i.1,
711 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
712 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)) ≤ i :=
713 ⟨le_rfl, zcCompletedGroupAlgebraOpenImage_comapIndex_le C hC hForm psi hpsi hfopen i⟩
714 have hstagezero :
715 zcCompletedGroupAlgebraMapStage C hC psi
716 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i)
717 (zcCompletedGroupAlgebraTransition C G hsource
718 (zcCompletedGroupAlgebraProjection C G i x)) = 0 := by
719 rw [zcCompletedGroupAlgebraTransition_projection]
720 convert htargetzero using 1
721 rfl
722 have hqzero :
723 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
724 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)
725 (zcCompletedGroupAlgebraProjection C G i x) = 0 := by
726 rw [zcCompletedGroupAlgebraOpenImageQuotientMap_stage_eq C hC hForm psi hpsi hfopen i]
727 exact hstagezero
728 have hxker :
729 zcCompletedGroupAlgebraProjection C G i x ∈
730 RingHom.ker
731 (MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
732 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)) := by
733 rw [RingHom.mem_ker]
734 exact hqzero
735 rwa [groupAlgebraMapDomainRingHom_ker_eq_kernelAugmentationIdeal_of_surjective
736 (R := ModNCompletedCoeff i.1.modulus)
737 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)
738 (zcCompletedGroupAlgebraOpenImageQuotientMap_surjective C hC hForm psi hpsi hfopen i)]
739 at hxker
741/--
742Any source-stage projection of a completed-kernel element is the projection of an element of the
743algebraic completed kernel-augmentation ideal.
744-/
745theorem zcCompletedGAMap_sourceStageKernel_mem_proj_kernelAugmentationIdealMul_of_openMap_surj
747 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
748 (hfopen : IsOpenMap psi)
749 (i : ZCCompletedGroupAlgebraIndex C G)
750 (x : ZCCompletedGroupAlgebra C G)
751 (hx : x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi)) :
752 ∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
753 zcCompletedGroupAlgebraProjection C G i y =
754 zcCompletedGroupAlgebraProjection C G i x := by
755 exact
756 zcCompletedGAMapDomainKernelAugmentationIdeal_mem_proj_kernelAugmentationIdealMul
757 C psi i
758 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)
759 (zcCompletedGroupAlgebraOpenImageQuotientMap_kernel_lift C hC hForm psi hpsi hfopen i)
760 (zcCompletedGroupAlgebraProjection C G i x)
761 (zcCompletedGAProj_mem_openImage_kernelAugmentationIdeal_of_mem_ker
762 C hC hForm psi hpsi hfopen i x hx)
764/--
765For an open surjective target map, the completed kernel is the closure of the algebraic
766kernel-augmentation ideal generated by \([n]-1\) for \(n \in \ker \psi\).
767-/
768theorem closure_zcCompletedGAKernelAugmentationIdealMul_eq_ker_map_of_openMap_surj
771 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
772 (hfopen : IsOpenMap psi) :
773 closure
774 ((zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :
775 Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) =
776 ((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
777 Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) := by
778 let S := zcCompletedGroupAlgebraSystem C G
779 let Y : Set (ZCCompletedGroupAlgebra C G) :=
780 (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :
781 Set (ZCCompletedGroupAlgebra C G))
782 let K : Set (ZCCompletedGroupAlgebra C G) :=
783 (RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
784 Set (ZCCompletedGroupAlgebra C G))
785 letI : Nonempty (ZCCompletedGroupAlgebraIndex C G) :=
786 ⟨(ProCIntegerIndex.terminal (C := C) inferInstance, zcCompletedGroupAlgebraTopIndex C G)⟩
787 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TopologicalSpace (S.X i) := fun _ =>
788 inferInstance
789 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, CompactSpace (S.X i) := fun i => by
790 dsimp [S, zcCompletedGroupAlgebraSystem]
791 change @CompactSpace (ZCCompletedGroupAlgebraStage C G i) ⊥
792 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
793 letI : Finite (ZCCompletedGroupAlgebraStage C G i) :=
794 finite_modNCompletedGroupAlgebraStageInClass
795 (n := i.1.modulus) (G := G) C i.2
796 exact Finite.compactSpace
797 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, T2Space (S.X i) := fun i => by
798 dsimp [S, zcCompletedGroupAlgebraSystem]
799 change @T2Space (ZCCompletedGroupAlgebraStage C G i) ⊥
800 exact @DiscreteTopology.toT2Space _ ⊥ ⟨rfl⟩
801 have hdir : Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex C G →
802 ZCCompletedGroupAlgebraIndex C G) :=
803 directed_zcCompletedGroupAlgebraIndex_of_formation (C := C) (H := G) hForm
804 refine le_antisymm ?_ ?_
805 · intro x hx
806 exact closure_zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
807 C hC psi hx
808 · intro x hx
809 have hxClosureS :
810 (show S.inverseLimit from x) ∈
811 closure (show Set S.inverseLimit from Y) := by
812 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]
813 intro i
814 rcases
815 zcCompletedGAMap_sourceStageKernel_mem_proj_kernelAugmentationIdealMul_of_openMap_surj
816 C hC hForm psi hpsi hfopen i x (by simpa [K] using hx) with
817 ⟨y, hy, hyproj⟩
818 refine ⟨y, subset_closure ?_, ?_⟩
819 · convert hy using 1
820 rfl
821 exact hyproj
822 convert hxClosureS using 1 <;>
823 rfl
825end KernelAugmentationIdeal
827end
829end FoxDifferential