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

FoxDifferential/Completed/ProCIntegerCoefficients/AugmentationIdeal/Kernel.lean

1import FoxDifferential.Completed.Continuous.Naturality
2import FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Closure
3import ProCGroups.ProC.Kernels
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Completed/ProCIntegerCoefficients/AugmentationIdeal/Kernel.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Completed group algebra coefficients
16This module records augmentation-ideal statements for pro-\(C\) integer completed coefficient rings, including closure, finite-stage membership, and kernel descriptions.
17-/
18namespace FoxDifferential
20noncomputable section
22open ProCGroups.ProC
23open ProCGroups.Completion
24open ProCGroups.InverseSystems
26universe u v w
28section GroupAlgebraMapKernel
30variable {R : Type v} {A : Type u} {B : Type w} [CommRing R] [Group A] [Group B]
32/-- The ideal in `R[A]` generated by `[k] - 1` for `k ∈ ker f`. -/
34 Ideal (MonoidAlgebra R A) :=
35 Ideal.span (Set.range fun k : f.ker => MonoidAlgebra.of R A k.1 - 1)
37/-- A kernel augmentation generator lies in the group-algebra kernel-augmentation ideal. -/
39 (f : A →* B) (k : f.ker) :
40 MonoidAlgebra.of R A k.1 - 1 ∈
42 Ideal.subset_span (Set.mem_range_self k)
45 (f : A →* B) (r : R) (x : MonoidAlgebra R A) :
46 MonoidAlgebra.mapDomainRingHom R f (r • x) =
47 r • MonoidAlgebra.mapDomainRingHom R f x := by
48 rw [Algebra.smul_def, Algebra.smul_def, RingHom.map_mul]
49 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
50 MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]
52/-- A chosen linear section of the group-algebra map induced by a surjective group homomorphism.
53-/
55 (f : A →* B) (hf : Function.Surjective f) :
56 MonoidAlgebra R B →ₗ[R] MonoidAlgebra R A :=
57 Finsupp.linearCombination R
58 (fun b : B => MonoidAlgebra.of R A (Function.surjInv hf b))
60@[simp]
62 (f : A →* B) (hf : Function.Surjective f) (b : B) :
64 (MonoidAlgebra.of R B b) =
65 MonoidAlgebra.of R A (Function.surjInv hf b) := by
66 change
67 Finsupp.linearCombination R
68 (fun b : B => MonoidAlgebra.of R A (Function.surjInv hf b))
69 (Finsupp.single b (1 : R)) =
70 MonoidAlgebra.of R A (Function.surjInv hf b)
71 rw [Finsupp.linearCombination_single, one_smul]
73/-- The chosen group-algebra section is a right inverse to the map induced by `f`. -/
75 (f : A →* B) (hf : Function.Surjective f) (y : MonoidAlgebra R B) :
76 MonoidAlgebra.mapDomainRingHom R f
77 (groupAlgebraMapDomainTargetSection (R := R) f hf y) = y := by
78 classical
79 refine MonoidAlgebra.induction_on
80 (p := fun y : MonoidAlgebra R B =>
81 MonoidAlgebra.mapDomainRingHom R f
82 (groupAlgebraMapDomainTargetSection (R := R) f hf y) = y)
83 y ?single ?add ?smul
84 · intro b
86 rw [show MonoidAlgebra.mapDomainRingHom R f
87 (MonoidAlgebra.of R A (Function.surjInv hf b)) =
88 MonoidAlgebra.of R B (f (Function.surjInv hf b)) by
89 simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk,
90 MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]]
91 exact congrArg (MonoidAlgebra.of R B) (Function.surjInv_eq hf b)
92 · intro x y hx hy
93 rw [map_add, map_add, hx, hy]
94 · intro a y hy
95 rw [show groupAlgebraMapDomainTargetSection (R := R) f hf (a • y) =
96 a • groupAlgebraMapDomainTargetSection (R := R) f hf y by
100/-- A source basis element differs from the chosen lift of its target image by a kernel
101augmentation element. -/
103 (f : A →* B) (hf : Function.Surjective f) (a : A) :
104 MonoidAlgebra.of R A a -
106 (MonoidAlgebra.mapDomainRingHom R f (MonoidAlgebra.of R A a)) ∈
108 let t : B := f a
109 let lift : A := Function.surjInv hf t
110 let q : f.ker :=
111 ⟨lift⁻¹ * a, by
112 change f (lift⁻¹ * a) = 1
113 rw [map_mul, map_inv]
114 have hlift : f lift = t := Function.surjInv_eq hf t
115 rw [hlift]
116 simp only [inv_mul_cancel, t]⟩
117 have hsection :
119 (MonoidAlgebra.mapDomainRingHom R f (MonoidAlgebra.of R A a)) =
120 MonoidAlgebra.of R A lift := by
121 rw [show MonoidAlgebra.mapDomainRingHom R f (MonoidAlgebra.of R A a) =
122 MonoidAlgebra.of R B (f a) by
123 simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk,
124 MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]]
125 simpa [t, lift, MonoidAlgebra.of, MonoidAlgebra.single] using
127 rw [hsection]
128 have hmul :
129 MonoidAlgebra.of R A lift *
130 (MonoidAlgebra.of R A q.1 - 1) =
131 MonoidAlgebra.of R A a - MonoidAlgebra.of R A lift := by
132 simp only [MonoidAlgebra.of_apply]
133 rw [mul_sub, MonoidAlgebra.single_mul_single, mul_one]
134 simp only [mul_inv_cancel_left, mul_one, q]
135 rw [← hmul]
136 exact
140/-- Every group-algebra element differs from the chosen lift of its target image by a kernel
141augmentation element. -/
143 (f : A →* B) (hf : Function.Surjective f) (x : MonoidAlgebra R A) :
145 (MonoidAlgebra.mapDomainRingHom R f x) ∈
147 classical
148 refine MonoidAlgebra.induction_on
149 (p := fun x : MonoidAlgebra R A =>
151 (MonoidAlgebra.mapDomainRingHom R f x) ∈
153 x ?single ?add ?smul
154 · intro a
155 exact
157 (R := R) f hf a
158 · intro x y hx hy
159 have hcalc :
161 (MonoidAlgebra.mapDomainRingHom R f (x + y)) =
163 (MonoidAlgebra.mapDomainRingHom R f x)) +
165 (MonoidAlgebra.mapDomainRingHom R f y)) := by
167 abel
168 rw [hcalc]
169 exact (groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f).add_mem hx hy
170 · intro r x hx
171 have hcalc :
172 r • x - groupAlgebraMapDomainTargetSection (R := R) f hf
173 (MonoidAlgebra.mapDomainRingHom R f (r • x)) =
174 r • (x - groupAlgebraMapDomainTargetSection (R := R) f hf
175 (MonoidAlgebra.mapDomainRingHom R f x)) := by
177 rw [hcalc]
178 rw [Algebra.smul_def]
179 exact (groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f).mul_mem_left _ hx
181/-- For a surjective group map, the kernel of `R[A] → R[B]` is generated by the augmentation
182generators attached to `ker f`. -/
184 (f : A →* B) (hf : Function.Surjective f) :
185 RingHom.ker (MonoidAlgebra.mapDomainRingHom R f) =
187 apply le_antisymm
188 · intro x hx
189 have hxmap : MonoidAlgebra.mapDomainRingHom R f x = 0 :=
190 (RingHom.mem_ker).1 hx
191 have hdiff :=
193 (R := R) f hf x
194 rw [hxmap, map_zero, sub_zero] at hdiff
195 exact hdiff
196 · refine Ideal.span_le.2 ?_
197 rintro _ ⟨k, rfl⟩
198 change MonoidAlgebra.mapDomainRingHom R f
199 (MonoidAlgebra.of R A k.1 - 1) = 0
200 rw [map_sub, map_one]
201 have hk : f k.1 = 1 := MonoidHom.mem_ker.mp k.2
202 simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk,
203 MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, hk, MonoidAlgebra.one_def, sub_self]
205end GroupAlgebraMapKernel
207section KernelAugmentationIdeal
209variable (C : ProCGroups.FiniteGroupClass.{u})
211variable {G H : Type u}
212variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
213variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
215/-- The algebraic ideal in `Z_C[[G]]` generated by completed augmentation generators coming
216from the kernel of `psi`. -/
218 (psi : ContinuousMonoidHom G H) :
220 Ideal.span
221 (Set.range fun n : ProfiniteKernelSubgroup psi =>
222 zcGroupLike C G n.1 - 1)
224omit [IsTopologicalGroup H] in
225/-- A kernel augmentation generator lies in the algebraic kernel-augmentation ideal. -/
227 (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi) :
228 zcGroupLike C G n.1 - 1 ∈
230 Ideal.subset_span (Set.mem_range_self n)
232omit [IsTopologicalGroup H] in
233/-- The kernel-augmentation ideal is contained in the standard source augmentation ideal. -/
235 (psi : ContinuousMonoidHom G H) :
238 refine Ideal.span_le.2 ?_
239 rintro _ ⟨n, rfl⟩
242omit [IsTopologicalGroup H] in
243/-- Source group-like elements with the same target differ by an element of the algebraic
244kernel-augmentation ideal. -/
246 (psi : ContinuousMonoidHom G H) {g₁ g₂ : G} (h : psi g₁ = psi g₂) :
247 zcGroupLike C G g₁ - zcGroupLike C G g₂ ∈
250 ⟨g₂⁻¹ * g₁, by
251 change psi (g₂⁻¹ * g₁) = 1
252 rw [map_mul, map_inv, h]
253 simp only [inv_mul_cancel]⟩
254 have hgen :
255 zcGroupLike C G n.1 - 1 ∈
258 have hmul :
259 zcGroupLike C G g₂ * (zcGroupLike C G n.1 - 1) ∈
262 (zcGroupLike C G g₂) hgen
263 have hidentity :
264 zcGroupLike C G g₂ * (zcGroupLike C G n.1 - 1) =
265 zcGroupLike C G g₁ - zcGroupLike C G g₂ := by
266 rw [mul_sub, ← map_mul, mul_one]
267 simp only [mul_inv_cancel_left, n]
268 simpa [hidentity] using hmul
270/-- The algebraic kernel-augmentation ideal maps to zero under the completed target map. -/
272 (psi : ContinuousMonoidHom G H) :
274 RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) := by
275 refine Ideal.span_le.2 ?_
276 rintro x ⟨n, rfl⟩
277 change zcCompletedGroupAlgebraMap C hC psi (zcGroupLike C G n.1 - 1) = 0
279 have hn : psi n.1 = 1 := by
280 exact MonoidHom.mem_ker.mp
281 (show n.1 ∈ psi.toMonoidHom.ker from n.2)
282 rw [hn]
283 simp only [map_one, sub_self]
285/-- The kernel of the completed target map is closed in the inverse-limit topology. -/
288 (psi : ContinuousMonoidHom G H) :
289 IsClosed
290 ((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
291 Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) := by
292 change IsClosed ((zcCompletedGroupAlgebraMap C hC psi) ⁻¹'
293 ({0} : Set (ZCCompletedGroupAlgebra C H)))
294 exact isClosed_singleton.preimage
297/-- The closure of the algebraic kernel-augmentation ideal is contained in the completed kernel.
298-/
301 (psi : ContinuousMonoidHom G H) :
302 closure
305 ((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
306 Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) := by
307 exact closure_minimal
308 (by
309 intro x hx
311 C hC psi hx)
314/-- A finite target-stage relation-augmentation generator is the projection of an algebraic
315kernel-augmentation generator in `Z_C[[G]]`. -/
317 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
319 (q :
320 (completedGroupAlgebraComapQuotientMapInClass
321 (G := G) (H := H) C hC psi i.2).ker) :
324 (i.1, completedGroupAlgebraComapIndexInClass
325 (G := G) (H := H) C hC psi i.2) y =
327 let U : Subgroup H := (((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H)
328 let V : Subgroup G :=
329 ((((OrderDual.ofDual
330 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2)).1 :
331 OpenNormalSubgroup G) : Subgroup G))
332 rcases QuotientGroup.mk'_surjective V q.1 with ⟨g, hg⟩
333 have hmap1 :
334 completedGroupAlgebraComapQuotientMapInClass
335 (G := G) (H := H) C hC psi i.2 q.1 = 1 := by
336 exact MonoidHom.mem_ker.mp
337 (show q.1 ∈ (completedGroupAlgebraComapQuotientMapInClass
338 (G := G) (H := H) C hC psi i.2).ker from q.2)
339 have hpsi_g_U : psi g ∈ U := by
340 rw [← hg, completedGroupAlgebraComapQuotientMapInClass_mk] at hmap1
341 exact (QuotientGroup.eq_one_iff (N := U) (psi g)).1 hmap1
342 rcases hpsi (psi g)⁻¹ with ⟨t, ht⟩
343 have htV : t ∈ V := by
344 change psi t ∈ U
345 rw [ht]
346 exact U.inv_mem hpsi_g_U
347 let n : ProfiniteKernelSubgroup psi := ⟨g * t, by
348 change psi (g * t) = 1
349 rw [map_mul, ht]
350 simp only [mul_inv_cancel]⟩
351 refine ⟨zcGroupLike C G n.1 - 1,
353 have hqeq :
354 (QuotientGroup.mk' V (g * t) :
355 CompletedGroupAlgebraQuotientInClass G C
356 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2)) =
357 q.1 := by
358 rw [← hg]
359 apply QuotientGroup.eq.2
360 simpa [V, mul_assoc] using V.inv_mem htV
361 change
362 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
363 (CompletedGroupAlgebraQuotientInClass G C
364 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2))
365 (QuotientGroup.mk' V (g * t)) - 1 =
366 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
367 (CompletedGroupAlgebraQuotientInClass G C
368 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2)) q.1 - 1
369 rw [hqeq]
371/-- Every element of a finite target-stage relation-augmentation ideal is the projection of an
372element of the algebraic completed kernel-augmentation ideal. -/
374 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
379 (i.1, completedGroupAlgebraComapIndexInClass
380 (G := G) (H := H) C hC psi i.2) y =
381 (x :
383 (i.1, completedGroupAlgebraComapIndexInClass
384 (G := G) (H := H) C hC psi i.2)) := by
385 let sourceIndex : ZCCompletedGroupAlgebraIndex C G :=
386 (i.1, completedGroupAlgebraComapIndexInClass
387 (G := G) (H := H) C hC psi i.2)
388 let R := ZCCompletedGroupAlgebraStage C G sourceIndex
390 let P : R → Prop := fun z =>
393 have hxSpan :
394 (x : R) ∈ Submodule.span R
397 exact x.2
398 refine Submodule.span_induction (p := fun z _ => P z) ?_ ?_ ?_ ?_ hxSpan
399 · rintro _ ⟨q, rfl⟩
400 exact
402 C hC psi hpsi i q
404 · intro x y _ _ hx hy
405 rcases hx with ⟨x', hx'mem, hx'proj⟩
406 rcases hy with ⟨y', hy'mem, hy'proj⟩
407 refine ⟨x' + y',
408 (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).add_mem hx'mem hy'mem, ?_⟩
409 simp only [zcCompletedGroupAlgebraProjection_add, hx'proj, hy'proj]
410 · intro a x _ hx
411 rcases hx with ⟨x', hx'mem, hx'proj⟩
412 rcases zcCompletedGroupAlgebraProjection_surjective C G sourceIndex a with ⟨a', ha'⟩
413 refine ⟨a' * x',
414 (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).mul_mem_left a' hx'mem, ?_⟩
416 rfl
418omit [IsTopologicalGroup H] in
419/-- A finite source-stage ideal generated by kernel classes of a quotient map is the projection of
420the algebraic completed kernel-augmentation ideal, provided every finite kernel class has a
421representative in the actual kernel of `psi`. -/
423 (psi : ContinuousMonoidHom G H)
425 {Q : Type u} [Group Q]
426 (qmap : CompletedGroupAlgebraQuotientInClass G C i.2 →* Q)
427 (hkerLift :
428 ∀ q : qmap.ker,
430 QuotientGroup.mk'
431 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1 =
432 q.1)
434 (hx :
436 (R := ModNCompletedCoeff i.1.modulus) qmap) :
439 x := by
441 let I :=
443 (R := ModNCompletedCoeff i.1.modulus) qmap
444 let P : R → Prop := fun z =>
447 have hxSpan :
448 x ∈ Submodule.span R
449 (Set.range fun q : qmap.ker =>
450 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
451 (CompletedGroupAlgebraQuotientInClass G C i.2) q.1 - 1) := by
452 change x ∈ I
453 exact hx
454 refine Submodule.span_induction (p := fun z _ => P z) ?_ ?_ ?_ ?_ hxSpan
455 · rintro _ ⟨q, rfl⟩
456 rcases hkerLift q with ⟨n, hn⟩
457 refine ⟨zcGroupLike C G n.1 - 1,
459 change
460 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
461 (CompletedGroupAlgebraQuotientInClass G C i.2)
462 (QuotientGroup.mk'
463 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1) - 1 =
464 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
465 (CompletedGroupAlgebraQuotientInClass G C i.2) q.1 - 1
466 rw [hn]
468 · intro x y _ _ hx hy
469 rcases hx with ⟨x', hx'mem, hx'proj⟩
470 rcases hy with ⟨y', hy'mem, hy'proj⟩
471 refine ⟨x' + y',
472 (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).add_mem hx'mem hy'mem, ?_⟩
473 simp only [zcCompletedGroupAlgebraProjection_add, hx'proj, hy'proj]
474 · intro a x _ hx
475 rcases hx with ⟨x', hx'mem, hx'proj⟩
476 rcases zcCompletedGroupAlgebraProjection_surjective C G i a with ⟨a', ha'⟩
477 refine ⟨a' * x',
478 (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).mul_mem_left a' hx'mem, ?_⟩
480 rfl
482/-- The target quotient obtained by pushing a source quotient forward along an open surjective
483map. -/
486 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
487 (hfopen : IsOpenMap psi)
489 CompletedGroupAlgebraIndexInClass H C :=
490 OrderDual.toDual
491 (OpenNormalSubgroupInClass.mapOpenNormal_of_formation
492 (C := C) (G := G) hForm psi hfopen hpsi (OrderDual.ofDual i.2))
494/-- The two-parameter target stage whose group quotient is the open image of a source stage. -/
497 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
498 (hfopen : IsOpenMap psi)
501 (i.1, zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)
503omit [IsTopologicalGroup G] in
504/-- The comap of the open image quotient is coarser than the original source quotient. -/
507 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
508 (hfopen : IsOpenMap psi)
510 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
511 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i) ≤
512 i.2 := by
513 let U : OpenNormalSubgroupInClass C G := OrderDual.ofDual i.2
515 OpenNormalSubgroupInClass.mapOpenNormal_of_formation
516 (C := C) (G := G) hForm psi hfopen hpsi U
517 intro g hg
518 change psi g ∈ ((W.1 : OpenNormalSubgroup H) : Subgroup H)
519 change psi g ∈
520 ((OpenNormalSubgroup.map psi hfopen hpsi (U.1 : OpenNormalSubgroup G) :
521 OpenNormalSubgroup H) : Subgroup H)
522 exact ⟨g, hg, rfl⟩
524/-- The source-stage quotient map `G/U -> H/psi(U)` attached to an open surjective map. -/
527 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
528 (hfopen : IsOpenMap psi)
530 CompletedGroupAlgebraQuotientInClass G C i.2 →*
531 CompletedGroupAlgebraQuotientInClass H C
532 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i) :=
533 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC psi
534 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).comp
535 (OpenNormalSubgroupInClass.map
536 (C := C) (G := G)
537 (U := OrderDual.ofDual
538 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
540 (V := OrderDual.ofDual i.2)
541 (zcCompletedGroupAlgebraOpenImage_comapIndex_le C hC hForm psi hpsi hfopen i))
543@[simp 900]
546 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
547 (hfopen : IsOpenMap psi)
548 (i : ZCCompletedGroupAlgebraIndex C G) (g : G) :
550 (QuotientGroup.mk'
551 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) g) =
552 QuotientGroup.mk'
553 ((((OrderDual.ofDual
554 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
555 OpenNormalSubgroup H) : Subgroup H)) (psi g) := by
557 change completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC psi
559 (QuotientGroup.mk'
560 ((((OrderDual.ofDual
561 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
562 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i))).1 :
563 OpenNormalSubgroup G) : Subgroup G)) g) =
564 QuotientGroup.mk'
565 ((((OrderDual.ofDual
566 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
567 OpenNormalSubgroup H) : Subgroup H)) (psi g)
568 rw [completedGroupAlgebraComapQuotientMapInClass_mk]
570/-- The source-stage quotient map to the open image quotient is surjective. -/
573 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
574 (hfopen : IsOpenMap psi)
576 Function.Surjective
577 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i) := by
578 intro q
579 rcases QuotientGroup.mk'_surjective
580 ((((OrderDual.ofDual
581 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
582 OpenNormalSubgroup H) : Subgroup H)) q with
583 ⟨h, rfl⟩
584 rcases hpsi h with ⟨g, rfl⟩
585 refine ⟨QuotientGroup.mk'
586 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
589/-- Kernel classes of the source-stage quotient map lift to actual elements of `ker psi`. -/
592 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
593 (hfopen : IsOpenMap psi)
595 ∀ q : (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i).ker,
597 QuotientGroup.mk'
598 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1 =
599 q.1 := by
600 intro q
601 let U : OpenNormalSubgroupInClass C G := OrderDual.ofDual i.2
603 OpenNormalSubgroupInClass.mapOpenNormal_of_formation
604 (C := C) (G := G) hForm psi hfopen hpsi U
605 rcases QuotientGroup.mk'_surjective ((U.1 : OpenNormalSubgroup G) : Subgroup G) q.1 with
606 ⟨g, hg⟩
607 have hmap1 :
608 zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i q.1 = 1 :=
609 MonoidHom.mem_ker.mp q.2
610 have hpsi_g_W : psi g ∈ ((W.1 : OpenNormalSubgroup H) : Subgroup H) := by
611 rw [← hg] at hmap1
612 change
613 QuotientGroup.mk' ((W.1 : OpenNormalSubgroup H) : Subgroup H) (psi g) = 1 at hmap1
614 exact (QuotientGroup.eq_one_iff (N := ((W.1 : OpenNormalSubgroup H) : Subgroup H))
615 (psi g)).1 hmap1
616 rcases hpsi_g_W with ⟨u, hu, hpsi_u⟩
617 change psi u = psi g at hpsi_u
618 let n : ProfiniteKernelSubgroup psi := ⟨g * u⁻¹, by
619 change psi (g * u⁻¹) = 1
620 rw [map_mul, map_inv, hpsi_u]
621 simp only [mul_inv_cancel]⟩
622 refine ⟨n, ?_⟩
623 rw [← hg]
624 apply QuotientGroup.eq.2
625 simpa [n, mul_assoc] using (U.1 : OpenNormalSubgroup G).inv_mem hu
627/-- The source-stage quotient map is the finite-stage map obtained by first transitioning to the
628comap of the open image and then applying the completed target-map stage. -/
631 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
632 (hfopen : IsOpenMap psi)
634 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
635 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i) =
637 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i)).comp
639 (show
640 (i.1,
641 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
642 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)) ≤ i from
643 ⟨le_rfl,
644 zcCompletedGroupAlgebraOpenImage_comapIndex_le C hC hForm psi hpsi hfopen i⟩)) := by
645 rw [zcCompletedGroupAlgebraOpenImageQuotientMap, MonoidAlgebra.mapDomainRingHom_comp]
650/-- A completed-kernel element projects at any source stage into the finite kernel-augmentation
651ideal for the source-stage quotient map to the open image. -/
654 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
655 (hfopen : IsOpenMap psi)
658 (hx : x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi)) :
661 (R := ModNCompletedCoeff i.1.modulus)
662 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i) := by
663 have hmapzero : zcCompletedGroupAlgebraMap C hC psi x = 0 :=
664 (RingHom.mem_ker).1 hx
665 have htargetzero :
668 (zcCompletedGroupAlgebraMap C hC psi x) = 0 := by
669 rw [hmapzero]
671 have hsource :
672 (i.1,
673 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
674 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)) ≤ i :=
675 ⟨le_rfl, zcCompletedGroupAlgebraOpenImage_comapIndex_le C hC hForm psi hpsi hfopen i⟩
676 have hstagezero :
683 using htargetzero
684 have hqzero :
685 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
686 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)
689 exact hstagezero
690 have hxker :
692 RingHom.ker
693 (MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
694 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)) := by
695 rw [RingHom.mem_ker]
696 exact hqzero
698 (R := ModNCompletedCoeff i.1.modulus)
699 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)
701 at hxker
703/-- Any source-stage projection of a completed-kernel element is the projection of an element of
704the algebraic completed kernel-augmentation ideal. -/
707 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
708 (hfopen : IsOpenMap psi)
711 (hx : x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi)) :
715 exact
717 C psi i
718 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)
722 C hC hForm psi hpsi hfopen i x hx)
724/-- For an open surjective target map, the completed kernel is the closure of the algebraic
725kernel-augmentation ideal generated by `[n] - 1` for `n ∈ ker psi`. -/
730 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
731 (hfopen : IsOpenMap psi) :
732 closure
735 ((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
736 Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) := by
738 let Y : Set (ZCCompletedGroupAlgebra C G) :=
741 let K : Set (ZCCompletedGroupAlgebra C G) :=
742 (RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
744 letI : Nonempty (ZCCompletedGroupAlgebraIndex C G) :=
745 ⟨(ProCIntegerIndex.terminal (C := C) inferInstance, zcCompletedGroupAlgebraTopIndex C G)⟩
746 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TopologicalSpace (S.X i) := fun _ =>
747 inferInstance
748 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, CompactSpace (S.X i) := fun i => by
750 infer_instance
751 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, T2Space (S.X i) := fun i => by
753 infer_instance
754 have hdir : Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex C G →
757 refine le_antisymm ?_ ?_
758 · intro x hx
760 C hC psi hx
761 · intro x hx
762 have hxClosure : x ∈ closure Y := by
763 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]
764 intro i
765 rcases
767 C hC hForm psi hpsi hfopen i x (by simpa [K] using hx) with
768 ⟨y, hy, hyproj⟩
769 refine ⟨y, subset_closure (by simpa [Y] using hy), ?_⟩
770 exact hyproj
771 simpa [Y] using hxClosure
773end KernelAugmentationIdeal
775end
777end FoxDifferential