Source: ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.AugmentationIdeal
1import ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.InClassComparison
2import ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Surjectivity
3import ProCGroups.CompletedGroupAlgebra.Augmentation.AugmentationIdeal
5/-!
6# The canonical augmentation ideal
8This file defines the kernel of the canonical augmentation on the all-finite completed group
9algebra, packages its short exact sequence, and proves comparison and functoriality formulas for
10the ideal.
11-/
13open scoped Topology
15namespace CompletedGroupAlgebra
17noncomputable section
19open ProCGroups
20open ProCGroups.ProC
21open ProCGroups.InverseSystems
22open ProCGroups.Completion
24universe u v w
26variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
27variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30/--
31The canonical augmentation ideal \(I_G\subseteq \widehat{R[G]}\) is the kernel of the completed
32augmentation \(\varepsilon:\widehat{R[G]}\to R\).
33-/
34def completedGroupAlgebraCanonicalAugmentationIdeal (R : Type u) (G : Type v) [CommRing R]
35 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
36 [IsTopologicalGroup G] : Ideal (CompletedGroupAlgebraCarrier R G) :=
37 RingHom.ker (completedGroupAlgebraCanonicalAugmentation R G)
39/--
40An all-finite completed group-algebra element lies in the canonical augmentation ideal iff the
41canonical augmentation sends it to zero.
42-/
43@[simp]
44theorem mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff
45 {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R]
46 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
47 {x : CompletedGroupAlgebraCarrier R G} :
48 x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G ↔
49 completedGroupAlgebraCanonicalAugmentation R G x = 0 :=
50 Iff.rfl
52/-- The inclusion of the canonical completed augmentation ideal is injective. -/
53theorem completedGroupAlgebraCanonicalAugmentationIdeal_subtype_injective :
54 Function.Injective
55 (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
56 (x : CompletedGroupAlgebraCarrier R G)) := by
57 intro x y hxy
58 exact Subtype.ext hxy
60/--
61The canonical completed augmentation ideal is exactly the kernel of the canonical augmentation.
62-/
63theorem exact_completedGroupAlgebraCanonicalAugmentationIdeal_subtype :
64 Function.Exact
65 (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
66 (x : CompletedGroupAlgebraCarrier R G))
67 (completedGroupAlgebraCanonicalAugmentation R G) := by
68 intro x
69 constructor
70 · intro hx
71 exact ⟨⟨x, hx⟩, rfl⟩
72 · rintro ⟨y, rfl⟩
73 exact y.2
75/--
76The canonical augmentation sequence with augmentation ideal as kernel is short exact: the
77inclusion is injective, its image is the kernel of augmentation, and the augmentation is
78surjective.
79-/
80theorem completedGroupAlgebraCanonicalAugmentation_shortExact :
81 Function.Injective
82 (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
83 (x : CompletedGroupAlgebraCarrier R G)) ∧
84 Function.Exact
85 (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
86 (x : CompletedGroupAlgebraCarrier R G))
87 (completedGroupAlgebraCanonicalAugmentation R G) ∧
88 Function.Surjective (completedGroupAlgebraCanonicalAugmentation R G) := by
89 exact ⟨completedGroupAlgebraCanonicalAugmentationIdeal_subtype_injective (R := R) (G := G),
90 exact_completedGroupAlgebraCanonicalAugmentationIdeal_subtype (R := R) (G := G),
91 completedGroupAlgebraCanonicalAugmentation_surjective (R := R) (G := G)⟩
93/--
94The all-finite augmentation ideal pulls back along the from-in-class comparison map to the
95class-indexed augmentation ideal.
96-/
97@[simp]
98theorem completedGroupAlgebraCanonicalAugmentationIdeal_comap_fromInClass
99 (C : ProCGroups.FiniteGroupClass.{v})
101 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
102 Ideal.comap (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)
103 (completedGroupAlgebraCanonicalAugmentationIdeal R G) =
104 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C := by
105 ext x
106 rw [Ideal.mem_comap, mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff,
107 mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff,
108 completedGroupAlgebraFromInClassRingHom_apply,
109 completedGroupAlgebraCanonicalAugmentation_fromInClass]
111/--
112The from-in-class comparison map sends the class-indexed augmentation ideal into the all-finite
113augmentation ideal.
114-/
115@[simp]
116theorem completedGroupAlgebraCanonicalAugmentationIdealInClass_map_fromInClass
117 (C : ProCGroups.FiniteGroupClass.{v})
119 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
120 Ideal.map (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)
121 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ) =
122 completedGroupAlgebraCanonicalAugmentationIdeal R G := by
123 rw [← completedGroupAlgebraCanonicalAugmentationIdeal_comap_fromInClass
124 (R := R) (G := G) C hForm hG]
125 exact Ideal.map_comap_of_surjective
126 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)
127 (completedGroupAlgebraFromInClass_surjective (R := R) (G := G) C hForm hG)
128 (completedGroupAlgebraCanonicalAugmentationIdeal R G)
130/--
131The all-finite-to-in-class comparison map preserves and reflects membership in the canonical
132augmentation ideal.
133-/
134@[simp]
135theorem completedGroupAlgebraToInClass_mem_canonicalAugmentationIdeal_iff
136 {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R]
137 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
138 (C : ProCGroups.FiniteGroupClass.{v})
140 {x : CompletedGroupAlgebraCarrier R G} :
141 completedGroupAlgebraToInClassRingHom (R := R) (G := G) C x ∈
142 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ↔
143 x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G := by
144 rw [mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff,
145 mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff]
146 have haug := congrFun
147 (congrArg DFunLike.coe
148 (completedGroupAlgebraCanonicalAugmentationInClass_comp_toInClass
149 (R := R) (G := G) C ))
150 x
151 change completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
152 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C x) =
153 completedGroupAlgebraCanonicalAugmentation R G x at haug
154 rw [haug]
156/--
157The class-indexed augmentation ideal pulls back along the to-in-class comparison map to the
158all-finite augmentation ideal.
159-/
160@[simp]
161theorem completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_toInClass
162 (C : ProCGroups.FiniteGroupClass.{v})
164 Ideal.comap (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
165 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ) =
166 completedGroupAlgebraCanonicalAugmentationIdeal R G := by
167 ext x
168 exact completedGroupAlgebraToInClass_mem_canonicalAugmentationIdeal_iff
169 (R := R) (G := G) C
171/--
172The to-in-class comparison map sends the all-finite augmentation ideal into the class-indexed
173augmentation ideal.
174-/
175@[simp]
176theorem completedGroupAlgebraCanonicalAugmentationIdeal_map_toInClass
177 (C : ProCGroups.FiniteGroupClass.{v})
179 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
180 Ideal.map (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
181 (completedGroupAlgebraCanonicalAugmentationIdeal R G) =
182 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C := by
183 rw [← completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_toInClass
184 (R := R) (G := G) C ]
185 exact Ideal.map_comap_of_surjective
186 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
187 (completedGroupAlgebraToInClass_surjective (R := R) (G := G) C hForm hG)
188 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C )
190/--
191A functorial all-finite completed group-algebra map sends augmentation generators to their
192images.
193-/
194@[simp]
195theorem completedGroupAlgebraMap_sub_one_of
196 (φ : G →* H) (hφ : Continuous φ) (g : G) :
197 completedGroupAlgebraMap (G := G) (H := H) R φ hφ
198 (completedGroupAlgebraOf R G g - 1) =
199 completedGroupAlgebraOf R H (φ g) - 1 := by
200 rw [map_sub, completedGroupAlgebraMap_of, map_one]
202/--
203A functorial all-finite completed group-algebra map preserves and reflects membership in the
204canonical augmentation ideal.
205-/
206@[simp]
207theorem completedGroupAlgebraMap_mem_canonicalAugmentationIdeal_iff
208 {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R]
209 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
210 (φ : G →* H) (hφ : Continuous φ)
211 {x : CompletedGroupAlgebraCarrier R G} :
212 completedGroupAlgebraMap (G := G) (H := H) R φ hφ x ∈
213 completedGroupAlgebraCanonicalAugmentationIdeal R H ↔
214 x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G := by
215 rw [mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff,
216 mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff,
217 completedGroupAlgebraCanonicalAugmentation_map]
219/--
220Pulling back the target canonical augmentation ideal along a completed group-algebra map gives
221the source canonical augmentation ideal.
222-/
223@[simp]
224theorem completedGroupAlgebraCanonicalAugmentationIdeal_comap_map
225 (φ : G →* H) (hφ : Continuous φ) :
226 Ideal.comap (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)
227 (completedGroupAlgebraCanonicalAugmentationIdeal R H) =
228 completedGroupAlgebraCanonicalAugmentationIdeal R G := by
229 ext x
230 exact completedGroupAlgebraMap_mem_canonicalAugmentationIdeal_iff
231 (R := R) (G := G) (H := H) φ hφ
233/--
234A surjective functorial map sends the canonical completed augmentation ideal onto the target
235canonical augmentation ideal.
236-/
237theorem completedGroupAlgebraCanonicalAugmentationIdeal_map_functorial_of_surjective
238 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
239 (φ : G →* H) (hφ : Continuous φ)
240 (hφsurj : Function.Surjective φ) :
241 Ideal.map (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)
242 (completedGroupAlgebraCanonicalAugmentationIdeal R G) =
243 completedGroupAlgebraCanonicalAugmentationIdeal R H := by
244 rw [← completedGroupAlgebraCanonicalAugmentationIdeal_comap_map
245 (R := R) (G := G) (H := H) φ hφ]
246 exact Ideal.map_comap_of_surjective
247 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)
248 (completedGroupAlgebraMap_surjective_of_surjective
249 (R := R) (G := G) (H := H) φ hφ hφsurj)
250 (completedGroupAlgebraCanonicalAugmentationIdeal R H)
251end
253end CompletedGroupAlgebra