FoxDifferential/Completed/Continuous/Universal/AugmentationQuotient.lean

1import FoxDifferential.Completed.Continuous.Universal.NaturalTopology
2import FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Kernel
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/Continuous/Universal/AugmentationQuotient.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Source augmentation quotient for the completed differential module
15This file records the source-augmentation quotient used in the Morishita 10.3.4
16route. The algebraic quotient is kept as the literal `I(G) / I(ker psi) I(G)`;
17the closed finite-stage quotient carries an unconditional completed
18`Z_C[[H]]`-module structure.
19-/
21namespace FoxDifferential
23noncomputable section
25open ProCGroups.ProC
27universe u
29section KernelAugmentationQuotient
31variable (C : ProCGroups.FiniteGroupClass.{u})
32variable {G H : Type u}
33variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
34variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
36/-- The algebraic product `I(ker psi) I(G)` inside the algebraic standard source augmentation
37ideal. -/
39 (psi : ContinuousMonoidHom G H) :
40 Submodule (ZCCompletedGroupAlgebra C G)
42 Submodule.span (ZCCompletedGroupAlgebra C G)
43 (Set.range fun p :
45 (zcGroupLike C G p.1.1 - 1) • p.2)
47omit [IsTopologicalGroup H] in
48/-- A generator `(n - 1) s` lies in the algebraic product `I(ker psi) I(G)`. -/
50 (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi)
52 (zcGroupLike C G n.1 - 1) • s ∈
54 Submodule.subset_span (Set.mem_range_self (n, s))
56/-- Projection of the algebraic standard augmentation ideal to a finite augmentation stage. -/
62 intro x
67@[simp]
75 rfl
82 have hval : Continuous (fun x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G =>
84 (continuous_zcCompletedGroupAlgebraProjection C G i).comp continuous_subtype_val
85 exact Continuous.subtype_mk hval
88/-- On a finite coefficient stage, the identity crossed-differential boundary is a left inverse
89to the additive lift from the finite augmentation ideal. -/
95 (S := ModNCompletedCoeff i.1.modulus)
96 (G := CompletedGroupAlgebraQuotientInClass G C i.2)
99 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
100 have hxaug :
101 (MonoidAlgebra.lift
102 (ModNCompletedCoeff i.1.modulus)
103 (ModNCompletedCoeff i.1.modulus)
104 (CompletedGroupAlgebraQuotientInClass G C i.2)
105 (1 : CompletedGroupAlgebraQuotientInClass G C i.2 →* ModNCompletedCoeff i.1.modulus))
106 (x : ZCCompletedGroupAlgebraStage C G i) = 0 := by
109 (C := C) (H := G) (i := i) (x := (x : ZCCompletedGroupAlgebraStage C G i))).1 x.2
110 exact
112 (S := ModNCompletedCoeff i.1.modulus)
113 (G := CompletedGroupAlgebraQuotientInClass G C i.2)
115 hxaug
117@[simp]
123 apply Subtype.ext
127@[simp]
135 apply Subtype.ext
139@[simp]
148 apply Subtype.ext
154/-- The finite-stage projection of the standard augmentation ideal, as a semilinear map over
155the completed group-algebra projection. -/
163 map_add' := by
164 intro x y
166 map_smul' := by
167 intro a x
170@[simp]
177 rfl
179@[simp]
187 simpa using
190/-- The product of all finite-stage projections of the standard completed augmentation ideal. -/
198@[simp]
205 rfl
207/-- Finite-stage projections separate points of the standard completed augmentation ideal. -/
210 Function.Injective
212 intro x y hxy
213 apply Subtype.ext
214 apply Subtype.ext
215 funext i
216 exact congrArg Subtype.val (congrFun hxy i)
218/-- Extensionality for standard completed augmentation ideal elements by finite-stage projections. -/
225 x = y :=
227 (by
228 funext i
229 exact h i)
231/-- Every finite standard augmentation stage is hit by the completed standard augmentation
232ideal projection. -/
236 Function.Surjective
238 intro x
240 (C := C) (H := G) i x with
241 ⟨y, hy, hproj⟩
242 refine ⟨⟨y, hy⟩, ?_⟩
243 apply Subtype.ext
246/-- The finite-stage product `I(ker) I(G/U)` attached to the open-image quotient at a source
247stage. -/
252 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
253 (hfopen : IsOpenMap psi)
257 Submodule.span (ZCCompletedGroupAlgebraStage C G i)
258 (Set.range fun p :
259 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i).ker ×
261 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
262 (CompletedGroupAlgebraQuotientInClass G C i.2) p.1.1 - 1) • p.2)
264/-- A finite-stage product generator belongs to the finite-stage product submodule. -/
269 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
270 (hfopen : IsOpenMap psi)
272 (q : (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i).ker)
274 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
275 (CompletedGroupAlgebraQuotientInClass G C i.2) q.1 - 1) • s ∈
277 C hC hForm psi hpsi hfopen i :=
278 Submodule.subset_span (Set.mem_range_self (q, s))
280/-- The class of an actual kernel element in the finite-stage open-image kernel. -/
285 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
286 (hfopen : IsOpenMap psi)
289 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i).ker := by
290 refine ⟨QuotientGroup.mk'
291 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1, ?_⟩
292 rw [MonoidHom.mem_ker]
294 change QuotientGroup.mk'
295 ((((OrderDual.ofDual
296 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
297 OpenNormalSubgroup H) : Subgroup H)) (psi n.1) = 1
298 rw [show psi n.1 = 1 from n.2]
299 simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one]
301@[simp]
306 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
307 (hfopen : IsOpenMap psi)
310 (zcCompletedGroupAlgebraOpenImageKernelClass C hC hForm psi hpsi hfopen i n).1 =
311 QuotientGroup.mk'
312 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1 :=
313 rfl
315@[simp 900]
320 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
321 (hfopen : IsOpenMap psi)
326 ((zcGroupLike C G n.1 - 1) • s) =
327 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
328 (CompletedGroupAlgebraQuotientInClass G C i.2)
330 C hC hForm psi hpsi hfopen i n).1 - 1) •
332 apply Subtype.ext
334 ((zcGroupLike C G n.1 - 1) * (s : ZCCompletedGroupAlgebra C G)) =
335 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
336 (CompletedGroupAlgebraQuotientInClass G C i.2)
337 (QuotientGroup.mk'
338 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1) - 1) *
342 MonoidAlgebra.of_apply, zcCompletedGroupAlgebraProjection_one, QuotientGroup.mk'_apply]
344/-- Projection of the algebraic product lands in the corresponding finite-stage product. -/
349 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
350 (hfopen : IsOpenMap psi)
356 C hC hForm psi hpsi hfopen i := by
357 let T :=
359 C hC hForm psi hpsi hfopen i
360 refine Submodule.span_induction
362 ?_ ?_ ?_ ?_ hx
363 · rintro _ ⟨p, rfl
364 rcases p with ⟨n, s⟩
366 C hC hForm psi hpsi hfopen i n s]
367 exact
369 C hC hForm psi hpsi hfopen i
370 (zcCompletedGroupAlgebraOpenImageKernelClass C hC hForm psi hpsi hfopen i n)
373 · intro x y _ _ hx hy
374 simpa [T] using T.add_mem hx hy
375 · intro a x _ hx
377 exact T.smul_mem (zcCompletedGroupAlgebraProjection C G i a) hx
379/-- Every finite-stage product element is the projection of an algebraic product element. -/
384 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
385 (hfopen : IsOpenMap psi)
388 (hx :
390 C hC hForm psi hpsi hfopen i) :
393 let T :=
395 C hC hForm psi hpsi hfopen i
396 let P : zcCompletedGroupAlgebraStageAugmentationIdeal C G i → Prop := fun x =>
399 refine Submodule.span_induction (p := fun x _ => P x) ?_ ?_ ?_ ?_ hx
400 · rintro _ ⟨p, rfl
401 rcases p with ⟨q, s⟩
402 rcases
404 C hC hForm psi hpsi hfopen i q with
405 ⟨n, hn⟩
406 rcases
408 (C := C) (H := G) i s with
409 ⟨s', hs', hs'proj⟩
411 refine ⟨(zcGroupLike C G n.1 - 1) • sStd,
414 C hC hForm psi hpsi hfopen i n sStd]
415 apply Subtype.ext
416 change
417 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
418 (CompletedGroupAlgebraQuotientInClass G C i.2)
419 (QuotientGroup.mk'
420 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1) - 1) *
422 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
423 (CompletedGroupAlgebraQuotientInClass G C i.2) q.1 - 1) * s.1
424 rw [hn, hs'proj]
425 · refine ⟨0, (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi).zero_mem, ?_⟩
427 · intro x y _ _ hx hy
428 rcases hx with ⟨x', hx'mem, hx'proj⟩
429 rcases hy with ⟨y', hy'mem, hy'proj⟩
430 refine ⟨x' + y',
433 · intro a x _ hx
434 rcases hx with ⟨x', hx'mem, hx'proj⟩
435 rcases zcCompletedGroupAlgebraProjection_surjective C G i a with ⟨a', ha'⟩
436 refine ⟨a' • x',
440/-- The closed finite-stage hull of `I(ker psi) I(G)` inside the standard source
441augmentation ideal: an element belongs exactly when every finite projection belongs to the
442corresponding finite-stage open-image kernel product. -/
447 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
448 (hfopen : IsOpenMap psi) :
451 carrier := {x | ∀ i : ZCCompletedGroupAlgebraIndex C G,
454 C hC hForm psi hpsi hfopen i}
455 zero_mem' := by
456 intro i
458 add_mem' := by
459 intro x y hx hy i
460 simpa using
462 C hC hForm psi hpsi hfopen i).add_mem (hx i) (hy i)
463 smul_mem' := by
464 intro a x hx i
466 exact
468 C hC hForm psi hpsi hfopen i).smul_mem
471/-- The algebraic product is contained in its finite-stage closed hull. -/
476 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
477 (hfopen : IsOpenMap psi) :
480 C hC hForm psi hpsi hfopen := by
481 intro x hx i
482 exact
484 C hC hForm psi hpsi hfopen i hx
486/-- The finite-stage hull is closed in the standard source augmentation ideal. -/
492 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
493 (hfopen : IsOpenMap psi) :
494 IsClosed
496 C hC hForm psi hpsi hfopen :
502 C hC hForm psi hpsi hfopen i}
503 simp only [Set.setOf_forall]
504 refine isClosed_iInter ?_
505 intro i
506 haveI : DiscreteTopology (zcCompletedGroupAlgebraStageAugmentationIdeal C G i) := by
507 infer_instance
508 exact
509 (isClosed_discrete
511 C hC hForm psi hpsi hfopen i :
515/-- The closure of the algebraic product is contained in the finite-stage closed hull. -/
521 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
522 (hfopen : IsOpenMap psi) :
523 closure
527 C hC hForm psi hpsi hfopen :
529 exact
530 closure_minimal
531 (by
532 intro x hx
533 exact
535 C hC hForm psi hpsi hfopen hx)
537 C hC hForm psi hpsi hfopen)
539/-- The finite-stage closed hull is contained in the closure of the algebraic product. The
540proof uses the inverse-limit closed-set criterion: every finite coordinate of an element in
541the hull is the coordinate of an algebraic product element. -/
547 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
548 (hfopen : IsOpenMap psi) :
550 C hC hForm psi hpsi hfopen :
552 closure
555 intro x hx
560 let Yamb : Set R := Subtype.val '' Ystd
561 have hxAmb : (x : R) ∈ closure Yamb := by
562 letI : Nonempty (ZCCompletedGroupAlgebraIndex C G) :=
565 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TopologicalSpace (Ssys.X i) := fun _ =>
566 inferInstance
567 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, CompactSpace (Ssys.X i) := fun i => by
569 infer_instance
570 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, T2Space (Ssys.X i) := fun i => by
572 infer_instance
573 have hdir : Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex C G →
576 rw [Ssys.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]
577 intro i
578 rcases
580 C hC hForm psi hpsi hfopen i
582 (hx i) with
583 ⟨y, hy, hyproj⟩
584 refine ⟨(y : R), subset_closure ?_, ?_⟩
585 · exact ⟨y, by simpa [Ystd] using hy, rfl
588 congrArg Subtype.val hyproj
589 have hclosure :
590 closure Ystd =
591 (Subtype.val : zcCompletedGroupAlgebraStandardAugmentationIdeal C G → R) ⁻¹'
592 closure Yamb := by
593 exact Topology.IsEmbedding.subtypeVal.closure_eq_preimage_closure_image Ystd
594 show x ∈ closure Ystd
595 rw [hclosure]
596 exact hxAmb
598/-- The closure of `I(ker psi) I(G)` is exactly the finite-stage kernel-product condition. -/
604 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
605 (hfopen : IsOpenMap psi) :
606 closure
610 C hC hForm psi hpsi hfopen :
612 exact Set.Subset.antisymm
614 C hC hForm psi hpsi hfopen)
616 C hC hForm psi hpsi hfopen)
618/-- The algebraic product is closed exactly when it already equals the finite-stage closed
619hull. This is the precise non-circular closedness frontier. -/
625 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
626 (hfopen : IsOpenMap psi) :
627 IsClosed
633 C hC hForm psi hpsi hfopen :
635 constructor
636 · intro hclosed
637 apply Set.Subset.antisymm
639 C hC hForm psi hpsi hfopen
640 · intro x hx
641 have hxclosure :
642 x ∈ closure
646 C hC hForm psi hpsi hfopen]
647 exact hx
648 rwa [hclosed.closure_eq] at hxclosure
649 · intro hEq
650 rw [hEq]
652 C hC hForm psi hpsi hfopen
655/-- The source-side augmentation quotient
656`I Z_C[[G]] / I(ker psi) I Z_C[[G]]`, before descending scalars to `Z_C[[H]]`. -/
658 (psi : ContinuousMonoidHom G H) : Type u :=
662/-- The closed source-side augmentation quotient, using the finite-stage closed hull of
663`I(ker psi) I(G)` as denominator. -/
669 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
670 (hfopen : IsOpenMap psi) : Type u :=
673 C hC hForm psi hpsi hfopen
675/-- The quotient map to the closed source augmentation quotient is a quotient map. -/
681 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
682 (hfopen : IsOpenMap psi) :
683 Topology.IsQuotientMap
685 C hC hForm psi hpsi hfopen).mkQ := by
686 rw [Topology.isQuotientMap_iff]
687 constructor
688 · exact
689 Submodule.Quotient.mk_surjective
691 C hC hForm psi hpsi hfopen)
692 · intro s
693 rfl
695/-- Continuity out of the closed source augmentation quotient can be tested after precomposing
696with the quotient map from the standard augmentation ideal. -/
702 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
703 (hfopen : IsOpenMap psi)
704 {A : Type u} [TopologicalSpace A]
705 (f : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen → A) :
706 Continuous f ↔
709 C hC hForm psi hpsi hfopen).mkQ x)) := by
710 simpa [Function.comp_def] using
712 C hC hForm psi hpsi hfopen).continuous_iff (g := f)
714/-- The closed source augmentation quotient is T1 for the quotient topology. -/
720 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
721 (hfopen : IsOpenMap psi) :
722 T1Space (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) := by
723 letI : IsClosed
725 C hC hForm psi hpsi hfopen :
730 C hC hForm psi hpsi hfopen
731 infer_instance
733/-- The zero class is closed in the closed source augmentation quotient. -/
739 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
740 (hfopen : IsOpenMap psi) :
741 IsClosed
742 ({0} : Set
743 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)) := by
744 letI : T1Space
745 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
747 exact isClosed_singleton
749/-- The finite-stage quotient of the source augmentation ideal by the open-image kernel product. -/
754 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
755 (hfopen : IsOpenMap psi)
756 (i : ZCCompletedGroupAlgebraIndex C G) : Type u :=
759 C hC hForm psi hpsi hfopen i
761/-- The finite-stage coordinate of the closed source augmentation quotient. -/
767 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
768 (hfopen : IsOpenMap psi)
770 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen →ₛₗ[
772 KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i :=
774 C hC hForm psi hpsi hfopen).mapQ
776 C hC hForm psi hpsi hfopen i)
778 (by
779 intro x hx
780 exact hx i)
782@[simp 900]
788 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
789 (hfopen : IsOpenMap psi)
793 C hC hForm psi hpsi hfopen i
795 C hC hForm psi hpsi hfopen).mkQ x) =
797 C hC hForm psi hpsi hfopen i).mkQ
799 KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) := by
800 exact
801 Submodule.mapQ_apply
803 C hC hForm psi hpsi hfopen)
805 C hC hForm psi hpsi hfopen i)
807 x
809/-- Each finite-stage coordinate of the closed source augmentation quotient is continuous. -/
815 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
816 (hfopen : IsOpenMap psi)
818 Continuous
820 C hC hForm psi hpsi hfopen i) := by
822 (C := C) (G := G) (H := H) hC hForm psi hpsi hfopen]
823 have hproj :
826 have hq :
829 C hC hForm psi hpsi hfopen i).mkQ y :
830 KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i)) :=
831 continuous_quotient_mk'
832 simpa using hq.comp hproj
834/-- The product of all finite-stage coordinates of the closed source augmentation quotient. -/
840 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
841 (hfopen : IsOpenMap psi) :
842 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen →
844 KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i :=
846 C hC hForm psi hpsi hfopen i x
848@[simp]
854 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
855 (hfopen : IsOpenMap psi)
856 (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
859 C hC hForm psi hpsi hfopen x i =
861 C hC hForm psi hpsi hfopen i x :=
862 rfl
864/-- The finite-stage coordinate product of the closed source augmentation quotient is continuous. -/
870 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
871 (hfopen : IsOpenMap psi) :
872 Continuous
874 C hC hForm psi hpsi hfopen) := by
875 exact continuous_pi fun i =>
877 C hC hForm psi hpsi hfopen i
879/-- Finite-stage coordinates separate points in the closed source augmentation quotient. -/
885 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
886 (hfopen : IsOpenMap psi) :
887 Function.Injective
889 C hC hForm psi hpsi hfopen) := by
890 let S :=
892 C hC hForm psi hpsi hfopen
893 intro qx qy hxy
894 revert qy
895 refine Submodule.Quotient.induction_on (p := S) qx ?_
896 intro x qy hxy
897 revert hxy
898 refine Submodule.Quotient.induction_on (p := S) qy ?_
899 intro y hxy
900 apply (Submodule.Quotient.eq S).2
901 change x - y ∈ S
902 intro i
903 let T :=
905 C hC hForm psi hpsi hfopen i
906 have hi :
908 C hC hForm psi hpsi hfopen i (Submodule.Quotient.mk (p := S) x) =
910 C hC hForm psi hpsi hfopen i (Submodule.Quotient.mk (p := S) y) := by
911 exact congrFun hxy i
912 have hstage :
915 apply (Submodule.Quotient.eq T).1
916 simpa [S, T] using hi
917 simpa [S, T] using hstage
919/-- Extensionality for the closed source augmentation quotient by finite-stage coordinates. -/
925 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
926 (hfopen : IsOpenMap psi)
927 {x y : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen}
930 C hC hForm psi hpsi hfopen i x =
932 C hC hForm psi hpsi hfopen i y) :
933 x = y := by
934 exact
936 C hC hForm psi hpsi hfopen
937 (by
938 funext i
939 exact h i)
941/-- The quotient topology on the closed source augmentation quotient is exactly the topology
942induced by all finite closed-quotient coordinates. -/
948 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
949 (hfopen : IsOpenMap psi) :
950 (inferInstance :
951 TopologicalSpace
952 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)) =
953 TopologicalSpace.induced
955 C hC hForm psi hpsi hfopen) inferInstance := by
956 let Sclosed :=
958 C hC hForm psi hpsi hfopen
959 let Q := KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
960 let stageProduct :=
962 C hC hForm psi hpsi hfopen
963 ext U
964 constructor
965 · intro hU
966 let Tind : TopologicalSpace Q :=
967 TopologicalSpace.induced stageProduct inferInstance
968 rw [@isOpen_iff_forall_mem_open Q Tind U]
969 intro qx hqxU
970 refine Submodule.Quotient.induction_on
971 (p := Sclosed)
972 (C := fun qx =>
973 qx ∈ U → ∃ t, t ⊆ U ∧ @IsOpen Q Tind t ∧ qx ∈ t)
974 qx ?_ hqxU
975 intro x hxU
977 Sclosed.mkQ
978 have hquot :
979 @Topology.IsQuotientMap
981 inferInstance (QuotientModule.Quotient.topologicalSpace Sclosed) q := by
982 simpa [q, Sclosed] using
984 C hC hForm psi hpsi hfopen
985 have hUquot :
986 @IsOpen Q (QuotientModule.Quotient.topologicalSpace Sclosed) U := hU
987 have hpreOpen :
988 @IsOpen
990 inferInstance (q ⁻¹' U) := by
991 letI : TopologicalSpace Q := QuotientModule.Quotient.topologicalSpace Sclosed
992 exact ((Topology.isQuotientMap_iff.mp hquot).2 U).1 hUquot
993 rcases isOpen_induced_iff.mp hpreOpen with ⟨V, hVopen, hVeq⟩
994 have hxV : (x : ZCCompletedGroupAlgebra C G) ∈ V := by
995 have hxpre : x ∈ q ⁻¹' U := hxU
996 rwa [← hVeq] at hxpre
998 letI : Nonempty (ZCCompletedGroupAlgebraIndex C G) :=
1001 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TopologicalSpace (Ssys.X i) := fun _ =>
1002 inferInstance
1003 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, CompactSpace (Ssys.X i) := fun i => by
1005 infer_instance
1006 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, T2Space (Ssys.X i) := fun i => by
1008 infer_instance
1009 have hdir : Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex C G →
1012 rcases Ssys.exists_projection_preimage_subset hdir hVopen hxV with
1013 ⟨i, W, hWopen, hxW, hWV⟩
1014 let t : Set Q :=
1016 C hC hForm psi hpsi hfopen i z =
1018 C hC hForm psi hpsi hfopen i (q x)}
1019 refine ⟨t, ?_, ?_, ?_⟩
1020 · intro z hz
1021 refine Submodule.Quotient.induction_on
1022 (p := Sclosed)
1023 (C := fun z => z ∈ t → z ∈ U)
1024 z ?_ hz
1025 intro y hy
1026 let T :=
1028 C hC hForm psi hpsi hfopen i
1029 have hyStage :
1032 apply (Submodule.Quotient.eq T).1
1033 have hy' := hy
1034 dsimp [t, q] at hy'
1035 simpa [Sclosed, T] using hy'
1036 rcases
1038 C hC hForm psi hpsi hfopen i
1041 hyStage with
1042 ⟨r, hr, hrproj⟩
1043 have hq : q (y - r) = q y := by
1044 apply (Submodule.Quotient.eq Sclosed).2
1045 change (y - r) - y ∈ Sclosed
1046 have hdiff : (y - r) - y = -r := by
1047 abel
1048 rw [hdiff]
1049 exact Sclosed.neg_mem
1051 C hC hForm psi hpsi hfopen hr)
1052 have hproj_eq :
1056 abel
1057 have hyW : Ssys.projection i ((y - r : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
1058 ZCCompletedGroupAlgebra C G) ∈ W := by
1059 have hval := congrArg Subtype.val hproj_eq
1060 change
1065 (x : ZCCompletedGroupAlgebra C G) at hval
1066 have hxW' :
1068 (x : ZCCompletedGroupAlgebra C G) ∈ W := by
1069 simpa [Ssys, zcCompletedGroupAlgebraSystem] using hxW
1070 change
1074 rw [hval]
1075 exact hxW'
1076 have hyV :
1079 hWV hyW
1080 have hyU : q (y - r) ∈ U := by
1081 have hyPre :
1084 ZCCompletedGroupAlgebra C G) ⁻¹' V := hyV
1085 rwa [hVeq] at hyPre
1086 rwa [hq] at hyU
1087 · letI : TopologicalSpace Q := Tind
1088 have hprod : Continuous stageProduct :=
1089 continuous_induced_dom
1090 have hcoord :
1091 Continuous (fun z : Q =>
1093 C hC hForm psi hpsi hfopen i z) := by
1094 simpa [stageProduct,
1096 (continuous_apply i).comp hprod
1097 have hsingle_open :
1098 IsOpen
1100 C hC hForm psi hpsi hfopen i (q x)} :
1101 Set (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i)) := by
1102 let T :=
1104 C hC hForm psi hpsi hfopen i
1105 haveI : DiscreteTopology (zcCompletedGroupAlgebraStageAugmentationIdeal C G i) := by
1106 infer_instance
1107 change
1108 @IsOpen
1109 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i)
1110 (TopologicalSpace.coinduced T.mkQ inferInstance)
1112 C hC hForm psi hpsi hfopen i (q x)} :
1113 Set (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i))
1114 rw [isOpen_coinduced]
1115 exact isOpen_discrete _
1116 exact
1117 hsingle_open.preimage hcoord
1118 · exact rfl
1119 · intro hU
1120 rcases isOpen_induced_iff.mp hU with ⟨V, hVopen, hVU⟩
1121 rw [← hVU]
1122 exact hVopen.preimage
1124 C hC hForm psi hpsi hfopen)
1126/-- The finite-stage source-to-open-image group-algebra map used to descend the source-stage
1127action on the closed finite augmentation quotient to the matching target stage. -/
1132 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1133 (hfopen : IsOpenMap psi)
1137 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i) :=
1138 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
1139 (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)
1141@[simp]
1146 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1147 (hfopen : IsOpenMap psi)
1149 (q : CompletedGroupAlgebraQuotientInClass G C i.2) :
1151 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
1152 (CompletedGroupAlgebraQuotientInClass G C i.2) q) =
1153 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
1154 (CompletedGroupAlgebraQuotientInClass H C
1155 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i).2)
1157 C hC hForm psi hpsi hfopen i q) := by
1158 simp only [zcCompletedGroupAlgebraOpenImageStageRingHom, MonoidAlgebra.of_apply]
1159 exact MonoidAlgebra.mapDomain_single
1161/-- The finite-stage source-to-open-image group-algebra map is surjective. -/
1166 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1167 (hfopen : IsOpenMap psi)
1169 Function.Surjective
1171 C hC hForm psi hpsi hfopen i) := by
1173 MonoidAlgebra.mapDomainRingHom_apply] using
1174 (Finsupp.mapDomain_surjective (M := ModNCompletedCoeff i.1.modulus)
1176 C hC hForm psi hpsi hfopen i))
1178/-- Source-stage elements in the kernel of the open-image stage map multiply the finite
1179augmentation stage into the finite kernel-product denominator. -/
1184 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1185 (hfopen : IsOpenMap psi)
1188 (hk : k ∈ RingHom.ker
1190 C hC hForm psi hpsi hfopen i))
1192 k • s ∈
1194 C hC hForm psi hpsi hfopen i := by
1196 C hC hForm psi hpsi hfopen i
1197 let T :=
1199 C hC hForm psi hpsi hfopen i
1200 have hkIdeal :
1202 (R := ModNCompletedCoeff i.1.modulus) f := by
1203 have hk' :
1204 k ∈ RingHom.ker
1205 (MonoidAlgebra.mapDomainRingHom
1206 (ModNCompletedCoeff i.1.modulus) f) := by
1209 (R := ModNCompletedCoeff i.1.modulus) f
1211 C hC hForm psi hpsi hfopen i)] at hk'
1212 change k • s ∈ T
1214 refine Submodule.span_induction
1215 (p := fun k _ => k • s ∈ T) ?hgen ?hzero ?hadd ?hsmul hkIdeal
1216 · rintro _ ⟨q, rfl
1217 exact
1219 C hC hForm psi hpsi hfopen i q s
1220 · simp only [zero_smul, zero_mem]
1221 · intro a b _ _ ha hb
1222 simpa [add_smul] using T.add_mem ha hb
1223 · intro a b _ hb
1224 simpa [mul_smul] using T.smul_mem a hb
1226/-- Source-stage kernels act trivially on the closed finite augmentation quotient. -/
1231 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1232 (hfopen : IsOpenMap psi)
1235 (hk : k ∈ RingHom.ker
1237 C hC hForm psi hpsi hfopen i))
1238 (x : KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :
1239 k • x = 0 := by
1240 let T :=
1242 C hC hForm psi hpsi hfopen i
1243 refine Submodule.Quotient.induction_on (p := T) x ?_
1244 intro s
1245 apply (Submodule.Quotient.mk_eq_zero (p := T)).2
1246 exact
1248 C hC hForm psi hpsi hfopen i k hk s
1250/-- The finite closed augmentation quotient as a module over the matching open-image target
1251group-algebra stage. -/
1256 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1257 (hfopen : IsOpenMap psi)
1259 Module
1262 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) := by
1264 C hC hForm psi hpsi hfopen i
1266 C hC hForm psi hpsi hfopen i
1267 letI : SMul
1270 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
1271fun a x => Function.surjInv hφ a • x⟩
1272 refine hφ.moduleLeft φ ?_
1273 intro a x
1274 change Function.surjInv hφ (φ a) • x = a • x
1275 have hdiff : Function.surjInv hφ (φ a) - a ∈ RingHom.ker φ := by
1276 rw [RingHom.mem_ker, map_sub, Function.surjInv_eq hφ, sub_self]
1277 have hzero :=
1279 C hC hForm psi hpsi hfopen i
1280 (Function.surjInv hφ (φ a) - a) hdiff x
1281 rw [sub_smul] at hzero
1282 exact sub_eq_zero.mp hzero
1288 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1289 (hfopen : IsOpenMap psi)
1292 (x : KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :
1293 letI : Module
1296 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
1298 C hC hForm psi hpsi hfopen i
1299 zcCompletedGroupAlgebraOpenImageStageRingHom C hC hForm psi hpsi hfopen i a • x =
1300 a • x := by
1302 C hC hForm psi hpsi hfopen i
1304 C hC hForm psi hpsi hfopen i
1305 letI : Module
1308 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
1310 C hC hForm psi hpsi hfopen i
1311 change Function.surjInv hφ (φ a) • x = a • x
1312 have hdiff : Function.surjInv hφ (φ a) - a ∈ RingHom.ker φ := by
1313 rw [RingHom.mem_ker, map_sub, Function.surjInv_eq hφ, sub_self]
1314 have hzero :=
1316 C hC hForm psi hpsi hfopen i
1317 (Function.surjInv hφ (φ a) - a) hdiff x
1318 rw [sub_smul] at hzero
1319 exact sub_eq_zero.mp hzero
1321/-- The finite source quotient paired with the open-image target stage for a source group-algebra
1322coordinate. -/
1327 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1328 (hfopen : IsOpenMap psi)
1331 source := OrderDual.ofDual i.2
1332 target := zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i
1334 intro g hg
1335 change psi g ∈
1336 ((((OrderDual.ofDual
1337 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i).2).1 :
1338 OpenNormalSubgroup H) : Subgroup H))
1339 exact ⟨g, hg, rfl
1341/-- The finite closed source-boundary coordinate at one source group-algebra stage. -/
1346 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1347 (hfopen : IsOpenMap psi)
1349 (q : CompletedGroupAlgebraQuotientInClass G C i.2) :
1350 KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i :=
1351 Submodule.Quotient.mk
1353 C hC hForm psi hpsi hfopen i)
1356@[simp 900]
1361 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1362 (hfopen : IsOpenMap psi)
1365 (zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i)) :
1367 (zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i) q =
1369 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
1370 (CompletedGroupAlgebraQuotientInClass G C i.2) q) := by
1371 refine QuotientGroup.induction_on q ?_
1372 intro g
1374 have hq :
1376 (QuotientGroup.mk'
1377 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) g) =
1378 QuotientGroup.mk'
1379 ((((OrderDual.ofDual
1380 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i).2).1 :
1381 OpenNormalSubgroup H) : Subgroup H)) (psi g) :=
1383 C hC hForm psi hpsi hfopen i g
1387 congrArg
1388 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
1389 (CompletedGroupAlgebraQuotientInClass H C
1390 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i).2))
1391 hq.symm
1393/-- The finite source-boundary coordinate is a crossed differential over the matching
1394open-image target stage. -/
1399 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1400 (hfopen : IsOpenMap psi)
1402 let j := zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i
1403 letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
1404 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
1406 C hC hForm psi hpsi hfopen i
1409 (fun q : zcCompletedDifferentialModuleStageSource C psi.toMonoidHom j =>
1411 C hC hForm psi hpsi hfopen i q) := by
1412 let j := zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i
1413 let T :=
1415 C hC hForm psi hpsi hfopen i
1416 letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
1417 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
1419 C hC hForm psi hpsi hfopen i
1420 change
1423 (fun q : zcCompletedDifferentialModuleStageSource C psi.toMonoidHom j =>
1425 C hC hForm psi hpsi hfopen i q)
1426 intro q r
1429 (C := C) (hC := hC) (hForm := hForm) (psi := psi)
1430 (hpsi := hpsi) (hfopen := hfopen) (i := i)
1431 (a := MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
1432 (CompletedGroupAlgebraQuotientInClass G C i.2) q)
1434 C hC hForm psi hpsi hfopen i r)]
1435 change
1436 Submodule.Quotient.mk (p := T)
1438 Submodule.Quotient.mk (p := T)
1440 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
1441 (CompletedGroupAlgebraQuotientInClass G C i.2) q •
1442 Submodule.Quotient.mk (p := T)
1444 rw [← Submodule.Quotient.mk_smul, ← Submodule.Quotient.mk_add]
1445 apply congrArg (fun s : zcCompletedGroupAlgebraStageAugmentationIdeal C G i =>
1446 Submodule.Quotient.mk (p := T) s)
1447 apply Subtype.ext
1448 change
1449 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
1450 (CompletedGroupAlgebraQuotientInClass G C i.2) (q * r) - 1 =
1451 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
1452 (CompletedGroupAlgebraQuotientInClass G C i.2) q - 1) +
1453 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
1454 (CompletedGroupAlgebraQuotientInClass G C i.2) q *
1455 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
1456 (CompletedGroupAlgebraQuotientInClass G C i.2) r - 1)
1457 rw [map_mul, mul_sub, mul_one]
1458 abel
1460/-- The finite-stage lift induced by the finite closed source-boundary coordinate. -/
1465 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1466 (hfopen : IsOpenMap psi)
1468 let j := zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i
1469 letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
1470 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
1472 C hC hForm psi hpsi hfopen i
1475 (zcCompletedDifferentialModuleStageSource C psi.toMonoidHom j) →ₗ[
1477 KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i := by
1478 let j := zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i
1479 letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
1480 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
1482 C hC hForm psi hpsi hfopen i
1483 exact
1485 (R := zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
1487 C hC hForm psi hpsi hfopen i)
1489@[simp 900]
1494 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1495 (hfopen : IsOpenMap psi)
1498 (zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i))
1500 (zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i)) :
1501 let j := zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i
1502 letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
1503 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
1505 C hC hForm psi hpsi hfopen i
1507 C hC hForm psi hpsi hfopen i (Finsupp.single q a) =
1509 C hC hForm psi hpsi hfopen i q := by
1510 let j := zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i
1511 letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
1512 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
1514 C hC hForm psi hpsi hfopen i
1515 simp only [ContinuousMonoidHom.coe_toMonoidHom, Lean.Elab.WF.paramLet,
1518/-- The canonical quotient map from the algebraic kernel-product quotient to its closed
1519finite-stage quotient. -/
1525 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1526 (hfopen : IsOpenMap psi) :
1528 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen :=
1531 C hC hForm psi hpsi hfopen)
1532 LinearMap.id
1533 (by
1534 intro x hx
1535 simpa using
1537 C hC hForm psi hpsi hfopen hx)
1539@[simp]
1545 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1546 (hfopen : IsOpenMap psi)
1549 C hC hForm psi hpsi hfopen (Submodule.Quotient.mk x) =
1550 Submodule.Quotient.mk x := by
1552 Submodule.mapQ_apply]
1553 rfl
1555/-- The canonical map from the algebraic quotient
1556`I(G) / I(ker psi) I(G)` to the closed finite-stage quotient is injective exactly when the
1557algebraic product already equals its finite-stage closed hull. -/
1563 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1564 (hfopen : IsOpenMap psi) :
1565 Function.Injective
1567 C hC hForm psi hpsi hfopen) ↔
1571 C hC hForm psi hpsi hfopen :
1574 let T :=
1576 C hC hForm psi hpsi hfopen
1577 let Q :=
1579 C hC hForm psi hpsi hfopen
1580 constructor
1581 · intro hQ
1582 apply Set.Subset.antisymm
1583 · intro x hx
1585 C hC hForm psi hpsi hfopen hx
1586 · intro x hx
1587 have hmap :
1588 Q (Submodule.Quotient.mk (p := S) x) = 0 := by
1590 (C := C) (hC := hC) (hForm := hForm) (psi := psi)
1591 (hpsi := hpsi) (hfopen := hfopen) x]
1592 exact (Submodule.Quotient.mk_eq_zero (p := T) (x := x)).2 hx
1593 have hzero :
1594 (Submodule.Quotient.mk (p := S) x :
1596 apply hQ
1597 rw [hmap, map_zero]
1598 exact (Submodule.Quotient.mk_eq_zero (p := S) (x := x)).1 hzero
1599 · intro hEq a b hxy
1600 revert b
1601 refine Submodule.Quotient.induction_on
1602 (p := S) a ?_
1603 intro x y hxy
1604 revert hxy
1605 refine Submodule.Quotient.induction_on
1606 (p := S) y ?_
1607 intro y hxy
1608 apply (Submodule.Quotient.eq S).2
1609 have hmemT : x - y ∈ T := by
1610 apply (Submodule.Quotient.eq T).1
1612 (C := C) (hC := hC) (hForm := hForm) (psi := psi)
1613 (hpsi := hpsi) (hfopen := hfopen)] using hxy
1614 have hEqST : (S : Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)) = T := by
1615 simpa [S, T] using hEq
1616 have hmemTset :
1617 (x - y) ∈
1619 have hmemSset :
1620 (x - y) ∈
1622 rw [hEqST]
1623 exact hmemTset
1624 exact hmemSset
1626/-- Closedness of `I(ker psi) I(G)` is equivalently the injectivity of the canonical map from
1627the algebraic source augmentation quotient to the closed finite-stage quotient. -/
1633 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1634 (hfopen : IsOpenMap psi) :
1635 IsClosed
1638 Function.Injective
1640 C hC hForm psi hpsi hfopen) := by
1642 C hC hForm psi hpsi hfopen]
1643 exact
1645 C hC hForm psi hpsi hfopen).symm
1647/-- The source Fox boundary, valued in the source augmentation quotient. -/
1649 (psi : ContinuousMonoidHom G H) (g : G) :
1651 Submodule.Quotient.mk
1652zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
1654 C G (MonoidHom.id G) g⟩
1656omit [IsTopologicalGroup H] in
1657/-- The source-boundary map to the source augmentation quotient is a crossed differential for
1658the source completed group algebra. -/
1660 (psi : ContinuousMonoidHom G H) :
1662 (zcCompletedGroupAlgebraScalar C (MonoidHom.id G))
1664 intro g h
1665 have hboundary :=
1667 C G (MonoidHom.id G) g h
1669 change
1670 Submodule.Quotient.mk (p := p)
1672 C G (MonoidHom.id G) (g * h)) =
1673 Submodule.Quotient.mk (p := p)
1675 C G (MonoidHom.id G) g) +
1676 zcCompletedGroupAlgebraScalar C (MonoidHom.id G) g •
1677 Submodule.Quotient.mk (p := p)
1679 C G (MonoidHom.id G) h)
1680 rw [hboundary]
1681 rw [Submodule.Quotient.mk_add, Submodule.Quotient.mk_smul]
1683/-- The source Fox boundary, valued in the closed source augmentation quotient. -/
1689 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1690 (hfopen : IsOpenMap psi) (g : G) :
1691 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen :=
1692 Submodule.Quotient.mk
1693zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
1695 C G (MonoidHom.id G) g⟩
1697@[simp]
1703 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1704 (hfopen : IsOpenMap psi) (g : G) :
1706 C hC hForm psi hpsi hfopen
1709 C hC hForm psi hpsi hfopen g := by
1714/-- The source-boundary map to the closed source augmentation quotient is a crossed
1715differential for the source completed group algebra. -/
1721 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1722 (hfopen : IsOpenMap psi) :
1724 (zcCompletedGroupAlgebraScalar C (MonoidHom.id G))
1726 C hC hForm psi hpsi hfopen) := by
1727 intro g h
1728 have hboundary :=
1730 C G (MonoidHom.id G) g h
1731 let p :=
1733 C hC hForm psi hpsi hfopen
1734 change
1735 Submodule.Quotient.mk (p := p)
1737 C G (MonoidHom.id G) (g * h)) =
1738 Submodule.Quotient.mk (p := p)
1740 C G (MonoidHom.id G) g) +
1741 zcCompletedGroupAlgebraScalar C (MonoidHom.id G) g •
1742 Submodule.Quotient.mk (p := p)
1744 C G (MonoidHom.id G) h)
1745 rw [hboundary]
1746 rw [Submodule.Quotient.mk_add, Submodule.Quotient.mk_smul]
1748/-- The source Fox boundary into the closed source augmentation quotient is continuous. -/
1754 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1755 (hfopen : IsOpenMap psi) :
1756 Continuous
1758 C hC hForm psi hpsi hfopen) := by
1759 have hstd :
1760 Continuous
1762 C G (MonoidHom.id G)) := by
1763 have hval :
1764 Continuous (fun g : G =>
1766 C G (MonoidHom.id G) g : ZCCompletedGroupAlgebra C G)) :=
1768 (C := C) (G := G) (MonoidHom.id G) continuous_id
1769 exact Continuous.subtype_mk hval
1770 (fun g =>
1772 C G (MonoidHom.id G) g).2)
1773 have hq :
1775 (Submodule.Quotient.mk x :
1776 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)) :=
1777 continuous_quotient_mk'
1778 exact hq.comp hstd
1780omit [IsTopologicalGroup H] in
1781/-- Products `(n - 1) s` vanish in the source augmentation quotient. -/
1782@[simp]
1784 (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi)
1786 Submodule.Quotient.mk
1788 ((zcGroupLike C G n.1 - 1) • s) = 0 := by
1789 apply (Submodule.Quotient.mk_eq_zero
1793omit [IsTopologicalGroup H] in
1794/-- Source group-like actions with the same image under `psi` agree on the source augmentation
1795quotient. This is the algebraic descent statement needed before a completed target scalar
1796action can be installed. -/
1798 (psi : ContinuousMonoidHom G H) {g₁ g₂ : G} (h : psi g₁ = psi g₂)
1800 zcGroupLike C G g₁ • x = zcGroupLike C G g₂ • x := by
1801 refine Submodule.Quotient.induction_on
1803 intro y
1804 apply (Submodule.Quotient.eq
1807 ⟨g₂⁻¹ * g₁, by
1808 change psi (g₂⁻¹ * g₁) = 1
1809 rw [map_mul, map_inv, h]
1810 simp only [inv_mul_cancel]⟩
1811 have hgen :
1812 (zcGroupLike C G n.1 - 1) • y ∈
1815 have hmem :
1816 zcGroupLike C G g₂ • ((zcGroupLike C G n.1 - 1) • y) ∈
1819 (zcGroupLike C G g₂) hgen
1820 convert hmem using 1
1821 apply Subtype.ext
1822 change zcGroupLike C G g₁ * (y : ZCCompletedGroupAlgebra C G) -
1824 zcGroupLike C G g₂ *
1825 ((zcGroupLike C G n.1 - 1) * (y : ZCCompletedGroupAlgebra C G))
1826 rw [sub_mul, one_mul, mul_sub, ← mul_assoc, ← map_mul]
1827 simp only [mul_inv_cancel_left, n]
1829omit [IsTopologicalGroup H] in
1830/-- The additive endomorphism of the source augmentation quotient induced by any chosen lift
1831of a target element. -/
1833 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h : H) :
1834 AddMonoid.End (KernelAugmentationIdealQuotient C psi) where
1835 toFun x := zcGroupLike C G (Function.surjInv hpsi h) • x
1836 map_zero' := smul_zero _
1837 map_add' := by
1838 intro x y
1839 rw [smul_add]
1841omit [IsTopologicalGroup H] in
1842@[simp]
1844 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h : H)
1847 C psi hpsi h x =
1848 zcGroupLike C G (Function.surjInv hpsi h) • x :=
1849 rfl
1851omit [IsTopologicalGroup H] in
1852/-- The chosen-lift target action agrees with scalar multiplication by any source lift of
1853the same target element. -/
1855 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) {h : H} {g : G}
1856 (hg : psi g = h) (x : KernelAugmentationIdealQuotient C psi) :
1858 C psi hpsi h x =
1859 zcGroupLike C G g • x := by
1860 have hlift : psi (Function.surjInv hpsi h) = psi g := by
1861 rw [Function.surjInv_eq hpsi h, hg]
1863 C psi hlift x
1865omit [IsTopologicalGroup H] in
1866@[simp]
1868 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
1871 C psi hpsi (1 : H) x = x := by
1872 have hmap : psi (Function.surjInv hpsi (1 : H)) = psi (1 : G) := by
1873 rw [Function.surjInv_eq hpsi (1 : H), map_one]
1874 have hsmul :=
1876 C psi hmap x
1877 simpa using hsmul
1879omit [IsTopologicalGroup H] in
1880/-- The chosen-lift target group-like endomorphisms multiply pointwise on the quotient. -/
1882 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h₁ h₂ : H)
1885 C psi hpsi (h₁ * h₂) x =
1887 C psi hpsi h₁
1889 C psi hpsi h₂ x) := by
1890 let s₁ : G := Function.surjInv hpsi h₁
1891 let s₂ : G := Function.surjInv hpsi h₂
1892 let s₁₂ : G := Function.surjInv hpsi (h₁ * h₂)
1893 have hs : psi s₁₂ = psi (s₁ * s₂) := by
1895 simp only [Function.surjInv_eq hpsi, s₁₂, s₁, s₂]
1896 have hsmul :=
1898 C psi hs x
1899 change zcGroupLike C G s₁₂ • x =
1900 zcGroupLike C G s₁ • (zcGroupLike C G s₂ • x)
1901 rw [← mul_smul]
1902 rw [← (zcGroupLike C G).map_mul s₁ s₂]
1903 exact hsmul
1905omit [IsTopologicalGroup H] in
1906/-- The descended group-like target action on the source augmentation quotient, for a
1907surjective `psi`. -/
1909 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
1910 H →* AddMonoid.End (KernelAugmentationIdealQuotient C psi) where
1911 toFun h :=
1913 C psi hpsi h
1914 map_one' := by
1915 refine AddMonoidHom.ext ?_
1916 intro x
1917 exact
1919 C psi hpsi x
1920 map_mul' h₁ h₂ := by
1921 refine AddMonoidHom.ext ?_
1922 intro x
1923 change
1925 C psi hpsi (h₁ * h₂) x =
1927 C psi hpsi h₁
1929 C psi hpsi h₂ x)
1930 exact
1932 C psi hpsi h₁ h₂ x
1934omit [IsTopologicalGroup H] in
1935@[simp]
1937 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h : H)
1940 C psi hpsi h x =
1941 zcGroupLike C G (Function.surjInv hpsi h) • x :=
1942 rfl
1944omit [IsTopologicalGroup H] in
1945/-- Coefficients from `Z_C` act on the source augmentation quotient through the source
1946completed group algebra. -/
1948 (psi : ContinuousMonoidHom G H) (a : ZCCoeff C) :
1949 AddMonoid.End (KernelAugmentationIdealQuotient C psi) where
1950 toFun x := zcCompletedGroupAlgebraCoeffMap C G a • x
1951 map_zero' := smul_zero _
1952 map_add' := by
1953 intro x y
1954 rw [smul_add]
1956omit [IsTopologicalGroup H] in
1957@[simp]
1959 (psi : ContinuousMonoidHom G H) (a : ZCCoeff C)
1963 rfl
1965omit [IsTopologicalGroup H] in
1966/-- The coefficient action of `Z_C` on the source augmentation quotient. -/
1968 (psi : ContinuousMonoidHom G H) :
1969 ZCCoeff C →+* AddMonoid.End (KernelAugmentationIdealQuotient C psi) where
1971 map_zero' := by
1972 refine AddMonoidHom.ext ?_
1973 intro x
1974 change zcCompletedGroupAlgebraCoeffMap C G (0 : ZCCoeff C) • x = 0
1975 rw [map_zero, zero_smul]
1976 map_one' := by
1977 refine AddMonoidHom.ext ?_
1978 intro x
1979 change zcCompletedGroupAlgebraCoeffMap C G (1 : ZCCoeff C) • x = x
1980 rw [map_one, one_smul]
1981 map_add' a b := by
1982 refine AddMonoidHom.ext ?_
1983 intro x
1984 change zcCompletedGroupAlgebraCoeffMap C G (a + b) • x =
1987 rw [map_add, add_smul]
1988 map_mul' a b := by
1989 refine AddMonoidHom.ext ?_
1990 intro x
1991 change zcCompletedGroupAlgebraCoeffMap C G (a * b) • x =
1994 rw [map_mul, mul_smul]
1996omit [IsTopologicalGroup H] in
1997/-- Coefficient elements are central with respect to group-like elements in `Z_C[[G]]`. -/
1999 (a : ZCCoeff C) (g : G) :
2002 apply Subtype.ext
2003 funext i
2004 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
2005 change
2012 simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.single_mul_single, one_mul,
2016omit [IsTopologicalGroup H] in
2017/-- The algebraic target group algebra `Z_C[H]` acts on the source augmentation quotient. This
2018is the dense algebraic part of the eventual completed `Z_C[[H]]` scalar action. -/
2020 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
2021 MonoidAlgebra (ZCCoeff C) H →+*
2022 AddMonoid.End (KernelAugmentationIdealQuotient C psi) :=
2023 MonoidAlgebra.liftNCRingHom
2026 C psi hpsi)
2027 (by
2028 intro a h
2029 rw [Commute]
2030 apply AddMonoidHom.ext
2031 intro x
2032 change
2034 (zcGroupLike C G (Function.surjInv hpsi h) • x) =
2035 zcGroupLike C G (Function.surjInv hpsi h) •
2037 rw [← mul_smul, ← mul_smul,
2040omit [IsTopologicalGroup H] in
2041@[simp]
2043 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h : H) :
2045 C psi hpsi (MonoidAlgebra.of (ZCCoeff C) H h) =
2047 C psi hpsi h := by
2048 apply AddMonoidHom.ext
2049 intro x
2050 simp only [kerAugQuotTargetGAActionOfSurj, MonoidAlgebra.of_apply, MonoidAlgebra.liftNCRingHom_single,
2051 map_one, one_mul]
2053omit [IsTopologicalGroup H] in
2054/-- The descended algebraic `Z_C[H]`-module structure on the source augmentation quotient. -/
2055noncomputable abbrev
2056 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2057 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
2058 Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2059 Module.compHom (KernelAugmentationIdealQuotient C psi)
2061 C psi hpsi)
2063omit [IsTopologicalGroup H] in
2064@[simp]
2066 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2067 (a : MonoidAlgebra (ZCCoeff C) H) (x : KernelAugmentationIdealQuotient C psi) :
2068 letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2069 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2070 C psi hpsi
2071 a • x =
2073 C psi hpsi a x := by
2074 rfl
2076omit [IsTopologicalGroup H] in
2077@[simp]
2079 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h : H)
2081 letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2082 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2083 C psi hpsi
2084 MonoidAlgebra.of (ZCCoeff C) H h • x =
2085 zcGroupLike C G (Function.surjInv hpsi h) • x := by
2086 letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2087 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2088 C psi hpsi
2089 change
2091 C psi hpsi (MonoidAlgebra.of (ZCCoeff C) H h) x =
2092 zcGroupLike C G (Function.surjInv hpsi h) • x
2094 rfl
2096omit [IsTopologicalGroup H] in
2097/-- The algebraic target group-algebra action by `[h]` agrees with source multiplication by
2098any lift of `h`. -/
2100 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) {h : H} {g : G}
2101 (hg : psi g = h) (x : KernelAugmentationIdealQuotient C psi) :
2102 letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2103 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2104 C psi hpsi
2105 MonoidAlgebra.of (ZCCoeff C) H h • x = zcGroupLike C G g • x := by
2106 letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2107 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2108 C psi hpsi
2110 have hlift : psi (Function.surjInv hpsi h) = psi g := by
2111 rw [Function.surjInv_eq hpsi h, hg]
2113 C psi hlift x
2115omit [IsTopologicalGroup H] in
2116/-- The source boundary is a crossed differential for the descended algebraic target
2117group-algebra coefficients. -/
2119 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
2120 letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2121 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2122 C psi hpsi
2124 ((MonoidAlgebra.of (ZCCoeff C) H).comp psi.toMonoidHom)
2126 letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2127 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2128 C psi hpsi
2129 intro g h
2130 have hsource :=
2132 C psi g h
2133 rw [hsource]
2134 congr 1
2135 exact
2137 C psi hpsi (h := psi g) (g := g) rfl
2140omit [IsTopologicalGroup H] in
2141/-- The algebraic target-coefficient universal differential module maps to the source
2142augmentation quotient by `d g ↦ [g] - 1`. -/
2144 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
2145 letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2146 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2147 C psi hpsi
2148 CrossedDifferentialModule ((MonoidAlgebra.of (ZCCoeff C) H).comp psi.toMonoidHom) →ₗ[
2149 MonoidAlgebra (ZCCoeff C) H] KernelAugmentationIdealQuotient C psi := by
2150 letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2151 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2152 C psi hpsi
2153 exact
2156 ((MonoidAlgebra.of (ZCCoeff C) H).comp psi.toMonoidHom)
2159 C psi hpsi)
2161omit [IsTopologicalGroup H] in
2162@[simp]
2164 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (g : G) :
2165 letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2166 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2167 C psi hpsi
2170 ((MonoidAlgebra.of (ZCCoeff C) H).comp psi.toMonoidHom) g) =
2172 letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
2173 zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
2174 C psi hpsi
2175 exact
2178 ((MonoidAlgebra.of (ZCCoeff C) H).comp psi.toMonoidHom)
2181 C psi hpsi) g
2183omit [IsTopologicalGroup H] in
2184/-- Multiplying an algebraic kernel-augmentation element by a standard augmentation element
2185lands in the algebraic product `I(ker psi) I(G)`. The remaining completed-target descent
2186problem is exactly replacing the first hypothesis by membership in the completed map kernel. -/
2188 (psi : ContinuousMonoidHom G H)
2192 (⟨k * (y : ZCCompletedGroupAlgebra C G),
2197 refine Submodule.span_induction
2198 (p := fun k _ =>
2200 (⟨k * (y : ZCCompletedGroupAlgebra C G),
2203 · rintro _ ⟨n, rfl⟩ y
2205 · intro y
2206 convert S.zero_mem using 1
2207 ext
2208 simp only [zero_mul, zcCompletedGroupAlgebraProjection_zero, Finsupp.coe_zero, Pi.zero_apply,
2209 ZeroMemClass.coe_zero]
2210 · intro a b _ _ ha hb y
2211 have hsum : (⟨a * (y : ZCCompletedGroupAlgebra C G),
2214 (⟨b * (y : ZCCompletedGroupAlgebra C G),
2217 S.add_mem (ha y) (hb y)
2218 convert hsum using 1
2219 ext
2221 MonoidAlgebra.coe_add, Pi.add_apply, AddMemClass.mk_add_mk]
2222 · intro a b _ hb y
2223 have hsmul : a •
2224 (⟨b * (y : ZCCompletedGroupAlgebra C G),
2227 S.smul_mem a (hb y)
2228 convert hsmul using 1
2229 ext
2230 simp only [smul_eq_mul, mul_assoc, zcCompletedGroupAlgebraProjection_mul, SetLike.mk_smul_mk]
2232/-- Under the finite-stage open-map kernel theorem, a completed-kernel scalar times a standard
2233augmentation element lands in the closure of the algebraic product. This is the strongest
2234statement available without proving that the product submodule is closed. -/
2240 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2241 (hfopen : IsOpenMap psi)
2243 (hk : k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi))
2245 (⟨k * (y : ZCCompletedGroupAlgebra C G),
2248 closure
2255 ⟨a * (y : R), (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left a y.2⟩
2256 have hf : Continuous f := by
2257 have hmul : Continuous (fun a : R => a * (y : R)) :=
2258 continuous_id.mul continuous_const
2259 exact Continuous.subtype_mk hmul
2260 (fun a => (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left a y.2)
2261 have hkClosure : k ∈ closure ((I : Set R)) := by
2262 have hEq :=
2264 C hC hForm psi hpsi hfopen
2265 rw [hEq]
2266 exact hk
2267 have hmemImage : f k ∈ f '' closure ((I : Set R)) := ⟨k, hkClosure, rfl
2268 have hclosureImage : f k ∈ closure (f '' ((I : Set R))) :=
2269 image_closure_subset_closure_image hf hmemImage
2270 have himage_subset : f '' ((I : Set R)) ⊆ (S : Set _) := by
2271 rintro _ ⟨a, ha, rfl
2272 exact
2274 C psi ha y
2275 exact closure_mono himage_subset hclosureImage
2277/-- The finite-stage closed form of the completed-kernel product statement. -/
2283 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2284 (hfopen : IsOpenMap psi)
2286 (hk : k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi))
2288 (⟨k * (y : ZCCompletedGroupAlgebra C G),
2292 C hC hForm psi hpsi hfopen := by
2293 have hclosure :=
2295 C hC hForm psi hpsi hfopen hk y
2297 C hC hForm psi hpsi hfopen] at hclosure
2299/-- Completed-kernel scalars send the standard source augmentation ideal into the finite-stage
2300closed hull of `I(ker psi) I(G)`. -/
2306 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2307 (hfopen : IsOpenMap psi) :
2309 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
2311 (⟨k * (y : ZCCompletedGroupAlgebra C G),
2315 C hC hForm psi hpsi hfopen := by
2316 intro k hk y
2317 exact
2319 C hC hForm psi hpsi hfopen hk y
2321/-- If the algebraic product `I(ker psi) I(G)` is closed in the standard augmentation ideal,
2322then completed-kernel scalars send standard augmentation elements into that product. -/
2328 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2329 (hfopen : IsOpenMap psi)
2330 (hclosed :
2331 IsClosed
2335 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
2337 (⟨k * (y : ZCCompletedGroupAlgebra C G),
2341 intro k hk y
2342 have hclosure :=
2344 C hC hForm psi hpsi hfopen hk y
2345 rwa [hclosed.closure_eq] at hclosure
2347/-- If the canonical map from the algebraic source augmentation quotient to the closed
2348finite-stage quotient is injective, then completed-kernel scalars multiply standard augmentation
2349elements into the algebraic product `I(ker psi) I(G)`.
2351This descent step uses finite-stage closed membership and converts it back to algebraic
2352membership through injectivity of the quotient comparison map. -/
2358 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2359 (hfopen : IsOpenMap psi)
2360 (hinj :
2361 Function.Injective
2363 C hC hForm psi hpsi hfopen)) :
2365 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
2367 (⟨k * (y : ZCCompletedGroupAlgebra C G),
2371 intro k hk y
2373 let T :=
2375 C hC hForm psi hpsi hfopen
2377 ⟨k * (y : ZCCompletedGroupAlgebra C G),
2379 have hxT : x ∈ T :=
2381 C hC hForm psi hpsi hfopen hk y
2382 have hxmap :
2384 C hC hForm psi hpsi hfopen
2385 (Submodule.Quotient.mk (p := S) x) = 0 := by
2387 (C := C) (hC := hC) (hForm := hForm) (psi := psi)
2388 (hpsi := hpsi) (hfopen := hfopen) x]
2389 exact (Submodule.Quotient.mk_eq_zero (p := T) (x := x)).2 hxT
2390 have hxzero :
2391 (Submodule.Quotient.mk (p := S) x :
2393 apply hinj
2394 rw [hxmap, map_zero]
2395 exact (Submodule.Quotient.mk_eq_zero (p := S) (x := x)).1 hxzero
2397/-- If every completed-kernel scalar sends the standard source augmentation ideal into
2398`I(ker psi) I(G)`, then the completed kernel acts trivially on the quotient. -/
2400 (hC : ProCGroups.FiniteGroupClass.Hereditary C) (psi : ContinuousMonoidHom G H)
2401 (hker_mul :
2403 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
2405 (⟨k * (y : ZCCompletedGroupAlgebra C G),
2410 (hk : k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi))
2412 k • x = 0 := by
2413 refine Submodule.Quotient.induction_on
2415 intro y
2416 apply (Submodule.Quotient.mk_eq_zero
2418 change
2419 (⟨k * (y : ZCCompletedGroupAlgebra C G),
2423 exact hker_mul k hk y
2425/-- Conditional descent of the source action to a completed target `Z_C[[H]]`-module.
2427The extra hypothesis is exactly the missing kernel-product statement; it is kept explicit so
2428that closure membership is not used as algebraic equality. -/
2434 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
2436 Function.surjInv
2438 (C := C) (hC := hC) hForm psi hpsi)
2440@[simp 900]
2446 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2450 Function.surjInv_eq
2452 (C := C) (hC := hC) hForm psi hpsi) a
2459 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2460 (hker_mul :
2462 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
2464 (⟨k * (y : ZCCompletedGroupAlgebra C G),
2469 letI : SMul (ZCCompletedGroupAlgebra C H)
2472 C hC hForm psi hpsi a • x⟩
2474 (C := C) (hC := hC) hForm psi hpsi).moduleLeft
2476 intro a x
2478 (zcCompletedGroupAlgebraMap C hC psi a) • x =
2479 a • x
2480 have hdiff :
2482 (zcCompletedGroupAlgebraMap C hC psi a) - a ∈
2483 RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) := by
2486 (zcCompletedGroupAlgebraMap C hC psi a) - a) = 0
2488 have hzero :=
2490 C hC psi hker_mul
2492 (zcCompletedGroupAlgebraMap C hC psi a) - a) hdiff x
2493 rw [sub_smul] at hzero
2494 exact sub_eq_zero.mp hzero
2501 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2502 (hfopen : IsOpenMap psi)
2503 (hclosed :
2504 IsClosed
2509 C hC hForm psi hpsi
2511 C hC hForm psi hpsi hfopen hclosed)
2513/-- The completed kernel acts trivially on the closed source augmentation quotient. -/
2519 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2520 (hfopen : IsOpenMap psi)
2522 (hk : k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi))
2523 (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
2524 k • x = 0 := by
2525 refine Submodule.Quotient.induction_on
2527 C hC hForm psi hpsi hfopen) x ?_
2528 intro y
2529 apply (Submodule.Quotient.mk_eq_zero
2531 C hC hForm psi hpsi hfopen)).2
2532 change
2533 (⟨k * (y : ZCCompletedGroupAlgebra C G),
2537 C hC hForm psi hpsi hfopen
2538 exact
2540 C hC hForm psi hpsi hfopen k hk y
2542/-- Unconditional descent of the source action to a completed target `Z_C[[H]]`-module on the
2543closed source augmentation quotient. -/
2549 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2550 (hfopen : IsOpenMap psi) :
2552 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) := by
2553 letI : SMul (ZCCompletedGroupAlgebra C H)
2554 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2556 C hC hForm psi hpsi a • x⟩
2558 (C := C) (hC := hC) hForm psi hpsi).moduleLeft
2560 intro a x
2562 (zcCompletedGroupAlgebraMap C hC psi a) • x =
2563 a • x
2564 have hdiff :
2566 (zcCompletedGroupAlgebraMap C hC psi a) - a ∈
2567 RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) := by
2570 (zcCompletedGroupAlgebraMap C hC psi a) - a) = 0
2572 have hzero :=
2574 C hC hForm psi hpsi hfopen
2576 (zcCompletedGroupAlgebraMap C hC psi a) - a) hdiff x
2577 rw [sub_smul] at hzero
2578 exact sub_eq_zero.mp hzero
2585 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2586 (hfopen : IsOpenMap psi)
2588 (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
2589 letI : Module (ZCCompletedGroupAlgebra C H)
2590 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2592 C hC hForm psi hpsi hfopen
2593 zcCompletedGroupAlgebraMap C hC psi a • x = a • x := by
2594 letI : Module (ZCCompletedGroupAlgebra C H)
2595 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2597 C hC hForm psi hpsi hfopen
2599 (zcCompletedGroupAlgebraMap C hC psi a) • x =
2600 a • x
2601 have hdiff :
2603 (zcCompletedGroupAlgebraMap C hC psi a) - a ∈
2604 RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) := by
2607 (zcCompletedGroupAlgebraMap C hC psi a) - a) = 0
2609 have hzero :=
2611 C hC hForm psi hpsi hfopen
2613 (zcCompletedGroupAlgebraMap C hC psi a) - a) hdiff x
2614 rw [sub_smul] at hzero
2615 exact sub_eq_zero.mp hzero
2617/-- Source scalar multiplication on the closed source augmentation quotient is continuous in the
2618source scalar, for a fixed quotient element. -/
2624 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2625 (hfopen : IsOpenMap psi)
2626 (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
2627 Continuous (fun a : ZCCompletedGroupAlgebra C G => a • x) := by
2628 refine Submodule.Quotient.induction_on
2630 C hC hForm psi hpsi hfopen) x ?_
2631 intro y
2632 have hpre :
2633 Continuous (fun a : ZCCompletedGroupAlgebra C G =>
2634 (⟨a * (y : ZCCompletedGroupAlgebra C G),
2637 have hmul : Continuous (fun a : ZCCompletedGroupAlgebra C G =>
2638 a * (y : ZCCompletedGroupAlgebra C G)) :=
2639 continuous_id.mul continuous_const
2640 exact Continuous.subtype_mk hmul
2641 (fun a => (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left a y.2)
2642 have hq :
2644 (Submodule.Quotient.mk
2646 C hC hForm psi hpsi hfopen) z :
2647 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)) :=
2648 continuous_quotient_mk'
2649 simpa using hq.comp hpre
2651/-- Descended target scalar multiplication on the closed source augmentation quotient is
2652continuous in the target scalar, for a fixed quotient element. -/
2658 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2659 (hfopen : IsOpenMap psi)
2660 (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
2661 letI : Module (ZCCompletedGroupAlgebra C H)
2662 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2664 C hC hForm psi hpsi hfopen
2665 Continuous (fun a : ZCCompletedGroupAlgebra C H => a • x) := by
2666 letI : Module (ZCCompletedGroupAlgebra C H)
2667 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2669 C hC hForm psi hpsi hfopen
2671 have hq : Topology.IsQuotientMap q :=
2673 rw [hq.continuous_iff]
2674 change Continuous (fun a : ZCCompletedGroupAlgebra C G => q a • x)
2675 have hsource :=
2677 C hC hForm psi hpsi hfopen x
2678 have hEq :
2679 (fun a : ZCCompletedGroupAlgebra C G => q a • x) =
2680 (fun a : ZCCompletedGroupAlgebra C G => a • x) := by
2681 funext a
2682 exact
2684 C hC hForm psi hpsi hfopen a x
2685 simpa [hEq] using hsource
2687/-- Source scalar multiplication on the closed source augmentation quotient is jointly
2688continuous. -/
2694 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2695 (hfopen : IsOpenMap psi) :
2696 Continuous (fun p : ZCCompletedGroupAlgebra C G ×
2697 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen =>
2698 p.1 • p.2) := by
2699 let S :=
2701 C hC hForm psi hpsi hfopen
2702 have hquot :
2703 IsOpenQuotientMap
2706 (Submodule.Quotient.mk (p := S) z :
2707 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen))) :=
2708 IsOpenQuotientMap.id.prodMap S.isOpenQuotientMap_mkQ
2709 rw [← hquot.continuous_comp_iff]
2710 have hpre :
2711 Continuous (fun p : ZCCompletedGroupAlgebra C G ×
2713 (⟨p.1 * (p.2 : ZCCompletedGroupAlgebra C G),
2714 (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left p.1 p.2.2⟩ :
2716 have hmul : Continuous (fun p : ZCCompletedGroupAlgebra C G ×
2718 p.1 * (p.2 : ZCCompletedGroupAlgebra C G)) :=
2719 continuous_fst.mul (continuous_subtype_val.comp continuous_snd)
2720 exact Continuous.subtype_mk hmul
2721 (fun p => (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left p.1 p.2.2)
2722 have hmk :
2724 (Submodule.Quotient.mk (p := S) z :
2725 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)) :=
2726 continuous_quotient_mk'
2727 simpa [Function.comp_def, Prod.map, S] using hmk.comp hpre
2729/-- Descended target scalar multiplication on the closed source augmentation quotient is jointly
2730continuous. -/
2736 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2737 (hfopen : IsOpenMap psi) :
2738 letI : Module (ZCCompletedGroupAlgebra C H)
2739 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2741 C hC hForm psi hpsi hfopen
2742 Continuous (fun p : ZCCompletedGroupAlgebra C H ×
2743 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen =>
2744 p.1 • p.2) := by
2745 letI : Module (ZCCompletedGroupAlgebra C H)
2746 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2748 C hC hForm psi hpsi hfopen
2750 have hq : IsOpenQuotientMap q :=
2752 have hquot :
2753 IsOpenQuotientMap
2754 (Prod.map q
2755 (id :
2756 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen →
2757 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)) :=
2758 hq.prodMap IsOpenQuotientMap.id
2759 rw [← hquot.continuous_comp_iff]
2760 have hsource :=
2762 C hC hForm psi hpsi hfopen
2763 have hEq :
2765 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen =>
2766 q p.1 • p.2) =
2768 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen =>
2769 p.1 • p.2) := by
2770 funext p
2771 exact
2773 C hC hForm psi hpsi hfopen p.1 p.2
2774 simpa [Function.comp_def, Prod.map, hEq] using hsource
2776/-- The closed source augmentation quotient is a topological module for the source completed
2777group algebra. -/
2783 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2784 (hfopen : IsOpenMap psi) :
2785 ContinuousSMul (ZCCompletedGroupAlgebra C G)
2786 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) where
2787 continuous_smul :=
2789 C hC hForm psi hpsi hfopen
2791/-- The descended target module structure on the closed source augmentation quotient is
2792topological. -/
2798 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2799 (hfopen : IsOpenMap psi) :
2800 letI : Module (ZCCompletedGroupAlgebra C H)
2801 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2803 C hC hForm psi hpsi hfopen
2804 ContinuousSMul (ZCCompletedGroupAlgebra C H)
2805 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) := by
2806 letI : Module (ZCCompletedGroupAlgebra C H)
2807 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2809 C hC hForm psi hpsi hfopen
2810 exact
2812 C hC hForm psi hpsi hfopen⟩
2819 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2820 (hfopen : IsOpenMap psi)
2821 (g : G) (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
2822 letI : Module (ZCCompletedGroupAlgebra C H)
2823 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2825 C hC hForm psi hpsi hfopen
2826 zcGroupLike C H (psi g) • x = zcGroupLike C G g • x := by
2827 letI : Module (ZCCompletedGroupAlgebra C H)
2828 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2830 C hC hForm psi hpsi hfopen
2831 rw [← zcCompletedGroupAlgebraMap_groupLike (C := C) (hC := hC) psi g]
2832 exact
2834 C hC hForm psi hpsi hfopen (zcGroupLike C G g) x
2836/-- The source boundary to the closed source augmentation quotient is a crossed differential
2837for the descended completed target scalars. -/
2843 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2844 (hfopen : IsOpenMap psi) :
2845 letI : Module (ZCCompletedGroupAlgebra C H)
2846 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2848 C hC hForm psi hpsi hfopen
2852 C hC hForm psi hpsi hfopen) := by
2853 letI : Module (ZCCompletedGroupAlgebra C H)
2854 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2856 C hC hForm psi hpsi hfopen
2857 intro g h
2858 have hsource :=
2860 C hC hForm psi hpsi hfopen g h
2861 rw [hsource]
2862 congr 1
2863 change zcGroupLike C G g •
2865 C hC hForm psi hpsi hfopen h =
2866 zcGroupLike C H (psi g) •
2868 C hC hForm psi hpsi hfopen h
2869 exact
2871 C hC hForm psi hpsi hfopen g
2873 C hC hForm psi hpsi hfopen h)).symm
2875/-- Projecting a chosen completed source lift of a target coefficient to a source stage and then
2876passing to the open-image stage recovers the corresponding target finite-stage projection. -/
2882 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2883 (hfopen : IsOpenMap psi)
2890 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i) a := by
2892 have hsource :
2893 (i.1,
2894 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
2895 (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)) ≤ i :=
2896 ⟨le_rfl, zcCompletedGroupAlgebraOpenImage_comapIndex_le C hC hForm psi hpsi hfopen i⟩
2897 have hstage :
2904 exact congrFun
2905 (congrArg DFunLike.coe
2907 C hC hForm psi hpsi hfopen i))
2910 change
2914 ((zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i).1,
2915 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
2916 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i).2) b) =
2919 have hprojmap :=
2921 (C := C) (hC := hC) (H := G) (K := H) (φ := psi)
2922 (i := zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i)
2923 (x := b)
2924 have hmap : zcCompletedGroupAlgebraMap C hC psi b = a := by
2925 dsimp [b]
2927 have hmain :
2932 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i) a :=
2933 congrArg
2936 hmap
2937 exact hprojmap.symm.trans hmain
2939/-- The `i`-th closed augmentation quotient coordinate of the completed source-boundary lift
2940factors through the corresponding open-image finite pre-stage. -/
2946 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
2947 (hfopen : IsOpenMap psi)
2950 letI : Module (ZCCompletedGroupAlgebra C H)
2951 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2953 C hC hForm psi hpsi hfopen
2955 C hC hForm psi hpsi hfopen i
2959 C hC hForm psi hpsi hfopen) x) =
2961 C hC hForm psi hpsi hfopen i
2963 (zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i) x) := by
2964 letI : Module (ZCCompletedGroupAlgebra C H)
2965 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
2967 C hC hForm psi hpsi hfopen
2968 let j := zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i
2969 letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
2970 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
2972 C hC hForm psi hpsi hfopen i
2973 letI : Module
2976 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
2978 C hC hForm psi hpsi hfopen i
2979 refine Finsupp.induction_linear x ?zero ?add ?single
2980 · simp only [crossedDifferentialModuleLiftLinear, map_zero, ContinuousMonoidHom.coe_toMonoidHom,
2983 · intro x y hx hy
2984 simp only [map_add, hx, ContinuousMonoidHom.coe_toMonoidHom, Lean.Elab.WF.paramLet, hy]
2985 · intro g a
2990 have htarget :
2992 C hC hForm psi hpsi hfopen g =
2994 C hC hForm psi hpsi hfopen g := by
2995 rfl
2996 rw [htarget]
2997 change
2999 C hC hForm psi hpsi hfopen i
3001 C hC hForm psi hpsi hfopen g) =
3003 (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i) a •
3005 C hC hForm psi hpsi hfopen i
3007 rw [map_smulₛₗ]
3009 C hC hForm psi hpsi hfopen i a]
3011 (C := C) (hC := hC) (hForm := hForm) (psi := psi)
3012 (hpsi := hpsi) (hfopen := hfopen) (i := i)
3015 C hC hForm psi hpsi hfopen i
3017 have hstage_boundary :
3019 C hC hForm psi hpsi hfopen i
3021 C hC hForm psi hpsi hfopen g) =
3023 C hC hForm psi hpsi hfopen i
3027zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
3029 C G (MonoidHom.id G) g⟩
3030 change
3032 C hC hForm psi hpsi hfopen i
3033 (Submodule.Quotient.mk
3035 C hC hForm psi hpsi hfopen) s) =
3037 C hC hForm psi hpsi hfopen i
3039 let T :=
3041 C hC hForm psi hpsi hfopen i
3042 calc
3044 C hC hForm psi hpsi hfopen i
3045 (Submodule.Quotient.mk
3047 C hC hForm psi hpsi hfopen) s) =
3048 (Submodule.Quotient.mk
3049 (p := T)
3051 KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) := by
3052 exact
3054 C hC hForm psi hpsi hfopen i s
3055 _ =
3057 C hC hForm psi hpsi hfopen i
3059 apply congrArg (fun y : zcCompletedGroupAlgebraStageAugmentationIdeal C G i =>
3060 (Submodule.Quotient.mk (p := T) y :
3061 KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i))
3062 apply Subtype.ext
3067 ContinuousMonoidHom.coe_toMonoidHom, zcCompletedDifferentialModuleOpenImageIndex,
3068 zcCompletedDifferentialModuleStageSourceProj, QuotientGroup.mk'_apply, s, j]
3069 rw [hstage_boundary]
3070 rfl
3072/-- Each finite closed-augmentation coordinate of the pre-quotient source-boundary lift is
3073continuous for the finite-stage pre-module topology. -/
3079 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
3080 (hfopen : IsOpenMap psi)
3082 letI : Module (ZCCompletedGroupAlgebra C H)
3083 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
3085 C hC hForm psi hpsi hfopen
3086 @Continuous
3088 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i)
3090 inferInstance
3091 (fun x =>
3093 C hC hForm psi hpsi hfopen i
3097 C hC hForm psi hpsi hfopen) x)) := by
3098 letI : Module (ZCCompletedGroupAlgebra C H)
3099 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
3101 C hC hForm psi hpsi hfopen
3102 let j := zcCompletedDifferentialModuleOpenImageIndex C hC hForm psi hpsi hfopen i
3103 letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
3104 (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
3106 C hC hForm psi hpsi hfopen i
3107 letI : TopologicalSpace
3110 letI : TopologicalSpace
3114
3115 letI : DiscreteTopology
3119rfl
3120 have hpre :
3121 @Continuous
3127 inferInstance
3130 C psi.toMonoidHom j
3131 have hfinite :
3132 Continuous
3134 C hC hForm psi hpsi hfopen i) :=
3135 continuous_of_discreteTopology
3136 have hfactor :
3139 C hC hForm psi hpsi hfopen i
3143 C hC hForm psi hpsi hfopen) x)) =
3144 fun x =>
3146 C hC hForm psi hpsi hfopen i
3147 (zcCompletedDifferentialModulePreStageMap C psi.toMonoidHom j x) := by
3148 funext x
3149 exact
3151 C hC hForm psi hpsi hfopen i x
3152 rw [hfactor]
3153 exact hfinite.comp hpre
3155/-- The pre-quotient source-boundary lift to the closed source augmentation quotient is
3156continuous for the finite-stage pre-module topology. -/
3162 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
3163 (hfopen : IsOpenMap psi) :
3164 letI : Module (ZCCompletedGroupAlgebra C H)
3165 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
3167 C hC hForm psi hpsi hfopen
3168 @Continuous
3170 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
3172 inferInstance
3176 C hC hForm psi hpsi hfopen)) := by
3177 letI : Module (ZCCompletedGroupAlgebra C H)
3178 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
3180 C hC hForm psi hpsi hfopen
3181 letI : TopologicalSpace
3185 C hC hForm psi hpsi hfopen]
3186 rw [continuous_induced_rng]
3187 exact continuous_pi fun i =>
3189 C hC hForm psi hpsi hfopen i
3191/-- The separated universal differential is also a crossed differential for source completed
3192group-algebra scalars after restricting scalars along `Z_C[[G]] -> Z_C[[H]]`. -/
3197 (psi : ContinuousMonoidHom G H) :
3198 letI : Module (ZCCompletedGroupAlgebra C G)
3200 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3202 (zcCompletedGroupAlgebraScalar C (MonoidHom.id G))
3203 (zcSeparatedUniversalDifferential C psi.toMonoidHom) := by
3204 letI : Module (ZCCompletedGroupAlgebra C G)
3206 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3207 intro g h
3209 congr 1
3210 change zcGroupLike C H (psi g) •
3216/-- The source-identity completed differential module maps to the separated module for `psi`
3217by `d g ↦ d_sep g`, with source scalars restricted through `Z_C[[G]] -> Z_C[[H]]`. -/
3222 (psi : ContinuousMonoidHom G H) :
3223 letI : Module (ZCCompletedGroupAlgebra C G)
3225 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3228 letI : Module (ZCCompletedGroupAlgebra C G)
3230 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3231 exact
3234 C (MonoidHom.id G)
3238@[simp]
3243 (psi : ContinuousMonoidHom G H) (g : G) :
3245 (zcUniversalDifferential C (MonoidHom.id G) g) =
3246 zcSeparatedUniversalDifferential C psi.toMonoidHom g := by
3247 letI : Module (ZCCompletedGroupAlgebra C G)
3249 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3250 exact
3253 C (MonoidHom.id G)
3257/-- The finite source-identity coefficient map agrees with first projecting a completed
3258source coefficient down to the source-identity stage and then applying the finite target map. -/
3261 (psi : ContinuousMonoidHom G H)
3262 (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :
3263 let sourceIndex : ZCCompletedGroupAlgebraIndex C G :=
3264 (i.target.1, completedGroupAlgebraComapIndexInClass
3265 (G := G) (H := H) C hC psi i.target.2)
3266 let idIndex := zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i
3267 let hle : sourceIndex ≤ idIndex.target := by
3268 constructor
3269 exact le_rfl
3270 exact i.compatible
3271 ∀ x : ZCCompletedGroupAlgebraStage C G idIndex.target,
3275 intro sourceIndex idIndex hle x
3276 refine MonoidAlgebra.induction_on
3277 (p := fun x : ZCCompletedGroupAlgebraStage C G idIndex.target =>
3281 x ?single ?add ?smul
3282 · intro q
3283 refine QuotientGroup.induction_on q ?_
3284 intro g
3286 dsimp [sourceIndex, idIndex]
3288 change MonoidAlgebra.single
3289 ((completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC psi i.target.2)
3290 ((OpenNormalSubgroupInClass.map (C := C) (G := G)
3291 (U := OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
3292 (G := G) (H := H) C hC psi i.target.2))
3293 (V := i.source) i.compatible)
3294 (QuotientGroup.mk' (i.source.1 : Subgroup G) g))) 1 =
3295 MonoidAlgebra.mapDomain (zcCompletedDifferentialModuleStagePsi C psi.toMonoidHom i)
3296 (Finsupp.single (QuotientGroup.mk' (i.source.1 : Subgroup G) g) 1)
3297 rw [MonoidAlgebra.mapDomain_single]
3298 dsimp [OpenNormalSubgroupInClass.map]
3299 change MonoidAlgebra.single
3300 ((completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC psi i.target.2)
3301 (QuotientGroup.mk'
3302 ((((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
3303 (G := G) (H := H) C hC psi i.target.2)).1 :
3304 OpenNormalSubgroup G) : Subgroup G)) g)) 1 =
3305 MonoidAlgebra.single
3307 (QuotientGroup.mk' (i.source.1 : Subgroup G) g)) 1
3308 rw [completedGroupAlgebraComapQuotientMapInClass_mk]
3309 change MonoidAlgebra.single (QuotientGroup.mk'
3310 ((((OrderDual.ofDual i.target.2).1 : OpenNormalSubgroup H) : Subgroup H))
3311 (psi g)) 1 =
3312 MonoidAlgebra.single
3313 ((QuotientGroup.map (i.source.1 : Subgroup G)
3314 ((((OrderDual.ofDual i.target.2).1 : OpenNormalSubgroup H) : Subgroup H))
3315 psi.toMonoidHom i.compatible)
3316 (QuotientGroup.mk' (i.source.1 : Subgroup G) g)) 1
3317 rw [QuotientGroup.map_mk']
3318 rfl
3319 · intro x y hx hy
3320 simp only [ContinuousMonoidHom.coe_toMonoidHom, map_add, hx,
3322 · intro r x hx
3323 rcases ZMod.intCast_surjective r with ⟨t, rfl
3324 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
3325 simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedGroupAlgebraMapStage,
3330/-- Completed source coefficients viewed at the identity-source stage agree with target
3331finite projections after applying the completed group-algebra map. -/
3334 (psi : ContinuousMonoidHom G H)
3339 (zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i).target a) =
3341 (zcCompletedGroupAlgebraMap C hC psi a) := by
3342 let sourceIndex : ZCCompletedGroupAlgebraIndex C G :=
3343 (i.target.1, completedGroupAlgebraComapIndexInClass
3344 (G := G) (H := H) C hC psi i.target.2)
3345 let idIndex := zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i
3346 have hle : sourceIndex ≤ idIndex.target := by
3347 constructor
3348 exact le_rfl
3349 exact i.compatible
3352 C hC psi i (zcCompletedGroupAlgebraProjection C G idIndex.target a)]
3355/-- Finite-stage projections of the identity-source lift to the separated `ψ`-module are
3356computed by first projecting to the matching source-identity finite stage. -/
3361 (psi : ContinuousMonoidHom G H)
3363 (x : ZCCompletedDifferentialModule C (MonoidHom.id G)) :
3369 letI : Module (ZCCompletedGroupAlgebra C G)
3371 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3372 letI : Module (ZCCompletedGroupAlgebra C G)
3373 (ZCCompletedDifferentialModuleStage C psi.toMonoidHom i) :=
3374 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3375 let idIndex := zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i
3376 letI : Module
3377 (zcCompletedDifferentialModuleStageRing C (MonoidHom.id G) idIndex)
3378 (ZCCompletedDifferentialModuleStage C psi.toMonoidHom i) :=
3379 Module.compHom _ (zcCompletedDifferentialModuleIdentitySourceStageRingHom C psi.toMonoidHom i)
3380 let L :
3383 { toFun := fun x =>
3386 map_add' := by
3387 intro x y
3389 map_smul' := by
3390 intro a x
3392 change
3396 C hC psi x) =
3400 C hC psi x)
3401 rw [map_smul] }
3402 let R :
3405 { toFun := fun x =>
3409 map_add' := by
3410 intro x y
3412 map_smul' := by
3413 intro a x
3415 change
3418 idIndex.target a •
3420 idIndex x) =
3425 idIndex x)
3427 change
3429 (zcCompletedGroupAlgebraProjection C G idIndex.target a) •
3432 idIndex x) =
3437 idIndex x)
3439 have hLR : L = R := by
3441 intro g
3442 change
3445 (zcUniversalDifferential C (MonoidHom.id G) g)) =
3448 idIndex (zcUniversalDifferential C (MonoidHom.id G) g))
3451 calc
3454 (zcUniversalDifferential C psi.toMonoidHom g) := by
3456 _ =
3459 idIndex (zcUniversalDifferential C (MonoidHom.id G) g)) := by
3460 exact
3462 C psi.toMonoidHom i g).symm
3463 exact LinearMap.congr_fun hLR x
3465/-- The finite comparison from the source-identity stage to the `ψ`-stage commutes with
3466the finite Fox boundary. -/
3468 (ψ : G →* H)
3478 letI : Module (zcCompletedDifferentialModuleStageRing C (MonoidHom.id G) j)
3481 letI : Module (zcCompletedDifferentialModuleStageRing C (MonoidHom.id G) j)
3484 let ringMapLinear :
3485 zcCompletedDifferentialModuleStageRing C (MonoidHom.id G) j →ₗ[
3489 map_add' := by
3490 intro a b
3492 map_smul' := by
3493 intro a b
3494 change
3499 let L :
3500 ZCCompletedDifferentialModuleStage C (MonoidHom.id G) j →ₗ[
3503 toFun := fun x =>
3506 map_add' := by
3507 intro x y
3509 map_smul' := by
3510 intro a x
3512 change
3519 rw [map_smul] }
3520 let R :
3521 ZCCompletedDifferentialModuleStage C (MonoidHom.id G) j →ₗ[
3524 ringMapLinear.comp
3526 have hLR : L = R := by
3528 (coeff := zcCompletedDifferentialModuleStageScalar C (MonoidHom.id G) j)
3529 intro q
3530 change
3534 (zcCompletedDifferentialModuleStageScalar C (MonoidHom.id G) j) q)) =
3540 have hboundaryTarget :
3547 have hboundarySource :
3551 zcCompletedDifferentialModuleStageScalar C (MonoidHom.id G) j q - 1 := by
3554 rw [hboundaryTarget, hboundarySource]
3555 rw [map_sub, map_one,
3557 exact LinearMap.congr_fun hLR x
3559omit [IsTopologicalGroup H] in
3560/-- Applying the finite identity boundary after the source-identity finite projection recovers
3561the finite projection of the standard augmentation-valued completed Fox tail. -/
3565 (psi : ContinuousMonoidHom G H)
3567 (x : ZCCompletedDifferentialModule C (MonoidHom.id G)) :
3572 (zcToStdAugIdeal C G (MonoidHom.id G) x) :
3575 intro j
3576 have hcomp := congrArg (fun f => f x)
3578 C (MonoidHom.id G) j)
3579 simpa [LinearMap.comp_apply,
3582/-- The identity-source lift to the separated `ψ`-module kills the kernel of the standard
3583augmentation-valued completed Fox tail. -/
3588 (psi : ContinuousMonoidHom G H)
3589 (x : ZCCompletedDifferentialModule C (MonoidHom.id G))
3590 (hx :
3591 zcToStdAugIdeal C G (MonoidHom.id G) x = 0) :
3593 have hxFox : zcToCompletedGroupAlgebra C (MonoidHom.id G) x = 0 := by
3594 have hxval :=
3595 congrArg
3598 simpa [zcToStdAugIdeal_val] using hxval
3600 intro i
3602 have hsource :
3606 C psi.toMonoidHom i x hxFox
3607 rw [hsource, map_zero]
3609omit [IsTopologicalGroup G] in
3610/-- The standard-augmentation-valued completed Fox tail is continuous for the finite-stage
3611natural topology on the completed differential module. -/
3615 (psi : ContinuousMonoidHom G H) :
3616 @Continuous
3620 inferInstance
3621 (zcToStdAugIdeal C H psi.toMonoidHom) := by
3622 letI : TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
3624 have hval :
3625 @Continuous
3629 inferInstance
3630 (fun x =>
3632 C H psi.toMonoidHom x : ZCCompletedGroupAlgebra C H)) := by
3635 exact Continuous.subtype_mk hval
3637 C H psi.toMonoidHom x).2)
3639/-- Kernel group-like source scalars act trivially on the separated module after scalar
3640restriction along `Z_C[[G]] -> Z_C[[H]]`. -/
3645 (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi)
3647 letI : Module (ZCCompletedGroupAlgebra C G)
3649 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3650 zcGroupLike C G n.1 • x = x := by
3651 letI : Module (ZCCompletedGroupAlgebra C G)
3653 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3654 change zcCompletedGroupAlgebraMap C hC psi (zcGroupLike C G n.1) • x = x
3656 have hn : psi n.1 = 1 := by
3657 exact MonoidHom.mem_ker.mp
3658 (show n.1 ∈ psi.toMonoidHom.ker from n.2)
3659 rw [hn]
3660 simp only [ContinuousMonoidHom.coe_toMonoidHom, map_one, one_smul]
3662/-- Source scalar restriction on the separated module is exactly target scalar multiplication
3663after applying the completed group-algebra map. -/
3668 (psi : ContinuousMonoidHom G H)
3671 letI : Module (ZCCompletedGroupAlgebra C G)
3673 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3674 zcCompletedGroupAlgebraMap C hC psi a • x = a • x := by
3675 letI : Module (ZCCompletedGroupAlgebra C G)
3677 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3678 rfl
3680/-- Kernel augmentation generators annihilate the separated module under source scalar
3681restriction. -/
3686 (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi)
3688 letI : Module (ZCCompletedGroupAlgebra C G)
3690 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3691 (zcGroupLike C G n.1 - 1) • x = 0 := by
3692 letI : Module (ZCCompletedGroupAlgebra C G)
3694 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3695 calc
3696 (zcGroupLike C G n.1 - 1) • x =
3697 zcGroupLike C G n.1 • x - x := by
3698 rw [sub_smul, one_smul]
3699 _ = 0 := by
3701 simp only [ContinuousMonoidHom.coe_toMonoidHom, sub_self]
3703/-- The identity-source lift to the separated module kills source kernel augmentation
3704generators after scalar multiplication. -/
3709 (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi)
3710 (x : ZCCompletedDifferentialModule C (MonoidHom.id G)) :
3712 ((zcGroupLike C G n.1 - 1) • x) = 0 := by
3713 letI : Module (ZCCompletedGroupAlgebra C G)
3715 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3717 exact
3719 C hC psi n
3721 C hC psi x)
3723/-- A conditional source-standard-augmentation map to the separated module. The only remaining
3724well-definedness input is that the identity Fox tail kernel is killed by the source-identity
3725lift to the separated module. -/
3726noncomputable def
3727 stdAugIdealToZCSepDiffOfBoundaryKernel
3731 (psi : ContinuousMonoidHom G H)
3732 (hker :
3733 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
3734 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
3736 C hC psi x = 0) :
3737 letI : Module (ZCCompletedGroupAlgebra C G)
3739 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3742 letI : Module (ZCCompletedGroupAlgebra C G)
3744 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3745 let f :=
3746 zcToStdAugIdeal C G (MonoidHom.id G)
3747 let L :=
3749 have hf : Function.Surjective f := by
3750 exact
3752 C G (MonoidHom.id G) (fun g => ⟨g, rfl⟩)
3753 have hker_le : LinearMap.ker f ≤ LinearMap.ker L := by
3754 intro x hx
3755 rw [LinearMap.mem_ker] at hx ⊢
3756 exact hker x hx
3757 exact
3758 ((LinearMap.ker f).liftQ L hker_le).comp
3759 (f.quotKerEquivOfSurjective hf).symm.toLinearMap
3761/-- The source-standard-augmentation map to the separated module. -/
3762noncomputable def
3763 stdAugIdealToZCSepDiff
3767 (psi : ContinuousMonoidHom G H) :
3768 letI : Module (ZCCompletedGroupAlgebra C G)
3770 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3773 stdAugIdealToZCSepDiffOfBoundaryKernel
3774 C hC psi
3776 C hC psi)
3778@[simp 900]
3779theorem
3780 stdAugIdealToZCSepDiffOfBoundaryKernel_comp_zcToStdAugIdeal
3784 (psi : ContinuousMonoidHom G H)
3785 (hker :
3786 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
3787 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
3789 C hC psi x = 0) :
3790 letI : Module (ZCCompletedGroupAlgebra C G)
3792 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3793 (stdAugIdealToZCSepDiffOfBoundaryKernel
3794 C hC psi hker).comp
3795 (zcToStdAugIdeal C G (MonoidHom.id G)) =
3797 letI : Module (ZCCompletedGroupAlgebra C G)
3799 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3800 let f :=
3801 zcToStdAugIdeal C G (MonoidHom.id G)
3802 let L :=
3804 have hf : Function.Surjective f := by
3805 exact
3807 C G (MonoidHom.id G) (fun g => ⟨g, rfl⟩)
3808 have hker_le : LinearMap.ker f ≤ LinearMap.ker L := by
3809 intro x hx
3810 rw [LinearMap.mem_ker] at hx ⊢
3811 exact hker x hx
3812 apply LinearMap.ext
3813 intro x
3814 change
3815 (((LinearMap.ker f).liftQ L hker_le).comp
3816 (f.quotKerEquivOfSurjective hf).symm.toLinearMap).comp f x = L x
3817 rw [LinearMap.comp_apply, LinearMap.comp_apply]
3818 have hsymm :
3819 (f.quotKerEquivOfSurjective hf).symm.toLinearMap (f x) =
3820 Submodule.Quotient.mk x := by
3821 exact LinearMap.quotKerEquivOfSurjective_symm_apply (f := f) hf x
3822 rw [hsymm, Submodule.liftQ_apply]
3824@[simp]
3825theorem
3826 stdAugIdealToZCSepDiff_comp_zcToStdAugIdeal
3830 (psi : ContinuousMonoidHom G H) :
3831 letI : Module (ZCCompletedGroupAlgebra C G)
3833 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3834 (stdAugIdealToZCSepDiff
3835 C hC psi).comp
3836 (zcToStdAugIdeal C G (MonoidHom.id G)) =
3838 exact
3839 stdAugIdealToZCSepDiffOfBoundaryKernel_comp_zcToStdAugIdeal
3840 C hC psi
3842 C hC psi)
3844/-- Finite-stage boundary formula for the source-standard map into the separated module. -/
3845theorem
3846 stdAugIdealToZCSepDiff_stageBoundary_stageProj
3850 (psi : ContinuousMonoidHom G H)
3855 (stdAugIdealToZCSepDiff
3856 C hC psi s)) =
3859 (s : ZCCompletedGroupAlgebra C G)) := by
3860 letI : Module (ZCCompletedGroupAlgebra C G)
3862 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3863 let f :=
3864 zcToStdAugIdeal C G (MonoidHom.id G)
3865 let M :=
3866 stdAugIdealToZCSepDiff
3867 C hC psi
3868 let L :=
3870 have hf : Function.Surjective f := by
3871 exact
3873 C G (MonoidHom.id G) (fun g => ⟨g, rfl⟩)
3874 rcases hf s with ⟨x, hx⟩
3875 rw [← hx]
3876 have hcomp :=
3877 congrArg (fun F => F x)
3878 (stdAugIdealToZCSepDiff_comp_zcToStdAugIdeal
3879 C hC psi)
3880 change M (f x) = L x at hcomp
3881 rw [hcomp]
3885 let idIndex := zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i
3886 have hmap :=
3888 C hC psi i (f x : ZCCompletedGroupAlgebra C G)
3889 simpa [f, idIndex] using hmap
3891/-- The finite-stage projection of the source-standard map depends only on the matching
3892source-identity finite projection of the standard augmentation ideal. -/
3893theorem
3894 stdAugIdealToZCSepDiff_stageProj_eq_of_standardProj_eq
3898 (psi : ContinuousMonoidHom G H)
3901 (hst :
3905 (zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i).target t) :
3907 (stdAugIdealToZCSepDiff
3908 C hC psi s) =
3910 (stdAugIdealToZCSepDiff
3911 C hC psi t) := by
3912 letI : Module (ZCCompletedGroupAlgebra C G)
3914 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
3915 let f :=
3916 zcToStdAugIdeal C G (MonoidHom.id G)
3917 let M :=
3918 stdAugIdealToZCSepDiff
3919 C hC psi
3920 let L :=
3922 let idIndex := zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i
3923 have hf : Function.Surjective f := by
3924 exact
3926 C G (MonoidHom.id G) (fun g => ⟨g, rfl⟩)
3927 rcases hf s with ⟨x, hx⟩
3928 rcases hf t with ⟨y, hy⟩
3929 have hxyProjection :
3932 simpa [idIndex, hx, hy] using hst
3933 have hcomp_x :=
3934 congrArg (fun F => F x)
3935 (stdAugIdealToZCSepDiff_comp_zcToStdAugIdeal
3936 C hC psi)
3937 have hcomp_y :=
3938 congrArg (fun F => F y)
3939 (stdAugIdealToZCSepDiff_comp_zcToStdAugIdeal
3940 C hC psi)
3941 change M (f x) = L x at hcomp_x
3942 change M (f y) = L y at hcomp_y
3943 rw [← hx, ← hy, hcomp_x, hcomp_y]
3946 have hsource :
3947 zcCompletedDifferentialModuleStageProjection C (MonoidHom.id G) idIndex x =
3948 zcCompletedDifferentialModuleStageProjection C (MonoidHom.id G) idIndex y := by
3949 apply sub_eq_zero.mp
3950 have hzero :
3951 zcCompletedDifferentialModuleStageProjection C (MonoidHom.id G) idIndex (x - y) = 0 :=
3953 C psi.toMonoidHom i (x - y) (by
3954 rw [map_sub]
3955 rw [map_sub]
3958 rw [hxyProjection, sub_self])
3959 simpa [map_sub] using hzero
3960 rw [hsource]
3962/-- Each finite-stage coordinate of the source-standard map into the separated module is
3963continuous. The coordinate factors through the matching finite standard augmentation
3964projection. -/
3965theorem
3966 continuous_stdAugIdealToZCSepDiff_stageProj
3970 (psi : ContinuousMonoidHom G H)
3971 (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :
3972 Continuous
3975 (stdAugIdealToZCSepDiff
3976 C hC psi s)) := by
3977 let idIndex := zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i
3978 let p :=
3980 have hsurj : Function.Surjective p :=
3983 ZCCompletedDifferentialModuleStage C psi.toMonoidHom i := fun y =>
3985 (stdAugIdealToZCSepDiff
3986 C hC psi (Classical.choose (hsurj y)))
3987 have hfactor :
3990 (stdAugIdealToZCSepDiff
3991 C hC psi s)) =
3992 fun s => F (p s) := by
3993 funext s
3994 exact
3995 stdAugIdealToZCSepDiff_stageProj_eq_of_standardProj_eq
3996 C hC psi i
3997 (by
3998 dsimp [p, F]
3999 exact (Classical.choose_spec (hsurj (p s))).symm)
4000 rw [hfactor]
4001 haveI : DiscreteTopology (zcCompletedGroupAlgebraStageAugmentationIdeal C G idIndex.target) := by
4002 infer_instance
4003 have hF : Continuous F :=
4004 continuous_of_discreteTopology
4007/-- The product of all finite-stage coordinates of the source-standard map into the separated
4008module is continuous. -/
4009theorem
4010 continuous_stdAugIdealToZCSepDiff_stageProjProduct
4014 (psi : ContinuousMonoidHom G H) :
4015 Continuous
4018 (stdAugIdealToZCSepDiff
4019 C hC psi s)) := by
4020 exact continuous_pi fun i =>
4021 continuous_stdAugIdealToZCSepDiff_stageProj
4022 C hC psi i
4024/-- The source-standard map to the separated completed differential module is continuous for
4025the finite-stage quotient topology. -/
4026theorem
4027 continuous_stdAugIdealToZCSepDiff
4032 (psi : ContinuousMonoidHom G H) :
4033 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4035 @Continuous
4038 inferInstance
4040 (stdAugIdealToZCSepDiff
4041 C hC psi) := by
4042 letI : Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :=
4045 C psi.toMonoidHom (directed_zcCompletedDifferentialModuleIndex C hForm hC psi)]
4046 rw [continuous_induced_rng]
4047 exact
4048 continuous_stdAugIdealToZCSepDiff_stageProjProduct
4049 C hC psi
4051@[simp 900]
4052theorem
4053 stdAugIdealToZCSepDiffOfBoundaryKernel_boundary
4057 (psi : ContinuousMonoidHom G H)
4058 (hker :
4059 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
4060 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
4062 C hC psi x = 0)
4063 (g : G) :
4064 stdAugIdealToZCSepDiffOfBoundaryKernel
4065 C hC psi hker
4066zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
4068 C G (MonoidHom.id G) g⟩ =
4069 zcSeparatedUniversalDifferential C psi.toMonoidHom g := by
4070 letI : Module (ZCCompletedGroupAlgebra C G)
4072 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
4073 have hcomp :=
4074 congrArg
4075 (fun f =>
4076 f (zcUniversalDifferential C (MonoidHom.id G) g))
4077 (stdAugIdealToZCSepDiffOfBoundaryKernel_comp_zcToStdAugIdeal
4078 C hC psi hker)
4079 calc
4080 stdAugIdealToZCSepDiffOfBoundaryKernel
4081 C hC psi hker
4082zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
4084 C G (MonoidHom.id G) g⟩ =
4086 C hC psi (zcUniversalDifferential C (MonoidHom.id G) g) := by
4089 _ = zcSeparatedUniversalDifferential C psi.toMonoidHom g := by
4090 exact
4092 C hC psi g
4094@[simp]
4095theorem
4096 stdAugIdealToZCSepDiff_boundary
4100 (psi : ContinuousMonoidHom G H)
4101 (g : G) :
4102 stdAugIdealToZCSepDiff
4103 C hC psi
4104zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
4106 C G (MonoidHom.id G) g⟩ =
4107 zcSeparatedUniversalDifferential C psi.toMonoidHom g := by
4108 exact
4109 stdAugIdealToZCSepDiffOfBoundaryKernel_boundary
4110 C hC psi
4112 C hC psi) g
4114/-- The conditional source-standard map kills each algebraic kernel-product generator. -/
4115theorem
4116 stdAugIdealToZCSepDiffOfBoundaryKernel_kernel_generator_smul
4120 (psi : ContinuousMonoidHom G H)
4121 (hker :
4122 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
4123 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
4125 C hC psi x = 0)
4128 stdAugIdealToZCSepDiffOfBoundaryKernel
4129 C hC psi hker ((zcGroupLike C G n.1 - 1) • s) = 0 := by
4130 letI : Module (ZCCompletedGroupAlgebra C G)
4132 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
4133 let f :=
4134 zcToStdAugIdeal C G (MonoidHom.id G)
4135 let M :=
4136 stdAugIdealToZCSepDiffOfBoundaryKernel
4137 C hC psi hker
4138 let L :=
4140 have hf : Function.Surjective f := by
4141 exact
4143 C G (MonoidHom.id G) (fun g => ⟨g, rfl⟩)
4144 rcases hf s with ⟨y, hy⟩
4145 have hcomp :=
4146 congrArg
4147 (fun F =>
4148 F ((zcGroupLike C G n.1 - 1) • y))
4149 (stdAugIdealToZCSepDiffOfBoundaryKernel_comp_zcToStdAugIdeal
4150 C hC psi hker)
4151 have harg :
4152 (zcGroupLike C G n.1 - 1) • s =
4153 f ((zcGroupLike C G n.1 - 1) • y) := by
4154 rw [map_smul, hy]
4155 calc
4156 M ((zcGroupLike C G n.1 - 1) • s) =
4157 M (f ((zcGroupLike C G n.1 - 1) • y)) := by
4158 rw [harg]
4159 _ = L ((zcGroupLike C G n.1 - 1) • y) := by
4160 simpa [M, L, f] using hcomp
4161 _ = 0 := by
4162 exact
4164 C hC psi n y
4166/-- The conditional source-standard map kills the algebraic product `I(ker psi) I(G)`. -/
4167theorem
4168 stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandard
4172 (psi : ContinuousMonoidHom G H)
4173 (hker :
4174 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
4175 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
4177 C hC psi x = 0)
4180 stdAugIdealToZCSepDiffOfBoundaryKernel
4181 C hC psi hker x = 0 := by
4182 letI : Module (ZCCompletedGroupAlgebra C G)
4184 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
4185 let M :=
4186 stdAugIdealToZCSepDiffOfBoundaryKernel
4187 C hC psi hker
4189 refine Submodule.span_induction
4190 (p := fun y _ => M y = 0) ?_ ?_ ?_ ?_ hx
4191 · rintro _ ⟨p, rfl
4192 exact
4193 stdAugIdealToZCSepDiffOfBoundaryKernel_kernel_generator_smul
4194 C hC psi hker p.1 p.2
4195 · simp only [ContinuousMonoidHom.coe_toMonoidHom, map_zero, M]
4196 · intro y z _ _ hy hz
4197 rw [map_add, hy, hz, add_zero]
4198 · intro a y _ hy
4199 rw [map_smul, hy, smul_zero]
4201/-- The source-standard map kills the algebraic product `I(ker psi) I(G)`. -/
4202theorem
4203 stdAugIdealToZCSepDiff_kills_kernelMulStandard
4207 (psi : ContinuousMonoidHom G H)
4210 stdAugIdealToZCSepDiff
4211 C hC psi x = 0 :=
4212 stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandard
4213 C hC psi
4215 C hC psi) hx
4217/-- If the conditional source-standard map is continuous for the separated quotient topology,
4218then killing the algebraic denominator implies that it kills the finite-stage closed denominator.
4220theorem
4221 stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandardClosed_of_continuous
4226 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4227 (hfopen : IsOpenMap psi)
4228 (hker :
4229 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
4230 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
4232 C hC psi x = 0)
4233 (hcont :
4234 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4236 @Continuous
4239 inferInstance
4241 (stdAugIdealToZCSepDiffOfBoundaryKernel
4242 C hC psi hker))
4245 C hC hForm psi hpsi hfopen) :
4246 stdAugIdealToZCSepDiffOfBoundaryKernel
4247 C hC psi hker x = 0 := by
4248 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4250 let M :=
4251 stdAugIdealToZCSepDiffOfBoundaryKernel
4252 C hC psi hker
4253 have hxcl :
4254 x ∈ closure
4258 C hC hForm psi hpsi hfopen]
4259 exact hx
4260 have hclosed_preimage :
4261 IsClosed
4262 (M ⁻¹'
4263 ({0} : Set (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom))) := by
4264 exact
4266 C psi.toMonoidHom).preimage hcont
4267 have hsubset :
4270 M ⁻¹' ({0} : Set (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)) := by
4271 intro y hy
4272 exact
4273 stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandard
4274 C hC psi hker hy
4275 exact closure_minimal hsubset hclosed_preimage hxcl
4277/-- If the source-standard map is continuous for the separated quotient topology, then it kills
4278the closed finite-stage denominator. -/
4279theorem
4280 stdAugIdealToZCSepDiff_kills_kernelMulStandardClosed_of_continuous
4285 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4286 (hfopen : IsOpenMap psi)
4287 (hcont :
4288 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4290 @Continuous
4293 inferInstance
4295 (stdAugIdealToZCSepDiff
4296 C hC psi))
4299 C hC hForm psi hpsi hfopen) :
4300 stdAugIdealToZCSepDiff
4301 C hC psi x = 0 := by
4302 have hcont' :
4303 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4305 @Continuous
4308 inferInstance
4310 (stdAugIdealToZCSepDiffOfBoundaryKernel
4311 C hC psi
4313 C hC psi)) := by
4314 simpa [stdAugIdealToZCSepDiff] using hcont
4315 exact
4316 stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandardClosed_of_continuous
4317 C hC hForm psi hpsi hfopen
4319 C hC psi) hcont' hx
4321/-- The source-standard map kills the closed finite-stage denominator. -/
4322theorem
4323 stdAugIdealToZCSepDiff_kills_kernelMulStandardClosed
4328 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4329 (hfopen : IsOpenMap psi)
4332 C hC hForm psi hpsi hfopen) :
4333 stdAugIdealToZCSepDiff
4334 C hC psi x = 0 :=
4335 stdAugIdealToZCSepDiff_kills_kernelMulStandardClosed_of_continuous
4336 C hC hForm psi hpsi hfopen
4337 (continuous_stdAugIdealToZCSepDiff
4338 C hC hForm psi) hx
4340/-- A conditional reverse map from the closed source augmentation quotient to the separated
4341module. The remaining closed-denominator input is isolated as `hclosed_kill`. -/
4342noncomputable def
4343 kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill
4348 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4349 (hfopen : IsOpenMap psi)
4350 (hker :
4351 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
4352 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
4354 C hC psi x = 0)
4355 (hclosed_kill :
4358 C hC hForm psi hpsi hfopen →
4359 stdAugIdealToZCSepDiffOfBoundaryKernel
4360 C hC psi hker x = 0) :
4361 letI : Module (ZCCompletedGroupAlgebra C G)
4363 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
4364 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
4367 letI : Module (ZCCompletedGroupAlgebra C G)
4369 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
4370 let M :=
4371 stdAugIdealToZCSepDiffOfBoundaryKernel
4372 C hC psi hker
4373 exact
4375 C hC hForm psi hpsi hfopen).liftQ M
4376 (by
4377 intro x hx
4378 rw [LinearMap.mem_ker]
4379 exact hclosed_kill x hx)
4381@[simp 900]
4382theorem
4383 kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill_boundary
4388 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4389 (hfopen : IsOpenMap psi)
4390 (hker :
4391 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
4392 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
4394 C hC psi x = 0)
4395 (hclosed_kill :
4398 C hC hForm psi hpsi hfopen →
4399 stdAugIdealToZCSepDiffOfBoundaryKernel
4400 C hC psi hker x = 0)
4401 (g : G) :
4402 kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill
4403 C hC hForm psi hpsi hfopen hker hclosed_kill
4404 (Submodule.Quotient.mk
4406 C hC hForm psi hpsi hfopen)
4407zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
4409 C G (MonoidHom.id G) g⟩) =
4410 zcSeparatedUniversalDifferential C psi.toMonoidHom g := by
4411 letI : Module (ZCCompletedGroupAlgebra C G)
4413 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
4414 rw [kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill,
4415 Submodule.liftQ_apply]
4416 exact
4417 stdAugIdealToZCSepDiffOfBoundaryKernel_boundary
4418 C hC psi hker g
4420/-- Target-linear version of the conditional reverse map from the closed source augmentation
4421quotient to the separated module. -/
4422noncomputable def
4423 kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill
4428 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4429 (hfopen : IsOpenMap psi)
4430 (hker :
4431 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
4432 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
4434 C hC psi x = 0)
4435 (hclosed_kill :
4438 C hC hForm psi hpsi hfopen →
4439 stdAugIdealToZCSepDiffOfBoundaryKernel
4440 C hC psi hker x = 0) :
4441 letI : Module (ZCCompletedGroupAlgebra C H)
4442 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
4444 C hC hForm psi hpsi hfopen
4445 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
4448 letI : Module (ZCCompletedGroupAlgebra C H)
4449 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
4451 C hC hForm psi hpsi hfopen
4452 letI : Module (ZCCompletedGroupAlgebra C G)
4454 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
4455 let Q :=
4456 kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill
4457 C hC hForm psi hpsi hfopen hker hclosed_kill
4458 refine
4459 { toFun := Q
4460 map_add' := by
4461 intro x y
4462 exact map_add Q x y
4463 map_smul' := by
4464 intro a x
4465 change Q
4466 (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a • x) =
4467 a • Q x
4469 symm
4470 calc
4471 a • Q x =
4474 Q x := by
4476 _ =
4478 Q x := by
4479 exact
4481 C hC psi
4483 (Q x) }
4485@[simp 900]
4486theorem
4487 kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill_boundary
4492 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4493 (hfopen : IsOpenMap psi)
4494 (hker :
4495 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
4496 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
4498 C hC psi x = 0)
4499 (hclosed_kill :
4502 C hC hForm psi hpsi hfopen →
4503 stdAugIdealToZCSepDiffOfBoundaryKernel
4504 C hC psi hker x = 0)
4505 (g : G) :
4506 kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill
4507 C hC hForm psi hpsi hfopen hker hclosed_kill
4508 (Submodule.Quotient.mk
4510 C hC hForm psi hpsi hfopen)
4511zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
4513 C G (MonoidHom.id G) g⟩) =
4514 zcSeparatedUniversalDifferential C psi.toMonoidHom g := by
4515 exact
4516 kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill_boundary
4517 C hC hForm psi hpsi hfopen hker hclosed_kill g
4519/-- Target-linear reverse map from the closed source augmentation quotient to the separated
4520module, reducing the closed-denominator condition to continuity of the source-standard map. -/
4521noncomputable def
4522 kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfContStdMap
4527 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4528 (hfopen : IsOpenMap psi)
4529 (hker :
4530 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
4531 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
4533 C hC psi x = 0)
4534 (hcont :
4535 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4537 @Continuous
4540 inferInstance
4542 (stdAugIdealToZCSepDiffOfBoundaryKernel
4543 C hC psi hker)) :
4544 letI : Module (ZCCompletedGroupAlgebra C H)
4545 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
4547 C hC hForm psi hpsi hfopen
4548 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
4551 kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill
4552 C hC hForm psi hpsi hfopen hker
4553 (fun _ hx =>
4554 stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandardClosed_of_continuous
4555 C hC hForm psi hpsi hfopen hker hcont hx)
4557@[simp 900]
4558theorem
4559 kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfContStdMap_boundary
4564 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4565 (hfopen : IsOpenMap psi)
4566 (hker :
4567 ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
4568 zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
4570 C hC psi x = 0)
4571 (hcont :
4572 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4574 @Continuous
4577 inferInstance
4579 (stdAugIdealToZCSepDiffOfBoundaryKernel
4580 C hC psi hker))
4581 (g : G) :
4582 kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfContStdMap
4583 C hC hForm psi hpsi hfopen hker hcont
4584 (Submodule.Quotient.mk
4586 C hC hForm psi hpsi hfopen)
4587zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
4589 C G (MonoidHom.id G) g⟩) =
4590 zcSeparatedUniversalDifferential C psi.toMonoidHom g := by
4591 exact
4592 kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill_boundary
4593 C hC hForm psi hpsi hfopen hker
4594 (fun x hx =>
4595 stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandardClosed_of_continuous
4596 C hC hForm psi hpsi hfopen hker hcont hx)
4599/-- Reverse map from the closed source augmentation quotient to the separated module, assuming
4600only that the closed denominator is killed by the unconditional source-standard map. -/
4601noncomputable def
4602 kerAugIdealQuotToZCSepDiffOfClosedKill
4607 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4608 (hfopen : IsOpenMap psi)
4609 (hclosed_kill :
4612 C hC hForm psi hpsi hfopen →
4613 stdAugIdealToZCSepDiff
4614 C hC psi x = 0) :
4615 letI : Module (ZCCompletedGroupAlgebra C G)
4617 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
4618 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
4621 kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill
4622 C hC hForm psi hpsi hfopen
4624 C hC psi)
4625 (fun x hx => by
4626 simpa [stdAugIdealToZCSepDiff]
4627 using hclosed_kill x hx)
4629@[simp 900]
4630theorem
4631 kerAugIdealQuotToZCSepDiffOfClosedKill_boundary
4636 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4637 (hfopen : IsOpenMap psi)
4638 (hclosed_kill :
4641 C hC hForm psi hpsi hfopen →
4642 stdAugIdealToZCSepDiff
4643 C hC psi x = 0)
4644 (g : G) :
4645 kerAugIdealQuotToZCSepDiffOfClosedKill
4646 C hC hForm psi hpsi hfopen hclosed_kill
4647 (Submodule.Quotient.mk
4649 C hC hForm psi hpsi hfopen)
4650zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
4652 C G (MonoidHom.id G) g⟩) =
4653 zcSeparatedUniversalDifferential C psi.toMonoidHom g := by
4654 exact
4655 kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill_boundary
4656 C hC hForm psi hpsi hfopen
4658 C hC psi)
4659 (fun x hx => by
4660 simpa [stdAugIdealToZCSepDiff]
4661 using hclosed_kill x hx) g
4663/-- The reverse map from the closed source augmentation quotient to the separated module is
4664continuous once the source-standard map is continuous. -/
4665theorem
4666 continuous_kerAugIdealQuotToZCSepDiffOfClosedKill
4671 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4672 (hfopen : IsOpenMap psi)
4673 (hclosed_kill :
4676 C hC hForm psi hpsi hfopen →
4677 stdAugIdealToZCSepDiff
4678 C hC psi x = 0)
4679 (hcont :
4680 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4682 @Continuous
4685 inferInstance
4687 (stdAugIdealToZCSepDiff
4688 C hC psi)) :
4689 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4691 Continuous
4692 (kerAugIdealQuotToZCSepDiffOfClosedKill
4693 C hC hForm psi hpsi hfopen hclosed_kill) := by
4694 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4697 C hC hForm psi hpsi hfopen]
4698 have hcomp :
4700 kerAugIdealQuotToZCSepDiffOfClosedKill
4701 C hC hForm psi hpsi hfopen hclosed_kill
4703 C hC hForm psi hpsi hfopen).mkQ x)) =
4704 stdAugIdealToZCSepDiff
4705 C hC psi := by
4706 funext x
4707 simp only [ContinuousMonoidHom.coe_toMonoidHom, kerAugIdealQuotToZCSepDiffOfClosedKill,
4708 kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill, Submodule.mkQ_apply, Submodule.liftQ_apply,
4709 stdAugIdealToZCSepDiff]
4710 rw [hcomp]
4711 exact hcont
4713/-- Target-linear reverse map from the closed source augmentation quotient to the separated
4714module, assuming only that the closed denominator is killed by the unconditional source-standard
4715map. -/
4716noncomputable def
4717 kerAugIdealQuotToZCSepDiffLinearOfClosedKill
4722 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4723 (hfopen : IsOpenMap psi)
4724 (hclosed_kill :
4727 C hC hForm psi hpsi hfopen →
4728 stdAugIdealToZCSepDiff
4729 C hC psi x = 0) :
4730 letI : Module (ZCCompletedGroupAlgebra C H)
4731 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
4733 C hC hForm psi hpsi hfopen
4734 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
4737 kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill
4738 C hC hForm psi hpsi hfopen
4740 C hC psi)
4741 (fun x hx => by
4742 simpa [stdAugIdealToZCSepDiff]
4743 using hclosed_kill x hx)
4745@[simp 900]
4746theorem
4747 kerAugIdealQuotToZCSepDiffLinearOfClosedKill_boundary
4752 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4753 (hfopen : IsOpenMap psi)
4754 (hclosed_kill :
4757 C hC hForm psi hpsi hfopen →
4758 stdAugIdealToZCSepDiff
4759 C hC psi x = 0)
4760 (g : G) :
4761 kerAugIdealQuotToZCSepDiffLinearOfClosedKill
4762 C hC hForm psi hpsi hfopen hclosed_kill
4763 (Submodule.Quotient.mk
4765 C hC hForm psi hpsi hfopen)
4766zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
4768 C G (MonoidHom.id G) g⟩) =
4769 zcSeparatedUniversalDifferential C psi.toMonoidHom g :=
4770 kerAugIdealQuotToZCSepDiffOfClosedKill_boundary
4771 C hC hForm psi hpsi hfopen hclosed_kill g
4773/-- Target-linear reverse map from the closed source augmentation quotient to the separated
4774module, reducing the closed-denominator condition to continuity of the unconditional
4775source-standard map. -/
4776noncomputable def
4777 kerAugIdealQuotToZCSepDiffLinearOfContStdMap
4782 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4783 (hfopen : IsOpenMap psi)
4784 (hcont :
4785 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4787 @Continuous
4790 inferInstance
4792 (stdAugIdealToZCSepDiff
4793 C hC psi)) :
4794 letI : Module (ZCCompletedGroupAlgebra C H)
4795 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
4797 C hC hForm psi hpsi hfopen
4798 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
4801 kerAugIdealQuotToZCSepDiffLinearOfClosedKill
4802 C hC hForm psi hpsi hfopen
4803 (fun _ hx =>
4804 stdAugIdealToZCSepDiff_kills_kernelMulStandardClosed_of_continuous
4805 C hC hForm psi hpsi hfopen hcont hx)
4807@[simp 900]
4808theorem
4809 kerAugIdealQuotToZCSepDiffLinearOfContStdMap_boundary
4814 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4815 (hfopen : IsOpenMap psi)
4816 (hcont :
4817 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4819 @Continuous
4822 inferInstance
4824 (stdAugIdealToZCSepDiff
4825 C hC psi))
4826 (g : G) :
4827 kerAugIdealQuotToZCSepDiffLinearOfContStdMap
4828 C hC hForm psi hpsi hfopen hcont
4829 (Submodule.Quotient.mk
4831 C hC hForm psi hpsi hfopen)
4832zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
4834 C G (MonoidHom.id G) g⟩) =
4835 zcSeparatedUniversalDifferential C psi.toMonoidHom g :=
4836 kerAugIdealQuotToZCSepDiffLinearOfClosedKill_boundary
4837 C hC hForm psi hpsi hfopen
4838 (fun _ hx =>
4839 stdAugIdealToZCSepDiff_kills_kernelMulStandardClosed_of_continuous
4840 C hC hForm psi hpsi hfopen hcont hx) g
4842/-- The target-linear reverse map obtained from a continuous source-standard map is continuous. -/
4843theorem
4844 continuous_kerAugIdealQuotToZCSepDiffLinearOfContStdMap
4849 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4850 (hfopen : IsOpenMap psi)
4851 (hcont :
4852 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4854 @Continuous
4857 inferInstance
4859 (stdAugIdealToZCSepDiff
4860 C hC psi)) :
4861 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4863 Continuous
4864 (kerAugIdealQuotToZCSepDiffLinearOfContStdMap
4865 C hC hForm psi hpsi hfopen hcont) := by
4866 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4868 simpa [kerAugIdealQuotToZCSepDiffLinearOfContStdMap,
4869 kerAugIdealQuotToZCSepDiffLinearOfClosedKill]
4870 using
4871 continuous_kerAugIdealQuotToZCSepDiffOfClosedKill
4872 C hC hForm psi hpsi hfopen
4873 (fun _ hx =>
4874 stdAugIdealToZCSepDiff_kills_kernelMulStandardClosed_of_continuous
4875 C hC hForm psi hpsi hfopen hcont hx)
4876 hcont
4878/-- Target-linear reverse map from the closed source augmentation quotient to the separated
4879module. -/
4880noncomputable def
4881 kerAugIdealQuotToZCSepDiffLinear
4886 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4887 (hfopen : IsOpenMap psi) :
4888 letI : Module (ZCCompletedGroupAlgebra C H)
4889 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
4891 C hC hForm psi hpsi hfopen
4892 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
4895 kerAugIdealQuotToZCSepDiffLinearOfContStdMap
4896 C hC hForm psi hpsi hfopen
4897 (continuous_stdAugIdealToZCSepDiff
4898 C hC hForm psi)
4900@[simp 900]
4901theorem
4902 kerAugIdealQuotToZCSepDiffLinear_boundary
4907 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4908 (hfopen : IsOpenMap psi)
4909 (g : G) :
4910 kerAugIdealQuotToZCSepDiffLinear
4911 C hC hForm psi hpsi hfopen
4912 (Submodule.Quotient.mk
4914 C hC hForm psi hpsi hfopen)
4915zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
4917 C G (MonoidHom.id G) g⟩) =
4918 zcSeparatedUniversalDifferential C psi.toMonoidHom g :=
4919 kerAugIdealQuotToZCSepDiffLinearOfContStdMap_boundary
4920 C hC hForm psi hpsi hfopen
4921 (continuous_stdAugIdealToZCSepDiff
4922 C hC hForm psi) g
4924/-- The target-linear reverse map from the closed source augmentation quotient to the separated
4925module is continuous. -/
4926theorem
4927 continuous_kerAugIdealQuotToZCSepDiffLinear
4932 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4933 (hfopen : IsOpenMap psi) :
4934 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
4936 Continuous
4937 (kerAugIdealQuotToZCSepDiffLinear
4938 C hC hForm psi hpsi hfopen) :=
4939 continuous_kerAugIdealQuotToZCSepDiffLinearOfContStdMap
4940 C hC hForm psi hpsi hfopen
4941 (continuous_stdAugIdealToZCSepDiff
4942 C hC hForm psi)
4944/-- The completed universal differential module maps to the closed source augmentation quotient
4945by `d g ↦ [g] - 1`. -/
4951 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4952 (hfopen : IsOpenMap psi) :
4953 letI : Module (ZCCompletedGroupAlgebra C H)
4954 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
4956 C hC hForm psi hpsi hfopen
4958 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
4959 letI : Module (ZCCompletedGroupAlgebra C H)
4960 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
4962 C hC hForm psi hpsi hfopen
4963 exact
4965 (A := KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
4966 C psi.toMonoidHom
4968 C hC hForm psi hpsi hfopen)
4970 C hC hForm psi hpsi hfopen)
4972@[simp 900]
4978 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
4979 (hfopen : IsOpenMap psi) (g : G) :
4981 C hC hForm psi hpsi hfopen
4982 (zcUniversalDifferential C psi.toMonoidHom g) =
4984 C hC hForm psi hpsi hfopen g := by
4985 letI : Module (ZCCompletedGroupAlgebra C H)
4986 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
4988 C hC hForm psi hpsi hfopen
4989 exact
4991 (A := KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
4992 C psi.toMonoidHom
4994 C hC hForm psi hpsi hfopen)
4996 C hC hForm psi hpsi hfopen) g
4998/-- If the pre-quotient source-boundary lift to the closed augmentation quotient is continuous
4999for the finite-stage pre-module topology, then it kills the finite-stage closed relation
5000denominator. This is the exact descent criterion needed to factor the algebraic map through the
5001separated completed differential module. -/
5007 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5008 (hfopen : IsOpenMap psi)
5009 [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
5010 (hdir : Directed (· ≤ ·)
5011 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
5013 (hcont :
5014 letI : Module (ZCCompletedGroupAlgebra C H)
5015 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5017 C hC hForm psi hpsi hfopen
5018 @Continuous
5020 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5022 inferInstance
5026 C hC hForm psi hpsi hfopen)))
5029 letI : Module (ZCCompletedGroupAlgebra C H)
5030 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5032 C hC hForm psi hpsi hfopen
5036 C hC hForm psi hpsi hfopen) x = 0 := by
5037 letI : Module (ZCCompletedGroupAlgebra C H)
5038 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5040 C hC hForm psi hpsi hfopen
5041 letI : TopologicalSpace
5044 letI : T1Space
5045 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5047 have hxcl :
5048 x ∈ closure
5050 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom) :
5054 have hEq :=
5056 C psi.toMonoidHom hdir
5057 rw [hEq]
5058 exact hx
5059 have hker_closed :
5060 IsClosed
5065 C hC hForm psi hpsi hfopen) y) ⁻¹'
5066 ({0} : Set
5067 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen))) :=
5068 isClosed_singleton.preimage hcont
5069 have hrel_subset_ker :
5071 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom) :
5079 C hC hForm psi hpsi hfopen) y) ⁻¹'
5080 ({0} : Set
5081 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen))) := by
5082 intro y hy
5083 exact
5085 (A := KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5088 C hC hForm psi hpsi hfopen)
5090 C hC hForm psi hpsi hfopen)) hy
5091 exact closure_minimal hrel_subset_ker hker_closed hxcl
5093/-- Version of
5095with nonemptiness and directedness of finite stages supplied by the continuous source map. -/
5101 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5102 (hfopen : IsOpenMap psi)
5103 (hcont :
5104 letI : Module (ZCCompletedGroupAlgebra C H)
5105 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5107 C hC hForm psi hpsi hfopen
5108 @Continuous
5110 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5112 inferInstance
5116 C hC hForm psi hpsi hfopen)))
5119 letI : Module (ZCCompletedGroupAlgebra C H)
5120 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5122 C hC hForm psi hpsi hfopen
5126 C hC hForm psi hpsi hfopen) x = 0 := by
5127 letI : Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :=
5129 exact
5131 C hC hForm psi hpsi hfopen
5133 hcont hx
5135/-- Under the explicit continuity hypothesis for the pre-quotient source-boundary lift, the closed
5136source augmentation quotient receives the separated completed universal differential module. -/
5142 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5143 (hfopen : IsOpenMap psi)
5144 [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
5145 (hdir : Directed (· ≤ ·)
5146 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
5148 (hcont :
5149 letI : Module (ZCCompletedGroupAlgebra C H)
5150 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5152 C hC hForm psi hpsi hfopen
5153 @Continuous
5155 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5157 inferInstance
5161 C hC hForm psi hpsi hfopen))) :
5162 letI : Module (ZCCompletedGroupAlgebra C H)
5163 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5165 C hC hForm psi hpsi hfopen
5167 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
5168 letI : Module (ZCCompletedGroupAlgebra C H)
5169 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5171 C hC hForm psi hpsi hfopen
5172 exact
5177 C hC hForm psi hpsi hfopen))
5178 (by
5179 intro x hx
5180 rw [LinearMap.mem_ker]
5181 exact
5183 C hC hForm psi hpsi hfopen hdir hcont hx)
5185/-- Public version of the closed-augmentation descent map with finite-stage nonemptiness and
5186directedness supplied by the continuous source map. -/
5192 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5193 (hfopen : IsOpenMap psi)
5194 (hcont :
5195 letI : Module (ZCCompletedGroupAlgebra C H)
5196 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5198 C hC hForm psi hpsi hfopen
5199 @Continuous
5201 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5203 inferInstance
5207 C hC hForm psi hpsi hfopen))) :
5208 letI : Module (ZCCompletedGroupAlgebra C H)
5209 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5211 C hC hForm psi hpsi hfopen
5213 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
5214 letI : Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :=
5216 exact
5218 C hC hForm psi hpsi hfopen
5220 hcont
5222@[simp 900]
5228 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5229 (hfopen : IsOpenMap psi)
5230 [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
5231 (hdir : Directed (· ≤ ·)
5232 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
5234 (hcont :
5235 letI : Module (ZCCompletedGroupAlgebra C H)
5236 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5238 C hC hForm psi hpsi hfopen
5239 @Continuous
5241 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5243 inferInstance
5247 C hC hForm psi hpsi hfopen)))
5248 (g : G) :
5250 C hC hForm psi hpsi hfopen hdir hcont
5251 (zcSeparatedUniversalDifferential C psi.toMonoidHom g) =
5253 C hC hForm psi hpsi hfopen g := by
5254 letI : Module (ZCCompletedGroupAlgebra C H)
5255 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5257 C hC hForm psi hpsi hfopen
5259 zcSeparatedUniversalDifferential, Submodule.mkQ_apply, Submodule.liftQ_apply]
5262@[simp 900]
5268 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5269 (hfopen : IsOpenMap psi)
5270 (hcont :
5271 letI : Module (ZCCompletedGroupAlgebra C H)
5272 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5274 C hC hForm psi hpsi hfopen
5275 @Continuous
5277 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5279 inferInstance
5283 C hC hForm psi hpsi hfopen)))
5284 (g : G) :
5286 C hC hForm psi hpsi hfopen hcont
5287 (zcSeparatedUniversalDifferential C psi.toMonoidHom g) =
5289 C hC hForm psi hpsi hfopen g := by
5290 letI : Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :=
5292 exact
5294 C hC hForm psi hpsi hfopen
5296 hcont g
5298/-- The separated closed-augmentation map is the factorization of the algebraic closed-augmentation
5299map through `A_psi(C) -> A_psi(C)_sep`. -/
5305 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5306 (hfopen : IsOpenMap psi)
5307 [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
5308 (hdir : Directed (· ≤ ·)
5309 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
5311 (hcont :
5312 letI : Module (ZCCompletedGroupAlgebra C H)
5313 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5315 C hC hForm psi hpsi hfopen
5316 @Continuous
5318 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5320 inferInstance
5324 C hC hForm psi hpsi hfopen))) :
5325 letI : Module (ZCCompletedGroupAlgebra C H)
5326 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5328 C hC hForm psi hpsi hfopen
5330 C hC hForm psi hpsi hfopen hdir hcont).comp
5333 C hC hForm psi hpsi hfopen := by
5334 letI : Module (ZCCompletedGroupAlgebra C H)
5335 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5337 C hC hForm psi hpsi hfopen
5339 intro g
5340 rw [LinearMap.comp_apply,
5350 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5351 (hfopen : IsOpenMap psi)
5352 (hcont :
5353 letI : Module (ZCCompletedGroupAlgebra C H)
5354 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5356 C hC hForm psi hpsi hfopen
5357 @Continuous
5359 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5361 inferInstance
5365 C hC hForm psi hpsi hfopen))) :
5366 letI : Module (ZCCompletedGroupAlgebra C H)
5367 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5369 C hC hForm psi hpsi hfopen
5371 C hC hForm psi hpsi hfopen hcont).comp
5374 C hC hForm psi hpsi hfopen := by
5375 letI : Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :=
5377 exact
5379 C hC hForm psi hpsi hfopen
5381 hcont
5383/-- The descended forward map to the closed augmentation quotient is continuous once the
5384pre-quotient source-boundary lift is continuous. -/
5390 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5391 (hfopen : IsOpenMap psi)
5392 [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
5393 (hdir : Directed (· ≤ ·)
5394 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
5396 (hcont :
5397 letI : Module (ZCCompletedGroupAlgebra C H)
5398 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5400 C hC hForm psi hpsi hfopen
5401 @Continuous
5403 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5405 inferInstance
5409 C hC hForm psi hpsi hfopen))) :
5410 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
5412 letI : Module (ZCCompletedGroupAlgebra C H)
5413 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5415 C hC hForm psi hpsi hfopen
5416 @Continuous
5418 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5420 inferInstance
5422 C hC hForm psi hpsi hfopen hdir hcont) := by
5423 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
5425 letI : Module (ZCCompletedGroupAlgebra C H)
5426 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5428 C hC hForm psi hpsi hfopen
5430 (C := C) (G := G) (H := H) (ψ := psi.toMonoidHom)]
5431 have hcomp :
5434 C hC hForm psi hpsi hfopen hdir hcont
5439 C hC hForm psi hpsi hfopen) := by
5440 funext x
5442 Submodule.mkQ_apply, Submodule.liftQ_apply]
5443 simpa [hcomp] using hcont
5445/-- Continuity of the forward map when the finite-stage index data are supplied by the
5446continuous source map. -/
5452 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5453 (hfopen : IsOpenMap psi)
5454 (hcont :
5455 letI : Module (ZCCompletedGroupAlgebra C H)
5456 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5458 C hC hForm psi hpsi hfopen
5459 @Continuous
5461 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5463 inferInstance
5467 C hC hForm psi hpsi hfopen))) :
5468 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
5470 letI : Module (ZCCompletedGroupAlgebra C H)
5471 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5473 C hC hForm psi hpsi hfopen
5474 @Continuous
5476 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5478 inferInstance
5480 C hC hForm psi hpsi hfopen hcont) := by
5481 letI : Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :=
5483 exact
5485 C hC hForm psi hpsi hfopen
5487 hcont
5489/-- The map `A_psi(C) -> I(G) / closure(I(ker psi) I(G))` is onto: the closed quotient is
5490generated by the source boundaries, and completed target scalars agree with source scalars there. -/
5496 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5497 (hfopen : IsOpenMap psi) :
5498 Function.Surjective
5500 C hC hForm psi hpsi hfopen) := by
5501 letI : Module (ZCCompletedGroupAlgebra C H)
5502 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5504 C hC hForm psi hpsi hfopen
5505 intro x
5506 refine Submodule.Quotient.induction_on
5508 C hC hForm psi hpsi hfopen) x ?_
5509 intro y
5510 let L :=
5512 C hC hForm psi hpsi hfopen
5514 ∃ m : ZCCompletedDifferentialModule C psi.toMonoidHom,
5515 L m = Submodule.Quotient.mk
5517 C hC hForm psi hpsi hfopen) y
5518 have hy : P y := by
5519 have hyspan : (y : ZCCompletedGroupAlgebra C G) ∈
5520 Submodule.span (ZCCompletedGroupAlgebra C G)
5521 (Set.range fun h : G => zcGroupLike C G h - 1) := by
5522 change (y : ZCCompletedGroupAlgebra C G) ∈
5524 exact y.2
5525 refine Submodule.span_induction
5526 (p := fun z hz =>
5528 ⟨z, by
5530 ?hgen ?hzero ?hadd ?hsmul hyspan
5531 · rintro _ ⟨g, rfl
5532 refine ⟨zcUniversalDifferential C psi.toMonoidHom g, ?_⟩
5534 rfl
5535 · refine ⟨0, ?_⟩
5536 change (0 : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) =
5537 Submodule.Quotient.mk
5539 C hC hForm psi hpsi hfopen)
5541 rw [Submodule.Quotient.mk_zero]
5542 · intro a b ha hb hpa hpb
5543 rcases hpa with ⟨ma, hma⟩
5544 rcases hpb with ⟨mb, hmb⟩
5545 refine ⟨ma + mb, ?_⟩
5546 rw [map_add, hma, hmb, ← Submodule.Quotient.mk_add]
5548 Submodule.Quotient.mk
5550 C hC hForm psi hpsi hfopen) t)
5551 exact Subtype.ext rfl
5552 · intro a b hb hpb
5553 rcases hpb with ⟨m, hm⟩
5554 refine ⟨zcCompletedGroupAlgebraMap C hC psi a • m, ?_⟩
5555 rw [map_smul, hm]
5556 calc
5558 Submodule.Quotient.mk
5560 C hC hForm psi hpsi hfopen)
5561 ⟨b, by
5563 a •
5564 Submodule.Quotient.mk
5566 C hC hForm psi hpsi hfopen)
5567 ⟨b, by
5569 exact
5571 C hC hForm psi hpsi hfopen a
5572 (Submodule.Quotient.mk
5574 C hC hForm psi hpsi hfopen)
5575 ⟨b, by
5577 _ = Submodule.Quotient.mk
5579 C hC hForm psi hpsi hfopen)
5580 ⟨a • b, by
5582 exact Submodule.smul_mem
5583 (Submodule.span (ZCCompletedGroupAlgebra C G)
5584 (Set.range fun h : G => zcGroupLike C G h - 1)) a hb⟩ := by
5585 rw [← Submodule.Quotient.mk_smul]
5587 Submodule.Quotient.mk
5589 C hC hForm psi hpsi hfopen) t)
5590 exact Subtype.ext rfl
5591 exact hy
5593/-- The separated closed-augmentation map is surjective under the same pre-quotient continuity
5594hypothesis needed for the descent. -/
5600 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5601 (hfopen : IsOpenMap psi)
5602 [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
5603 (hdir : Directed (· ≤ ·)
5604 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
5606 (hcont :
5607 letI : Module (ZCCompletedGroupAlgebra C H)
5608 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5610 C hC hForm psi hpsi hfopen
5611 @Continuous
5613 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5615 inferInstance
5619 C hC hForm psi hpsi hfopen))) :
5620 Function.Surjective
5622 C hC hForm psi hpsi hfopen hdir hcont) := by
5623 letI : Module (ZCCompletedGroupAlgebra C H)
5624 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5626 C hC hForm psi hpsi hfopen
5627 intro y
5628 rcases
5630 C hC hForm psi hpsi hfopen y with
5631 ⟨m, hm⟩
5632 refine ⟨zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom m, ?_⟩
5633 have hfactor :=
5634 congrArg (fun L : ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
5635 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen => L m)
5637 C hC hForm psi hpsi hfopen hdir hcont)
5638 simpa [LinearMap.comp_apply] using hfactor.trans hm
5645 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5646 (hfopen : IsOpenMap psi)
5647 (hcont :
5648 letI : Module (ZCCompletedGroupAlgebra C H)
5649 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5651 C hC hForm psi hpsi hfopen
5652 @Continuous
5654 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5656 inferInstance
5660 C hC hForm psi hpsi hfopen))) :
5661 Function.Surjective
5663 C hC hForm psi hpsi hfopen hcont) := by
5664 letI : Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :=
5666 exact
5668 C hC hForm psi hpsi hfopen
5670 hcont
5672/-- The separated completed universal differential module maps to the closed source augmentation
5673quotient by `d g ↦ [g] - 1`. The pre-quotient lift continuity is supplied by the
5674finite-stage factorization theorem. -/
5680 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5681 (hfopen : IsOpenMap psi) :
5682 letI : Module (ZCCompletedGroupAlgebra C H)
5683 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5685 C hC hForm psi hpsi hfopen
5687 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
5688 let hcont :=
5690 C hC hForm psi hpsi hfopen
5691 exact
5693 C hC hForm psi hpsi hfopen hcont
5695@[simp]
5701 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5702 (hfopen : IsOpenMap psi) (g : G) :
5704 C hC hForm psi hpsi hfopen
5705 (zcSeparatedUniversalDifferential C psi.toMonoidHom g) =
5707 C hC hForm psi hpsi hfopen g := by
5708 let hcont :=
5710 C hC hForm psi hpsi hfopen
5713 C hC hForm psi hpsi hfopen hcont g
5715/-- The unconditional separated closed-augmentation map factors the algebraic map through
5716`A_psi(C) -> A_psi(C)_sep`. -/
5722 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5723 (hfopen : IsOpenMap psi) :
5724 letI : Module (ZCCompletedGroupAlgebra C H)
5725 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5727 C hC hForm psi hpsi hfopen
5729 C hC hForm psi hpsi hfopen).comp
5732 C hC hForm psi hpsi hfopen := by
5733 let hcont :=
5735 C hC hForm psi hpsi hfopen
5738 C hC hForm psi hpsi hfopen hcont
5740/-- The separated closed-augmentation map is continuous, with the pre-quotient lift continuity
5741provided by the finite-stage factorization theorem. -/
5747 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5748 (hfopen : IsOpenMap psi) :
5749 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
5751 letI : Module (ZCCompletedGroupAlgebra C H)
5752 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5754 C hC hForm psi hpsi hfopen
5755 @Continuous
5757 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
5759 inferInstance
5761 C hC hForm psi hpsi hfopen) := by
5762 let hcont :=
5764 C hC hForm psi hpsi hfopen
5767 C hC hForm psi hpsi hfopen hcont
5769/-- The separated closed-augmentation map is surjective. -/
5775 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5776 (hfopen : IsOpenMap psi) :
5777 Function.Surjective
5779 C hC hForm psi hpsi hfopen) := by
5780 let hcont :=
5782 C hC hForm psi hpsi hfopen
5785 C hC hForm psi hpsi hfopen hcont
5787@[simp]
5793 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5794 (hfopen : IsOpenMap psi)
5796 kerAugIdealQuotToZCSepDiffLinear
5797 C hC hForm psi hpsi hfopen
5798 (Submodule.Quotient.mk
5800 C hC hForm psi hpsi hfopen) x) =
5801 stdAugIdealToZCSepDiff
5802 C hC psi x := by
5803 simp only [ContinuousMonoidHom.coe_toMonoidHom, kerAugIdealQuotToZCSepDiffLinear,
5804 kerAugIdealQuotToZCSepDiffLinearOfContStdMap, kerAugIdealQuotToZCSepDiffLinearOfClosedKill,
5805 kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill,
5806 kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill, LinearMap.coe_mk, AddHom.coe_mk, Submodule.liftQ_apply,
5807 stdAugIdealToZCSepDiff]
5809/-- The reverse closed-augmentation map composed with the forward separated map is the identity. -/
5815 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5816 (hfopen : IsOpenMap psi) :
5817 letI : Module (ZCCompletedGroupAlgebra C H)
5818 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5820 C hC hForm psi hpsi hfopen
5821 (kerAugIdealQuotToZCSepDiffLinear
5822 C hC hForm psi hpsi hfopen).comp
5824 C hC hForm psi hpsi hfopen) =
5825 LinearMap.id := by
5826 letI : Module (ZCCompletedGroupAlgebra C H)
5827 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5829 C hC hForm psi hpsi hfopen
5831 intro g
5832 rw [LinearMap.comp_apply,
5835 kerAugIdealQuotToZCSepDiffLinear_boundary
5836 C hC hForm psi hpsi hfopen g
5838/-- The forward separated map composed with the reverse closed-augmentation map is the identity. -/
5844 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
5845 (hfopen : IsOpenMap psi) :
5846 letI : Module (ZCCompletedGroupAlgebra C H)
5847 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5849 C hC hForm psi hpsi hfopen
5851 C hC hForm psi hpsi hfopen).comp
5852 (kerAugIdealQuotToZCSepDiffLinear
5853 C hC hForm psi hpsi hfopen) =
5854 LinearMap.id := by
5855 letI : Module (ZCCompletedGroupAlgebra C H)
5856 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
5858 C hC hForm psi hpsi hfopen
5859 letI : Module (ZCCompletedGroupAlgebra C G)
5861 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
5862 apply LinearMap.ext
5863 intro x
5864 refine Submodule.Quotient.induction_on
5866 C hC hForm psi hpsi hfopen) x ?_
5867 intro y
5868 let F :=
5870 C hC hForm psi hpsi hfopen
5871 let S :=
5872 stdAugIdealToZCSepDiff
5873 C hC psi
5875 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen :=
5876 fun y => Submodule.Quotient.mk
5878 C hC hForm psi hpsi hfopen) y
5879 have hmk :
5880 kerAugIdealQuotToZCSepDiffLinear
5881 C hC hForm psi hpsi hfopen (Q y) =
5882 S y := by
5883 exact
5885 C hC hForm psi hpsi hfopen y
5886 change F
5887 (kerAugIdealQuotToZCSepDiffLinear
5888 C hC hForm psi hpsi hfopen (Q y)) = Q y
5889 rw [hmk]
5891 F (S y) = Q y
5892 have hyspan : (y : ZCCompletedGroupAlgebra C G) ∈
5893 Submodule.span (ZCCompletedGroupAlgebra C G)
5894 (Set.range fun h : G => zcGroupLike C G h - 1) := by
5895 change (y : ZCCompletedGroupAlgebra C G) ∈
5897 exact y.2
5898 exact
5899 (Submodule.span_induction
5900 (p := fun z hz =>
5902 (y' : ZCCompletedGroupAlgebra C G) = z → P y')
5903 (by
5904 rintro _ ⟨g, rfl⟩ y' hy'
5905 have hy'' :
5906 y' =
5907zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
5909 C G (MonoidHom.id G) g⟩ := by
5910 apply Subtype.ext
5912 rw [hy'']
5914zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
5916 C G (MonoidHom.id G) g⟩
5917 change P yg
5918 have hSg :
5919 S yg = zcSeparatedUniversalDifferential C psi.toMonoidHom g := by
5920 exact
5921 stdAugIdealToZCSepDiff_boundary
5922 C hC psi g
5923 dsimp [P, Q]
5924 calc
5925 F (S yg) = F (zcSeparatedUniversalDifferential C psi.toMonoidHom g) := by
5926 exact congrArg F hSg
5927 _ =
5929 C hC hForm psi hpsi hfopen g := by
5931 _ = Submodule.Quotient.mk yg := rfl)
5932 (by
5933 intro y' hy'
5934 have hy'' : y' = 0 := by
5935 apply Subtype.ext
5936 simpa using hy'
5937 rw [hy'']
5939 simp only [ContinuousMonoidHom.coe_toMonoidHom, map_zero, Submodule.Quotient.mk_zero, P, Q])
5940 (by
5941 intro a b ha hb hpa hpb y' hy'
5943 ⟨a, by
5946 ⟨b, by
5948 have hpa' : P ya := hpa ya rfl
5949 have hpb' : P yb := hpb yb rfl
5950 change F (S ya) = Q ya at hpa'
5951 change F (S yb) = Q yb at hpb'
5952 have hy'' : y' = ya + yb := by
5953 apply Subtype.ext
5954 simpa [ya, yb] using hy'
5955 rw [hy'']
5956 change P (ya + yb)
5957 change F (S (ya + yb)) = Q (ya + yb)
5958 rw [map_add, map_add, hpa', hpb']
5959 simp only [Submodule.Quotient.mk_add, Q])
5960 (by
5961 intro a b hb hpb y' hy'
5963 ⟨b, by
5965 have hpb' : P yb := hpb yb rfl
5966 change F (S yb) = Q yb at hpb'
5967 have hy'' : y' = a • yb := by
5968 apply Subtype.ext
5969 simpa [yb] using hy'
5970 rw [hy'']
5971 change P (a • yb)
5972 change F (S (a • yb)) = Q (a • yb)
5973 have hsource :
5974 a • S yb =
5975 zcCompletedGroupAlgebraMap C hC psi a • S yb := by
5976 exact
5978 C hC psi a (S yb)).symm
5979 calc
5980 F (S (a • yb)) = F (a • S yb) := by
5982 _ = F (zcCompletedGroupAlgebraMap C hC psi a • S yb) := by
5983 rw [hsource]
5984 _ = zcCompletedGroupAlgebraMap C hC psi a • F (S yb) := by
5986 _ = zcCompletedGroupAlgebraMap C hC psi a • Q yb := by
5987 rw [hpb']
5988 _ = a • Q yb := by
5989 exact
5991 C hC hForm psi hpsi hfopen a (Q yb)
5992 _ = Q (a • yb) := by
5993 dsimp [Q])
5994 hyspan) y rfl
5996/-- The separated completed differential module is the closed source augmentation quotient for a
5997surjective open continuous homomorphism. -/
6003 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6004 (hfopen : IsOpenMap psi) :
6005 letI : Module (ZCCompletedGroupAlgebra C H)
6006 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
6008 C hC hForm psi hpsi hfopen
6011 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
6012 letI : Module (ZCCompletedGroupAlgebra C H)
6013 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
6015 C hC hForm psi hpsi hfopen
6016 exact
6017 LinearEquiv.ofLinear
6019 C hC hForm psi hpsi hfopen)
6020 (kerAugIdealQuotToZCSepDiffLinear
6021 C hC hForm psi hpsi hfopen)
6023 C hC hForm psi hpsi hfopen)
6025 C hC hForm psi hpsi hfopen)
6027@[simp]
6033 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6034 (hfopen : IsOpenMap psi)
6037 C hC hForm psi hpsi hfopen x =
6039 C hC hForm psi hpsi hfopen x := rfl
6041@[simp]
6047 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6048 (hfopen : IsOpenMap psi)
6049 (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
6051 C hC hForm psi hpsi hfopen).symm x =
6052 kerAugIdealQuotToZCSepDiffLinear
6053 C hC hForm psi hpsi hfopen x := rfl
6055/-- Paper-facing version of the closed source augmentation quotient equivalence. Here
6056`ZCApsi C psi` is definitionally the separated completed differential module, not the algebraic
6057quotient. -/
6063 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6064 (hfopen : IsOpenMap psi) :
6065 letI : Module (ZCCompletedGroupAlgebra C H)
6066 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
6068 C hC hForm psi hpsi hfopen
6069 ZCApsi C psi.toMonoidHom ≃ₗ[ZCCompletedGroupAlgebra C H]
6070 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen :=
6072 C hC hForm psi hpsi hfopen
6074@[simp]
6080 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6081 (hfopen : IsOpenMap psi)
6082 (x : ZCApsi C psi.toMonoidHom) :
6084 C hC hForm psi hpsi hfopen x =
6086 C hC hForm psi hpsi hfopen x := rfl
6088@[simp]
6094 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6095 (hfopen : IsOpenMap psi)
6096 (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
6098 C hC hForm psi hpsi hfopen).symm x =
6099 kerAugIdealQuotToZCSepDiffLinear
6100 C hC hForm psi hpsi hfopen x := rfl
6107 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6108 (hker_mul :
6110 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
6112 (⟨k * (y : ZCCompletedGroupAlgebra C G),
6119 C hC hForm psi hpsi hker_mul
6120 zcCompletedGroupAlgebraMap C hC psi a • x = a • x := by
6123 C hC hForm psi hpsi hker_mul
6125 (zcCompletedGroupAlgebraMap C hC psi a) • x =
6126 a • x
6127 have hdiff :
6129 (zcCompletedGroupAlgebraMap C hC psi a) - a ∈
6130 RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) := by
6133 (zcCompletedGroupAlgebraMap C hC psi a) - a) = 0
6135 have hzero :=
6137 C hC psi hker_mul
6139 (zcCompletedGroupAlgebraMap C hC psi a) - a) hdiff x
6140 rw [sub_smul] at hzero
6141 exact sub_eq_zero.mp hzero
6148 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6149 (hker_mul :
6151 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
6153 (⟨k * (y : ZCCompletedGroupAlgebra C G),
6160 C hC hForm psi hpsi hker_mul
6161 zcGroupLike C H (psi g) • x = zcGroupLike C G g • x := by
6164 C hC hForm psi hpsi hker_mul
6165 rw [← zcCompletedGroupAlgebraMap_groupLike (C := C) (hC := hC) psi g]
6166 exact
6168 C hC hForm psi hpsi hker_mul (zcGroupLike C G g) x
6170/-- Under the explicit kernel-product hypothesis, the source boundary is a crossed differential
6171for the descended completed target scalars. -/
6177 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6178 (hker_mul :
6180 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
6182 (⟨k * (y : ZCCompletedGroupAlgebra C G),
6188 C hC hForm psi hpsi hker_mul
6194 C hC hForm psi hpsi hker_mul
6195 intro g h
6196 have hsource :=
6198 C psi g h
6199 rw [hsource]
6200 congr 1
6201 change zcGroupLike C G g •
6203 zcGroupLike C H (psi g) •
6205 exact
6207 C hC hForm psi hpsi hker_mul g
6210/-- Under the explicit kernel-product hypothesis, the completed universal differential module maps
6211to the algebraic source augmentation quotient by `d g ↦ [g] - 1`.
6213This is the algebraic version of
6215the condition needed for the algebraic quotient `I(G) / I(ker psi) I(G)` to carry the completed
6216target `Z_C[[H]]`-module structure. -/
6222 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6223 (hker_mul :
6225 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
6227 (⟨k * (y : ZCCompletedGroupAlgebra C G),
6233 C hC hForm psi hpsi hker_mul
6238 C hC hForm psi hpsi hker_mul
6239 exact
6242 C psi.toMonoidHom
6245 C hC hForm psi hpsi hker_mul)
6247@[simp 900]
6253 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6254 (hker_mul :
6256 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
6258 (⟨k * (y : ZCCompletedGroupAlgebra C G),
6262 (g : G) :
6264 C hC hForm psi hpsi hker_mul
6265 (zcUniversalDifferential C psi.toMonoidHom g) =
6269 C hC hForm psi hpsi hker_mul
6270 exact
6273 C psi.toMonoidHom
6276 C hC hForm psi hpsi hker_mul) g
6278/-- The algebraic map `A_psi(C) -> I(G) / I(ker psi) I(G)` is onto once the algebraic quotient has
6279the completed target scalar action supplied by the explicit kernel-product hypothesis. -/
6285 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6286 (hker_mul :
6288 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
6290 (⟨k * (y : ZCCompletedGroupAlgebra C G),
6294 Function.Surjective
6296 C hC hForm psi hpsi hker_mul) := by
6299 C hC hForm psi hpsi hker_mul
6300 intro x
6301 refine Submodule.Quotient.induction_on
6303 intro y
6304 let L :=
6306 C hC hForm psi hpsi hker_mul
6308 ∃ m : ZCCompletedDifferentialModule C psi.toMonoidHom,
6309 L m = Submodule.Quotient.mk
6311 have hy : P y := by
6312 have hyspan : (y : ZCCompletedGroupAlgebra C G) ∈
6313 Submodule.span (ZCCompletedGroupAlgebra C G)
6314 (Set.range fun h : G => zcGroupLike C G h - 1) := by
6315 change (y : ZCCompletedGroupAlgebra C G) ∈
6317 exact y.2
6318 refine Submodule.span_induction
6319 (p := fun z hz =>
6321 ⟨z, by
6323 ?hgen ?hzero ?hadd ?hsmul hyspan
6324 · rintro _ ⟨g, rfl
6325 refine ⟨zcUniversalDifferential C psi.toMonoidHom g, ?_⟩
6327 rfl
6328 · refine ⟨0, ?_⟩
6330 Submodule.Quotient.mk
6333 rw [Submodule.Quotient.mk_zero]
6334 · intro a b ha hb hpa hpb
6335 rcases hpa with ⟨ma, hma⟩
6336 rcases hpb with ⟨mb, hmb⟩
6337 refine ⟨ma + mb, ?_⟩
6338 rw [map_add, hma, hmb, ← Submodule.Quotient.mk_add]
6340 Submodule.Quotient.mk
6342 exact Subtype.ext rfl
6343 · intro a b hb hpb
6344 rcases hpb with ⟨m, hm⟩
6345 refine ⟨zcCompletedGroupAlgebraMap C hC psi a • m, ?_⟩
6346 rw [map_smul, hm]
6347 calc
6349 Submodule.Quotient.mk
6351 ⟨b, by
6353 a •
6354 Submodule.Quotient.mk
6356 ⟨b, by
6358 exact
6360 C hC hForm psi hpsi hker_mul a
6361 (Submodule.Quotient.mk
6363 ⟨b, by
6365 _ = Submodule.Quotient.mk
6367 ⟨a • b, by
6369 exact Submodule.smul_mem
6370 (Submodule.span (ZCCompletedGroupAlgebra C G)
6371 (Set.range fun h : G => zcGroupLike C G h - 1)) a hb⟩ := by
6372 rw [← Submodule.Quotient.mk_smul]
6374 Submodule.Quotient.mk
6376 exact Subtype.ext rfl
6377 exact hy
6379/-- Under the explicit kernel-product hypothesis, the natural map from the algebraic source
6380augmentation quotient to the closed quotient is `Z_C[[H]]`-linear. -/
6386 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6387 (hfopen : IsOpenMap psi)
6388 (hker_mul :
6390 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
6392 (⟨k * (y : ZCCompletedGroupAlgebra C G),
6398 C hC hForm psi hpsi hker_mul
6399 letI : Module (ZCCompletedGroupAlgebra C H)
6400 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
6402 C hC hForm psi hpsi hfopen
6404 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
6407 C hC hForm psi hpsi hker_mul
6408 letI : Module (ZCCompletedGroupAlgebra C H)
6409 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
6411 C hC hForm psi hpsi hfopen
6412 let Q :=
6414 C hC hForm psi hpsi hfopen
6415 refine
6416 { toFun := Q
6417 map_add' := by
6418 intro x y
6419 exact map_add Q x y
6420 map_smul' := by
6421 intro a x
6422 change Q
6423 (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a • x) =
6424 a • Q x
6426 symm
6427 calc
6428 a • Q x =
6431 Q x := by
6433 _ =
6434 zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a • Q x := by
6435 exact
6437 C hC hForm psi hpsi hfopen
6439 (Q x) }
6441@[simp 900]
6447 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6448 (hfopen : IsOpenMap psi)
6449 (hker_mul :
6451 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
6453 (⟨k * (y : ZCCompletedGroupAlgebra C G),
6459 C hC hForm psi hpsi hfopen hker_mul (Submodule.Quotient.mk x) =
6460 (Submodule.Quotient.mk x :
6461 KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) := by
6464 C hC hForm psi hpsi hker_mul
6465 letI : Module (ZCCompletedGroupAlgebra C H)
6466 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
6468 C hC hForm psi hpsi hfopen
6470 exact
6472 C hC hForm psi hpsi hfopen x
6474/-- The algebraic quotient map followed by the natural closed-quotient map is the closed quotient
6475map already constructed directly from `A_psi(C)`. -/
6481 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6482 (hfopen : IsOpenMap psi)
6483 (hker_mul :
6485 k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
6487 (⟨k * (y : ZCCompletedGroupAlgebra C G),
6492 C hC hForm psi hpsi hfopen hker_mul).comp
6494 C hC hForm psi hpsi hker_mul) =
6496 C hC hForm psi hpsi hfopen := by
6499 C hC hForm psi hpsi hker_mul
6500 letI : Module (ZCCompletedGroupAlgebra C H)
6501 (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
6503 C hC hForm psi hpsi hfopen
6505 intro g
6506 calc
6508 C hC hForm psi hpsi hfopen hker_mul).comp
6510 C hC hForm psi hpsi hker_mul))
6511 (zcUniversalDifferential C psi.toMonoidHom g)
6514 C hC hForm psi hpsi hfopen hker_mul
6516 rw [LinearMap.comp_apply,
6518 _ =
6520 C hC hForm psi hpsi hfopen g := by
6522 exact
6524 C hC hForm psi hpsi hfopen hker_mul
6525zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
6527 C G (MonoidHom.id G) g⟩
6528 _ =
6530 C hC hForm psi hpsi hfopen
6531 (zcUniversalDifferential C psi.toMonoidHom g) := by
6534/-- If the product `I(ker psi) I(G)` is closed, the source boundary is a crossed differential
6535for the descended completed target scalars. -/
6541 (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
6542 (hfopen : IsOpenMap psi)
6543 (hclosed :
6544 IsClosed
6549 C hC hForm psi hpsi hfopen hclosed
6553 let hker_mul :=
6555 C hC hForm psi hpsi hfopen hclosed
6558 C hC hForm psi hpsi hker_mul
6559 exact
6561 C hC hForm psi hpsi hker_mul
6563/-- Source kernel group-like differences act trivially on `A_psi(C)` after restricting scalars
6564along `Z_C[[G]] -> Z_C[[H]]`. -/
6566 (hC : ProCGroups.FiniteGroupClass.Hereditary C) (psi : ContinuousMonoidHom G H)
6567 (n : ProfiniteKernelSubgroup psi) (x : ZCCompletedDifferentialModule C psi.toMonoidHom) :
6568 letI : Module (ZCCompletedGroupAlgebra C G)
6569 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
6570 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
6571 (zcGroupLike C G n.1 - 1) • x = 0 := by
6572 letI : Module (ZCCompletedGroupAlgebra C G)
6573 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
6574 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
6575 have hmap :
6576 zcCompletedGroupAlgebraMap C hC psi (zcGroupLike C G n.1 - 1) = 0 := by
6578 rw [show psi (n : G) = 1 from n.2]
6579 rw [map_one, sub_self]
6580 change zcCompletedGroupAlgebraMap C hC psi (zcGroupLike C G n.1 - 1) • x = 0
6581 rw [hmap, zero_smul]
6583/-- The algebraic product `I(ker psi) I(G)` acts trivially on `A_psi(C)` after restricting
6584scalars along `Z_C[[G]] -> Z_C[[H]]`. -/
6586 (hC : ProCGroups.FiniteGroupClass.Hereditary C) (psi : ContinuousMonoidHom G H)
6589 (x : ZCCompletedDifferentialModule C psi.toMonoidHom) :
6590 letI : Module (ZCCompletedGroupAlgebra C G)
6591 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
6592 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
6593 (y : ZCCompletedGroupAlgebra C G) • x = 0 := by
6594 letI : Module (ZCCompletedGroupAlgebra C G)
6595 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
6596 Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
6597 change (y : ZCCompletedGroupAlgebra C G) • x = 0
6598 refine Submodule.span_induction
6600 fun _ => (y : ZCCompletedGroupAlgebra C G) • x = 0) ?_ ?_ ?_ ?_ hy
6601 · rintro _ ⟨⟨n, s⟩, rfl
6602 change ((zcGroupLike C G n.1 - 1) * (s : ZCCompletedGroupAlgebra C G)) • x = 0
6603 rw [mul_smul]
6605 C hC psi n ((s : ZCCompletedGroupAlgebra C G) • x)
6606 · change (0 : ZCCompletedGroupAlgebra C G) • x = 0
6607 rw [zero_smul]
6608 · intro y z _ _ hy hz
6609 change ((y : ZCCompletedGroupAlgebra C G) +
6610 (z : ZCCompletedGroupAlgebra C G)) • x = 0
6611 rw [add_smul, hy, hz, zero_add]
6612 · intro a y _ hy
6613 change (a * (y : ZCCompletedGroupAlgebra C G)) • x = 0
6614 rw [mul_smul, hy, smul_zero]
6616end KernelAugmentationQuotient
6618end
6620end FoxDifferential