Source: ProCGroups.CompletedGroupAlgebra.Augmentation.AugmentationIdeal
1import ProCGroups.CompletedGroupAlgebra.Augmentation.CanonicalAugmentation
3/-!
4# The in-class augmentation ideal
6This file defines the kernel of the canonical augmentation on the in-class completed group
7algebra, establishes the associated short exact sequence, and identifies the ideal through the
8canonical map from the algebraic group algebra.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
19open ProCGroups.InverseSystems
20open ProCGroups.Completion
22universe u v w
24variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
25variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
26variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
28/-- The canonical augmentation ideal of the \(C\)-indexed completed group algebra. -/
29def completedGroupAlgebraCanonicalAugmentationIdealInClass
30 (C : ProCGroups.FiniteGroupClass.{v})
32 Ideal (CompletedGroupAlgebraInClass C R G) :=
33 RingHom.ker (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C )
35/--
36An in-class completed group-algebra element lies in the canonical augmentation ideal iff the
37in-class canonical augmentation sends it to zero.
38-/
39@[simp]
40theorem mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff
41 {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R]
42 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
43 {C : ProCGroups.FiniteGroupClass.{v}}
45 {x : CompletedGroupAlgebraInClass C R G} :
46 x ∈ completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ↔
47 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C x = 0 :=
48 Iff.rfl
50/-- The inclusion of the \(C\)-indexed canonical augmentation ideal is injective. -/
51theorem completedGroupAlgebraCanonicalAugmentationIdealInClass_subtype_injective
52 (C : ProCGroups.FiniteGroupClass.{v})
54 Function.Injective
55 (fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
56 (R := R) (G := G) C => (x : CompletedGroupAlgebraInClass C R G)) := by
57 intro x y hxy
58 exact Subtype.ext hxy
60/--
61The \(C\)-indexed canonical augmentation ideal is exactly the kernel of the canonical
62augmentation.
63-/
64theorem exact_completedGroupAlgebraCanonicalAugmentationIdealInClass_subtype
65 (C : ProCGroups.FiniteGroupClass.{v})
67 Function.Exact
68 (fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
69 (R := R) (G := G) C => (x : CompletedGroupAlgebraInClass C R G))
70 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ) := by
71 intro x
72 constructor
73 · intro hx
74 exact ⟨⟨x, hx⟩, rfl⟩
75 · rintro ⟨y, rfl⟩
76 exact y.2
78/--
79The canonical augmentation sequence with augmentation ideal as kernel is short exact: the
80inclusion is injective, its image is the kernel of augmentation, and the augmentation is
81surjective.
82-/
83theorem completedGroupAlgebraCanonicalAugmentationInClass_shortExact
84 (C : ProCGroups.FiniteGroupClass.{v})
86 Function.Injective
87 (fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
88 (R := R) (G := G) C => (x : CompletedGroupAlgebraInClass C R G)) ∧
89 Function.Exact
90 (fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
91 (R := R) (G := G) C => (x : CompletedGroupAlgebraInClass C R G))
92 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ) ∧
93 Function.Surjective
94 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ) := by
95 exact ⟨completedGroupAlgebraCanonicalAugmentationIdealInClass_subtype_injective
96 (R := R) (G := G) C ,
97 exact_completedGroupAlgebraCanonicalAugmentationIdealInClass_subtype
98 (R := R) (G := G) C ,
99 completedGroupAlgebraCanonicalAugmentationInClass_surjective (R := R) (G := G) C ⟩
101/-- The in-class canonical augmentation sends every completed group-like element to one. -/
102@[simp]
103theorem completedGroupAlgebraCanonicalAugmentationInClass_of
104 (C : ProCGroups.FiniteGroupClass.{v})
105 [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (g : G) :
106 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
107 (completedGroupAlgebraOfInClass C R G g) = 1 := by
108 rw [completedGroupAlgebraOfInClass,
109 canonicalAugmentationInClass_toCompleted]
110 simp only [MonoidAlgebra.of_apply, groupAlgebraAugmentation_single]
112end
114end CompletedGroupAlgebra