CompletedGroupAlgebra/AllFiniteAugmentation/InClassComparison.lean
1import CompletedGroupAlgebra.AllFiniteAugmentation.CanonicalAugmentation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/AllFiniteAugmentation/InClassComparison.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed group algebras
14The completed group algebra is presented as an inverse limit of finite group algebras, together with canonical augmentation, augmentation ideal, finite-stage maps, functoriality, and profinite module universal properties.
15-/
16open scoped Topology
18namespace CompletedGroupAlgebra
20noncomputable section
22open ProCGroups
23open ProCGroups.ProC
24open ProCGroups.InverseSystems
25open ProCGroups.Completion
27universe u v w
29variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33/-- The class-indexed canonical augmentation composed with the comparison map agrees with the
35@[simp 900]
37 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
39 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC).comp
40 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC) =
41 completedGroupAlgebraCanonicalAugmentation R G := by
42 apply RingHom.ext
43 intro x
44 let Uc : CompletedGroupAlgebraIndexInClass G C :=
45 terminalCompletedGroupAlgebraIndexInClass (G := G) C
46 let U : CompletedGroupAlgebraIndex G :=
48 calc
49 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
50 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x)
51 =
52 completedGroupAlgebraAugmentationAtInClass C R G hC Uc
53 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x) := by
55 (R := R) (G := G) C hC Uc
56 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x)
57 _ =
59 (completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC Uc x) := rfl
60 _ =
62 (completedGroupAlgebraProjection R G U x) := rfl
63 _ = completedGroupAlgebraCanonicalAugmentation R G x := by
64 exact (completedGroupAlgebraCanonicalAugmentation_eq_at (R := R) (G := G) U x).symm
66/-- The all-finite canonical augmentation after the comparison map from a class-indexed
67completion agrees with the class-indexed augmentation. -/
68@[simp]
70 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
72 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G)
73 (x : CompletedGroupAlgebraInClass C hC R G) :
75 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x) =
76 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC x := by
77 have h := congrFun
78 (congrArg DFunLike.coe
80 (R := R) (G := G) C hC))
81 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x)
82 change completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
83 (completedGroupAlgebraToInClass (R := R) (G := G) C hC
84 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x)) =
86 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x) at h
87 rw [completedGroupAlgebraToInClass_fromInClass] at h
88 exact h.symm
89end