CompletedGroupAlgebra/Augmentation/StageAugmentation.lean
1import CompletedGroupAlgebra.InClassFunctoriality.UnitRepresentation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Augmentation/StageAugmentation.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Augmentation and augmentation ideals
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]
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33/-- The augmentation map on one `C`-indexed finite stage. -/
35 (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
36 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
37 (U : CompletedGroupAlgebraIndexInClass G C) :
38 CompletedGroupAlgebraStageInClass C R G U →+* R :=
39 groupAlgebraAugmentation R (CompletedGroupAlgebraQuotientInClass G C U)
41/-- The in-class finite-stage augmentation sends every group-like basis element to one. -/
42@[simp]
44 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
45 (q : CompletedGroupAlgebraQuotientInClass G C U) :
46 completedGroupAlgebraStageAugmentationInClass C R G U (MonoidAlgebra.of R _ q) = 1 := by
47 simp only [completedGroupAlgebraStageAugmentationInClass, MonoidAlgebra.of_apply,
50/-- The in-class finite-stage augmentation sends a singleton to its coefficient. -/
51@[simp]
53 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
54 (q : CompletedGroupAlgebraQuotientInClass G C U) (r : R) :
55 completedGroupAlgebraStageAugmentationInClass C R G U (MonoidAlgebra.single q r) = r := by
58/-- In-class finite-stage augmentations are compatible with transition maps. -/
59@[simp]
61 (C : ProCGroups.FiniteGroupClass.{v})
62 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
63 (completedGroupAlgebraStageAugmentationInClass C R G U).comp
64 (completedGroupAlgebraTransitionInClass C R G hUV) =
65 completedGroupAlgebraStageAugmentationInClass C R G V := by
66 apply RingHom.ext
67 intro x
69 (CompletedGroupAlgebraQuotientInClass G C V)
70 (CompletedGroupAlgebraQuotientInClass G C U)
71 (OpenNormalSubgroupInClass.map
72 (C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) x
74/-- In-class finite-stage augmentation after the stage map is the abstract augmentation. -/
75@[simp]
77 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
78 (completedGroupAlgebraStageAugmentationInClass C R G U).comp
79 (completedGroupAlgebraStageMapInClass C R G U) =
80 groupAlgebraAugmentation R G := by
81 apply RingHom.ext
82 intro x
83 exact groupAlgebraAugmentation_mapDomainRingHom R G
84 (CompletedGroupAlgebraQuotientInClass G C U)
85 (openNormalSubgroupInClassProj (C := C) (G := G) U) x
87/-- In-class finite-stage augmentation is natural in the coefficient ring. -/
88@[simp]
90 (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S]
91 (f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C) :
92 (completedGroupAlgebraStageAugmentationInClass C S G U).comp
93 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U) =
94 f.comp (completedGroupAlgebraStageAugmentationInClass C R G U) := by
95 apply RingHom.ext
96 intro x
97 exact groupAlgebraAugmentation_mapRangeRingHom R S
98 (CompletedGroupAlgebraQuotientInClass G C U) f x
100/-- In-class finite-stage augmentation is natural for functorial finite-stage maps. -/
101@[simp]
103 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
104 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
105 (completedGroupAlgebraStageAugmentationInClass C R H V).comp
107 (G := G) (H := H) C hHer (R := R) φ hφ V) =
109 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) := by
110 apply RingHom.ext
111 intro x
113 (CompletedGroupAlgebraQuotientInClass G C
114 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
115 (CompletedGroupAlgebraQuotientInClass H C V)
116 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V) x
118end