CompletedGroupAlgebra/AllFiniteAugmentation/StageAugmentation.lean
1import CompletedGroupAlgebra.AllFiniteAugmentation.TerminalIndex
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/AllFiniteAugmentation/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# 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 augmentation map on one finite stage `R[G/U] -> R`. -/
34def completedGroupAlgebraStageAugmentation (R : Type u) (G : Type v) [CommRing R]
35 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
36 (U : CompletedGroupAlgebraIndex G) :
37 CompletedGroupAlgebraStage R G U →+* R :=
40omit [TopologicalSpace R] [IsTopologicalRing R] in
41/-- The finite-stage augmentation sends every group-like basis element to one. -/
42@[simp]
44 (U : CompletedGroupAlgebraIndex G) (q : CompletedGroupAlgebraQuotient G U) :
45 completedGroupAlgebraStageAugmentation R G U (MonoidAlgebra.of R _ q) = 1 := by
46 simp only [completedGroupAlgebraStageAugmentation, MonoidAlgebra.of_apply, groupAlgebraAugmentation_single]
48omit [TopologicalSpace R] [IsTopologicalRing R] in
49/-- The finite-stage augmentation sends a singleton to its coefficient. -/
50@[simp]
52 (U : CompletedGroupAlgebraIndex G) (q : CompletedGroupAlgebraQuotient G U) (r : R) :
53 completedGroupAlgebraStageAugmentation R G U (MonoidAlgebra.single q r) = r := by
56omit [TopologicalSpace R] [IsTopologicalRing R] in
57/-- Finite-stage augmentations are compatible with transition maps. -/
58@[simp]
60 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
61 (completedGroupAlgebraStageAugmentation R G U).comp
62 (completedGroupAlgebraTransition R G hUV) =
63 completedGroupAlgebraStageAugmentation R G V := by
64 apply RingHom.ext
65 intro x
68 (OpenNormalSubgroupInClass.map
69 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
70 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) x
72omit [TopologicalSpace R] [IsTopologicalRing R] in
73/-- Finite-stage augmentation after the stage map is the abstract group-algebra augmentation. -/
74@[simp]
76 (U : CompletedGroupAlgebraIndex G) :
77 (completedGroupAlgebraStageAugmentation R G U).comp
78 (completedGroupAlgebraStageMap R G U) =
79 groupAlgebraAugmentation R G := by
80 apply RingHom.ext
81 intro x
82 exact groupAlgebraAugmentation_mapDomainRingHom R G (CompletedGroupAlgebraQuotient G U)
84 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U) x
86omit [TopologicalSpace R] [IsTopologicalRing R] in
87/-- Finite-stage augmentation is natural in the coefficient ring. -/
88@[simp]
90 (S : Type w) [CommRing S] (f : R →+* S) (U : CompletedGroupAlgebraIndex G) :
91 (completedGroupAlgebraStageAugmentation S G U).comp
92 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U) =
93 f.comp (completedGroupAlgebraStageAugmentation R G U) := by
94 apply RingHom.ext
95 intro x
96 exact groupAlgebraAugmentation_mapRangeRingHom R S
97 (CompletedGroupAlgebraQuotient G U) f x
99omit [TopologicalSpace R] [IsTopologicalRing R] in
100/-- Finite-stage augmentation is natural with respect to functorial finite-stage maps. -/
101@[simp]
103 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
104 (V : CompletedGroupAlgebraIndex H) :
105 (completedGroupAlgebraStageAugmentation R H V).comp
106 (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V) =
108 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) := by
109 apply RingHom.ext
110 intro x
112 (CompletedGroupAlgebraQuotient G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V))
114 (completedGroupAlgebraComapQuotientMap (G := G) hG φ hφ V) x
115end