Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed
1import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Abstract
3/-!
4# Augmentation after completion
6An algebraic augmentation compatible with the completion map extends uniquely to a continuous
7augmentation of the completed group algebra. This file constructs that map, its kernel ideal and
8short exact sequence, and the finite-group-algebra instance.
9-/
11open scoped Topology
12open ProCGroups
14namespace CompletedGroupAlgebra
16universe u v w z
18/-- The coefficient map \(R \to R[G]\) attached to a dense map from the abstract group algebra. -/
19noncomputable def completedGroupAlgebraCoefficientMap
20 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
21 (dense : RingHom (MonoidAlgebra R G) RG) : RingHom R RG :=
22 dense.comp (algebraMap R (MonoidAlgebra R G))
24/--
25The coefficient-change map is evaluated coordinatewise: the support in the finite quotient is
26unchanged and every coefficient is carried through the given ring homomorphism.
27-/
28@[simp]
29theorem completedGroupAlgebraCoefficientMap_apply
30 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
31 (dense : RingHom (MonoidAlgebra R G) RG) (r : R) :
32 completedGroupAlgebraCoefficientMap R G RG dense r =
33 dense (algebraMap R (MonoidAlgebra R G) r) :=
34 rfl
36/--
37A completed group algebra model has a continuous augmentation when its dense abstract
38group-algebra map admits a continuous extension of the abstract augmentation.
39-/
40def hasCompletedGroupAlgebraAugmentation
41 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
42 [Group G] [Ring RG] [TopologicalSpace RG]
43 (dense : RingHom (MonoidAlgebra R G) RG) : Prop :=
44 Exists fun ε : RingHom RG R =>
45 And (ε.comp dense = groupAlgebraAugmentation R G) (Continuous ε)
47/-- The continuous augmentation extracted from completed group algebra augmentation data. -/
48noncomputable def completedGroupAlgebraAugmentation
49 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
50 [Group G] [Ring RG] [TopologicalSpace RG]
51 {dense : RingHom (MonoidAlgebra R G) RG}
52 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) : RingHom RG R :=
53 Classical.choose haug
55/-- The completed augmentation extends the abstract augmentation along the dense algebraic map. -/
56theorem completedGroupAlgebraAugmentation_comp_dense
57 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
58 [Group G] [Ring RG] [TopologicalSpace RG]
59 {dense : RingHom (MonoidAlgebra R G) RG}
60 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
61 (completedGroupAlgebraAugmentation R G RG haug).comp dense =
62 groupAlgebraAugmentation R G :=
63 (Classical.choose_spec haug).1
65/-- The augmentation extracted from the completed augmentation package is continuous. -/
66theorem continuous_completedGroupAlgebraAugmentation
67 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
68 [Group G] [Ring RG] [TopologicalSpace RG]
69 {dense : RingHom (MonoidAlgebra R G) RG}
70 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
71 Continuous (completedGroupAlgebraAugmentation R G RG haug) :=
72 (Classical.choose_spec haug).2
74/-- The coefficient map is a section of the completed augmentation. -/
75theorem completedGroupAlgebraAugmentation_comp_coefficientMap
76 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
77 [Group G] [Ring RG] [TopologicalSpace RG]
78 {dense : RingHom (MonoidAlgebra R G) RG}
79 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
80 (completedGroupAlgebraAugmentation R G RG haug).comp
81 (completedGroupAlgebraCoefficientMap R G RG dense) = RingHom.id R := by
82 ext r
83 have h := congrArg
84 (fun f : RingHom (MonoidAlgebra R G) R => f (algebraMap R (MonoidAlgebra R G) r))
85 (completedGroupAlgebraAugmentation_comp_dense R G RG haug)
86 simpa [completedGroupAlgebraCoefficientMap] using h
88/-- The augmentation ideal of a completed group algebra model with augmentation data. -/
89noncomputable def completedGroupAlgebraAugmentationIdeal
90 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
91 [Group G] [Ring RG] [TopologicalSpace RG]
92 {dense : RingHom (MonoidAlgebra R G) RG}
93 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) : Ideal RG :=
94 RingHom.ker (completedGroupAlgebraAugmentation R G RG haug)
96/--
97A completed finite group-algebra element lies in the completed augmentation ideal iff its
98completed augmentation is zero.
99-/
100@[simp]
101theorem mem_completedGroupAlgebraAugmentationIdeal_iff
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. -/
111theorem completedGroupAlgebraAugmentation_surjective
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/--
124The inclusion of the completed augmentation ideal into the completed group algebra model is
125injective.
126-/
127theorem completedGroupAlgebraAugmentationIdeal_subtype_injective
128 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
129 [Group G] [Ring RG] [TopologicalSpace RG]
130 {dense : RingHom (MonoidAlgebra R G) RG}
131 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
132 Function.Injective
133 (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG)) := by
134 intro x y hxy
135 exact Subtype.ext hxy
137/-- The completed augmentation ideal is exactly the kernel of the completed augmentation. -/
138theorem exact_completedGroupAlgebraAugmentationIdeal_subtype
139 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
140 [Group G] [Ring RG] [TopologicalSpace RG]
141 {dense : RingHom (MonoidAlgebra R G) RG}
142 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
143 Function.Exact
144 (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG))
145 (completedGroupAlgebraAugmentation R G RG haug) := by
146 intro x
147 constructor
148 · intro hx
149 exact ⟨⟨x, hx⟩, rfl⟩
150 · rintro ⟨y, rfl⟩
151 exact y.2
153/--
154For the completed augmentation data `haug`, the subtype inclusion of its augmentation ideal into
155\(RG\), followed by the completed augmentation, is a short exact sequence.
156-/
157theorem completedGroupAlgebraAugmentation_shortExact
158 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
159 [Group G] [Ring RG] [TopologicalSpace RG]
160 {dense : RingHom (MonoidAlgebra R G) RG}
161 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
162 Function.Injective
163 (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG)) ∧
164 Function.Exact
165 (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG))
166 (completedGroupAlgebraAugmentation R G RG haug) ∧
167 Function.Surjective (completedGroupAlgebraAugmentation R G RG haug) := by
168 exact ⟨completedGroupAlgebraAugmentationIdeal_subtype_injective R G RG haug,
169 exact_completedGroupAlgebraAugmentationIdeal_subtype R G RG haug,
170 completedGroupAlgebraAugmentation_surjective R G RG haug⟩
172/--
173In the finite-group case, the finite group algebra carries the completed augmentation data
174induced by the ordinary augmentation.
175-/
176theorem finiteGroupAlgebra_hasCompletedGroupAlgebraAugmentation
177 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
178 [Group G] [Finite G] :
179 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
180 hasCompletedGroupAlgebraAugmentation R G (MonoidAlgebra R G)
181 (RingHom.id (MonoidAlgebra R G)) := by
182 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
183 refine Exists.intro (groupAlgebraAugmentation R G) ?_
184 exact And.intro (RingHom.comp_id (groupAlgebraAugmentation R G))
185 (finiteGroupAlgebra_augmentation_continuous R G)
187end CompletedGroupAlgebra