Yamaguchi Lean 4 Library
Source: ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Comparison
ProCGroups/CompletedGroupAlgebra/InClassFunctoriality/Comparison/Source

Source: ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Comparison

1import ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.GroupLike
2import ProCGroups.CompletedGroupAlgebra.UniversalProperty.Basic
4/-!
5# Comparison maps for in-class completions
7This file computes the canonical maps between all-finite and in-class completed group algebras on
8group-like elements and their differences from one. It also records the corresponding formulas
9for functorial maps and restricted scalar actions.
10-/
12open scoped Topology
14namespace CompletedGroupAlgebra
16noncomputable section
18open ProCGroups
19open ProCGroups.ProC
20open ProCGroups.InverseSystems
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/--
29The all-finite completed group algebra comparison sends group-like elements to the \(C\)-indexed
30group-like elements.
31-/
32@[simp]
33theorem completedGroupAlgebraToInClass_of
34 (C : ProCGroups.FiniteGroupClass.{v})
35 (g : G) :
36 completedGroupAlgebraToInClassRingHom (R := R) (G := G) C
37 (completedGroupAlgebraOf R G g) =
38 completedGroupAlgebraOfInClass C R G g := by
39 change ((completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ).comp
40 (toCompletedGroupAlgebraRingHom R G)) (MonoidAlgebra.of R G g) =
41 toCompletedGroupAlgebraInClassRingHom C R G (MonoidAlgebra.of R G g)
42 exact congrFun
43 (congrArg DFunLike.coe
44 (completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra
45 (R := R) (G := G) C ))
46 (MonoidAlgebra.of R G g)
48/--
49The comparison map to a class-indexed completion sends all-finite augmentation generators to
50class-indexed generators.
51-/
52@[simp]
53theorem completedGroupAlgebraToInClass_of_sub_one
54 (C : ProCGroups.FiniteGroupClass.{v})
55 (g : G) :
56 completedGroupAlgebraToInClassRingHom (R := R) (G := G) C
57 (completedGroupAlgebraOf R G g - 1) =
58 completedGroupAlgebraOfInClass C R G g - 1 := by
59 rw [map_sub, completedGroupAlgebraToInClass_of, map_one]
61/--
62After restricting scalars along \(\widehat{R[G]} \to \widehat{R[G]}_C\), the all-finite
63augmentation generator acts as the matching \(C\)-indexed generator.
64-/
65@[simp]
66theorem completedGroupAlgebraToInClass_restrictScalars_sub_one_smul
67 (C : ProCGroups.FiniteGroupClass.{v})
68 (A : Type w) [AddCommGroup A] [Module (CompletedGroupAlgebraInClass C R G) A]
69 (g : G) (a : A) :
70 letI : Module (CompletedGroupAlgebraCarrier R G) A :=
71 Module.compHom A (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
72 (completedGroupAlgebraOf R G g - 1) • a =
73 (completedGroupAlgebraOfInClass C R G g - 1) • a := by
74 letI : Module (CompletedGroupAlgebraCarrier R G) A :=
75 Module.compHom A (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
76 change (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C
77 (completedGroupAlgebraOf R G g - 1)) • a =
78 (completedGroupAlgebraOfInClass C R G g - 1) • a
79 rw [completedGroupAlgebraToInClass_of_sub_one]
81/--
82The comparison map from a class-indexed completion sends class-indexed group-like elements to
83all-finite group-like elements.
84-/
85@[simp]
86theorem completedGroupAlgebraFromInClass_of
87 (C : ProCGroups.FiniteGroupClass.{v})
88 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (g : G) :
89 completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
90 (completedGroupAlgebraOfInClass C R G g) =
91 completedGroupAlgebraOf R G g := by
92 change ((completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG).comp
93 (toCompletedGroupAlgebraInClassRingHom C R G)) (MonoidAlgebra.of R G g) =
94 toCompletedGroupAlgebraRingHom R G (MonoidAlgebra.of R G g)
95 exact congrFun
96 (congrArg DFunLike.coe
97 (completedGroupAlgebraFromInClassRingHom_comp_toCompletedGroupAlgebraInClass
98 (R := R) (G := G) C hForm hG))
99 (MonoidAlgebra.of R G g)
101/--
102The comparison map from a class-indexed completion sends class-indexed augmentation generators
103to all-finite generators.
104-/
105@[simp]
106theorem completedGroupAlgebraFromInClass_of_sub_one
107 (C : ProCGroups.FiniteGroupClass.{v})
108 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (g : G) :
109 completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
110 (completedGroupAlgebraOfInClass C R G g - 1) =
111 completedGroupAlgebraOf R G g - 1 := by
112 change completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG
113 (completedGroupAlgebraOfInClass C R G g - 1) =
114 completedGroupAlgebraOf R G g - 1
115 rw [map_sub, map_one]
116 change completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
117 (completedGroupAlgebraOfInClass C R G g) - 1 =
118 completedGroupAlgebraOf R G g - 1
119 rw [completedGroupAlgebraFromInClass_of]
121/--
122After restricting scalars along \(\widehat{R[G]}_C \to \widehat{R[G]}\), the \(C\)-indexed
123augmentation generator acts as the matching all-finite generator.
124-/
125@[simp]
126theorem completedGroupAlgebraFromInClass_restrictScalars_sub_one_smul
127 (C : ProCGroups.FiniteGroupClass.{v})
128 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)
129 (A : Type w) [AddCommGroup A] [Module (CompletedGroupAlgebraCarrier R G) A]
130 (g : G) (a : A) :
131 letI : Module (CompletedGroupAlgebraInClass C R G) A :=
132 Module.compHom A (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)
133 (completedGroupAlgebraOfInClass C R G g - 1) • a =
134 (completedGroupAlgebraOf R G g - 1) • a := by
135 letI : Module (CompletedGroupAlgebraInClass C R G) A :=
136 Module.compHom A (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)
137 change (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG
138 (completedGroupAlgebraOfInClass C R G g - 1)) • a =
139 (completedGroupAlgebraOf R G g - 1) • a
140 rw [completedGroupAlgebraFromInClassRingHom_apply,
141 completedGroupAlgebraFromInClass_of_sub_one]
143/--
144The class-indexed completed group-algebra map sends the completed group-like element of \(g\) to
145the completed group-like element of its image.
146-/
147@[simp]
148theorem completedGroupAlgebraMapInClass_of
149 (C : ProCGroups.FiniteGroupClass.{v})
151 (φ : G →* H) (hφ : Continuous φ) (g : G) :
152 completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
153 (completedGroupAlgebraOfInClass C R G g) =
154 completedGroupAlgebraOfInClass C R H (φ g) := by
155 simpa [completedGroupAlgebraOfInClass] using
156 completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_of
157 (R := R) (G := G) (H := H) C hHer φ hφ g
159/-- The class-indexed functorial map sends group-like augmentation generators to their images. -/
160@[simp]
161theorem completedGroupAlgebraMapInClass_of_sub_one
162 (C : ProCGroups.FiniteGroupClass.{v})
164 (φ : G →* H) (hφ : Continuous φ) (g : G) :
165 completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
166 (completedGroupAlgebraOfInClass C R G g - 1) =
167 completedGroupAlgebraOfInClass C R H (φ g) - 1 := by
168 rw [map_sub, completedGroupAlgebraMapInClass_of, map_one]
170end
172end CompletedGroupAlgebra