CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Augmentation/Completed.lean
1import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Abstract
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Augmentation/Completed.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 packages for completed group algebra models
14This module transports finite-stage augmentation packages to completed group-algebra models and their augmentation ideals.
15-/
17open scoped Topology
18open ProCGroups
20namespace CompletedGroupAlgebra
22universe u v w z
24/-- The coefficient map `R → RG` attached to a dense map from the abstract group
25algebra. -/
26noncomputable def completedGroupAlgebraCoefficientMap
27 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
28 (dense : RingHom (MonoidAlgebra R G) RG) : RingHom R RG :=
29 dense.comp (algebraMap R (MonoidAlgebra R G))
31/-- The completed coefficient map is the dense map applied to coefficient scalars. -/
32@[simp]
34 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
35 (dense : RingHom (MonoidAlgebra R G) RG) (r : R) :
36 completedGroupAlgebraCoefficientMap R G RG dense r =
37 dense (algebraMap R (MonoidAlgebra R G) r) :=
38 rfl
40/-- A completed group algebra model has a continuous augmentation when its dense abstract
43 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
44 [Group G] [Ring RG] [TopologicalSpace RG]
45 (dense : RingHom (MonoidAlgebra R G) RG) : Prop :=
46 Exists fun ε : RingHom RG R =>
47 And (ε.comp dense = groupAlgebraAugmentation R G) (Continuous ε)
49/-- The continuous augmentation extracted from completed group algebra augmentation data. -/
50noncomputable def completedGroupAlgebraAugmentation
51 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
52 [Group G] [Ring RG] [TopologicalSpace RG]
53 {dense : RingHom (MonoidAlgebra R G) RG}
54 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) : RingHom RG R :=
55 Classical.choose haug
57/-- The completed augmentation extends the abstract augmentation along the dense map. -/
59 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
60 [Group G] [Ring RG] [TopologicalSpace RG]
61 {dense : RingHom (MonoidAlgebra R G) RG}
62 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
63 (completedGroupAlgebraAugmentation R G RG haug).comp dense =
64 groupAlgebraAugmentation R G :=
65 (Classical.choose_spec haug).1
67/-- The augmentation extracted from the completed augmentation package is continuous. -/
69 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
70 [Group G] [Ring RG] [TopologicalSpace RG]
71 {dense : RingHom (MonoidAlgebra R G) RG}
72 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
73 Continuous (completedGroupAlgebraAugmentation R G RG haug) :=
74 (Classical.choose_spec haug).2
76/-- The coefficient map is a section of the completed augmentation. -/
78 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
79 [Group G] [Ring RG] [TopologicalSpace RG]
80 {dense : RingHom (MonoidAlgebra R G) RG}
81 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
82 (completedGroupAlgebraAugmentation R G RG haug).comp
83 (completedGroupAlgebraCoefficientMap R G RG dense) = RingHom.id R := by
84 ext r
85 have h := congrArg
86 (fun f : RingHom (MonoidAlgebra R G) R => f (algebraMap R (MonoidAlgebra R G) r))
87 (completedGroupAlgebraAugmentation_comp_dense R G RG haug)
88 simpa [completedGroupAlgebraCoefficientMap] using h
90/-- The augmentation ideal of a completed group algebra model with augmentation data. -/
91noncomputable def completedGroupAlgebraAugmentationIdeal
92 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
93 [Group G] [Ring RG] [TopologicalSpace RG]
94 {dense : RingHom (MonoidAlgebra R G) RG}
95 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) : Ideal RG :=
96 RingHom.ker (completedGroupAlgebraAugmentation R G RG haug)
98/-- Membership in the completed augmentation ideal is the vanishing of the completed
99augmentation. -/
100@[simp]
102 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
103 [Group G] [Ring RG] [TopologicalSpace RG]
104 {dense : RingHom (MonoidAlgebra R G) RG}
105 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) (x : RG) :
106 x ∈ completedGroupAlgebraAugmentationIdeal R G RG haug ↔
107 completedGroupAlgebraAugmentation R G RG haug x = 0 :=
108 Iff.rfl
110/-- The completed augmentation is split by the completed coefficient map. -/
112 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
113 [Group G] [Ring RG] [TopologicalSpace RG]
114 {dense : RingHom (MonoidAlgebra R G) RG}
115 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
116 Function.Surjective (completedGroupAlgebraAugmentation R G RG haug) := by
117 intro r
118 refine ⟨completedGroupAlgebraCoefficientMap R G RG dense r, ?_⟩
119 have h := congrArg (fun f : RingHom R R => f r)
120 (completedGroupAlgebraAugmentation_comp_coefficientMap R G RG haug)
121 simpa using h
123/-- The inclusion of the completed augmentation ideal into the completed group algebra model is
124injective. -/
126 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
127 [Group G] [Ring RG] [TopologicalSpace RG]
128 {dense : RingHom (MonoidAlgebra R G) RG}
129 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
130 Function.Injective
131 (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG)) := by
132 intro x y hxy
133 exact Subtype.ext hxy
135/-- The completed augmentation ideal is exactly the kernel of the completed augmentation. -/
137 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
138 [Group G] [Ring RG] [TopologicalSpace RG]
139 {dense : RingHom (MonoidAlgebra R G) RG}
140 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
141 Function.Exact
142 (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG))
143 (completedGroupAlgebraAugmentation R G RG haug) := by
144 intro x
145 constructor
146 · intro hx
147 exact ⟨⟨x, hx⟩, rfl⟩
148 · rintro ⟨y, rfl⟩
149 exact y.2
151/-- Any completed group algebra model with augmentation data has a short exact augmentation
152sequence `0 → I_G → [[R G]] → R → 0`. -/
154 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
155 [Group G] [Ring RG] [TopologicalSpace RG]
156 {dense : RingHom (MonoidAlgebra R G) RG}
157 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
158 Function.Injective
159 (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG)) ∧
160 Function.Exact
161 (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG))
162 (completedGroupAlgebraAugmentation R G RG haug) ∧
163 Function.Surjective (completedGroupAlgebraAugmentation R G RG haug) := by
164 exact ⟨completedGroupAlgebraAugmentationIdeal_subtype_injective R G RG haug,
165 exact_completedGroupAlgebraAugmentationIdeal_subtype R G RG haug,
166 completedGroupAlgebraAugmentation_surjective R G RG haug⟩
168/-- In the finite-group case, the finite group algebra has the expected completed augmentation
169data. -/
171 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
172 [Group G] [Finite G] :
173 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
174 hasCompletedGroupAlgebraAugmentation R G (MonoidAlgebra R G)
175 (RingHom.id (MonoidAlgebra R G)) := by
176 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
177 refine Exists.intro (groupAlgebraAugmentation R G) ?_
178 exact And.intro (RingHom.comp_id (groupAlgebraAugmentation R G))