Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.UnitRepresentation
1import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed
3/-!
4# Group-like unit representations
6Groups embed as units in their algebraic and completed group algebras. This file relates that
7representation to augmentation and shows how restriction of scalars gives continuous group
8actions on modules.
9-/
11open scoped Topology
12open ProCGroups
14namespace CompletedGroupAlgebra
16universe u v w z
18/-- The canonical embedding of a group into the units of its abstract group algebra. -/
19noncomputable def groupAlgebraUnitRepresentation
20 (R : Type u) (G : Type v) [CommRing R] [Group G] :
21 G →* (MonoidAlgebra R G)ˣ where
22 toFun g :=
23 { val := MonoidAlgebra.of R G g
24 inv := MonoidAlgebra.of R G g⁻¹
25 val_inv := by
26 rw [← map_mul, mul_inv_cancel, map_one]
27 inv_val := by
28 rw [← map_mul, inv_mul_cancel, map_one]}
29 map_one' := by
30 apply Units.ext
31 exact map_one (MonoidAlgebra.of R G)
32 map_mul' := by
33 intro g h
34 apply Units.ext
35 exact map_mul (MonoidAlgebra.of R G) g h
37/-- The value of the abstract unit representation is the corresponding group-like basis element. -/
38@[simp]
39theorem groupAlgebraUnitRepresentation_val
40 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
41 ((groupAlgebraUnitRepresentation R G g : (MonoidAlgebra R G)ˣ) :
42 MonoidAlgebra R G) = MonoidAlgebra.of R G g :=
43 rfl
45/--
46A completed group algebra model receives the canonical unit representation of \(G\) through the
47dense abstract group-algebra map.
48-/
49noncomputable def completedGroupAlgebraUnitRepresentation
50 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
51 (dense : MonoidAlgebra R G →+* RG) : G →* RGˣ :=
52 (Units.map dense.toMonoidHom).comp (groupAlgebraUnitRepresentation R G)
54/--
55The value of the completed unit representation is the dense image of the group-like basis
56element.
57-/
58@[simp]
59theorem completedGroupAlgebraUnitRepresentation_val
60 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
61 (dense : MonoidAlgebra R G →+* RG) (g : G) :
62 ((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) =
63 dense (MonoidAlgebra.of R G g) :=
64 rfl
66/-- The completed unit representation has augmentation 1. -/
67theorem completedGroupAlgebraAugmentation_unitRepresentation_val
68 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
69 [Group G] [Ring RG] [TopologicalSpace RG]
70 {dense : RingHom (MonoidAlgebra R G) RG}
71 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) (g : G) :
72 completedGroupAlgebraAugmentation R G RG haug
73 ((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) = 1 := by
74 have h := congrArg (fun f : RingHom (MonoidAlgebra R G) R => f (MonoidAlgebra.of R G g))
75 (completedGroupAlgebraAugmentation_comp_dense R G RG haug)
76 simpa using h
78/-- The completed group-like difference \(g-1\) lies in the completed augmentation ideal. -/
79theorem completedGroupAlgebra_unit_sub_one_mem_augmentationIdeal
80 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
81 [Group G] [Ring RG] [TopologicalSpace RG]
82 {dense : RingHom (MonoidAlgebra R G) RG}
83 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) (g : G) :
84 ((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) - 1 ∈
85 completedGroupAlgebraAugmentationIdeal R G RG haug := by
86 change completedGroupAlgebraAugmentation R G RG haug
87 (((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) - 1) = 0
88 rw [map_sub, completedGroupAlgebraAugmentation_unitRepresentation_val R G RG haug g, map_one,
89 sub_self]
91/--
92Pull back a ring-module structure along a unit representation of a group. This is the algebraic
93core of Proposition 5.3.6(a).
94-/
95@[reducible]
96noncomputable def unitRepresentationDistribMulAction
97 (G : Type u) (S : Type v) (A : Type w) [Group G] [Ring S] [AddCommGroup A]
98 [Module S A] (ρ : G →* Sˣ) : DistribMulAction G A where
99 smul g a := ((ρ g : Sˣ) : S) • a
100 one_smul := by
101 intro a
102 change (((ρ (1 : G) : Sˣ) : S) • a) = a
103 rw [map_one]
104 exact one_smul S a
105 mul_smul := by
106 intro g h a
107 change (((ρ (g * h) : Sˣ) : S) • a) =
108 (((ρ g : Sˣ) : S) • (((ρ h : Sˣ) : S) • a))
109 rw [map_mul]
110 exact mul_smul (((ρ g : Sˣ) : S)) (((ρ h : Sˣ) : S)) a
111 smul_zero := by
112 intro g
113 change (((ρ g : Sˣ) : S) • (0 : A)) = 0
114 exact smul_zero (((ρ g : Sˣ) : S))
115 smul_add := by
116 intro g a b
117 change (((ρ g : Sˣ) : S) • (a + b)) =
118 ((ρ g : Sˣ) : S) • a + ((ρ g : Sˣ) : S) • b
119 exact smul_add (((ρ g : Sˣ) : S)) a b
121/--
122The pulled-back action is continuous whenever the unit representation is continuous after
123forgetting to the coefficient ring.
124-/
125theorem unitRepresentation_continuousSMul
126 (G : Type u) (S : Type v) (A : Type w) [Group G] [TopologicalSpace G] [Ring S]
127 [TopologicalSpace S] [AddCommGroup A] [TopologicalSpace A] [Module S A]
128 [ContinuousSMul S A] (ρ : G →* Sˣ)
129 (hρ : Continuous fun g : G => ((ρ g : Sˣ) : S)) :
130 letI : DistribMulAction G A := unitRepresentationDistribMulAction G S A ρ
131 ContinuousSMul G A := by
132 letI : DistribMulAction G A := unitRepresentationDistribMulAction G S A ρ
133 refine ContinuousSMul.mk ?_
134 have hpair : Continuous fun p : G × A => (((ρ p.1 : Sˣ) : S), p.2) :=
135 (hρ.comp continuous_fst).prodMk continuous_snd
136 exact (show Continuous (fun p : S × A => p.1 • p.2) from continuous_smul).comp hpair
138/--
139Finite-stage version of Proposition 5.3.6(a): a module over the finite group algebra inherits
140the continuous \(G\)-module structure coming from the canonical group-like units.
141-/
142theorem finiteGroupAlgebra_module_induces_continuous_gmodule
143 (R : Type u) (G : Type v) (A : Type w) [CommRing R] [TopologicalSpace R]
144 [Group G] [TopologicalSpace G] [Finite G] [DiscreteTopology G]
145 [AddCommGroup A] [TopologicalSpace A] [Module (MonoidAlgebra R G) A]
146 (hsmul : letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
147 ContinuousSMul (MonoidAlgebra R G) A) :
148 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
149 letI : DistribMulAction G A :=
150 unitRepresentationDistribMulAction G (MonoidAlgebra R G) A
151 (groupAlgebraUnitRepresentation R G)
152 ContinuousSMul G A := by
153 classical
154 letI : Fintype G := Fintype.ofFinite G
155 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
156 letI : ContinuousSMul (MonoidAlgebra R G) A := hsmul
157 letI : DistribMulAction G A :=
158 unitRepresentationDistribMulAction G (MonoidAlgebra R G) A
159 (groupAlgebraUnitRepresentation R G)
160 exact unitRepresentation_continuousSMul G (MonoidAlgebra R G) A
161 (groupAlgebraUnitRepresentation R G) continuous_of_discreteTopology
163/--
164Proposition 5.3.6(a), model-independent form: a module over a completed group algebra inherits
165the natural algebraic \(G\)-module structure.
166-/
167theorem completedGroupAlgebra_module_induces_gmodule
168 (R : Type u) (G : Type v) (RG A : Type w) [CommRing R] [Group G] [Ring RG]
169 [AddCommGroup A] [Module RG A] (dense : MonoidAlgebra R G →+* RG) :
170 Nonempty (DistribMulAction G A) := by
171 exact ⟨unitRepresentationDistribMulAction G RG A
172 (completedGroupAlgebraUnitRepresentation R G RG dense)⟩
174/--
175Topological version of the unit-representation construction, once the canonical unit
176representation is known to be continuous after forgetting to the completed group algebra model.
177-/
178theorem completedGroupAlgebra_module_induces_continuous_gmodule
179 (R : Type u) (G : Type v) (RG A : Type w) [CommRing R] [TopologicalSpace G]
180 [Group G] [Ring RG] [TopologicalSpace RG] [AddCommGroup A] [TopologicalSpace A]
181 [Module RG A] [ContinuousSMul RG A] (dense : MonoidAlgebra R G →+* RG)
182 (hdenseG : Continuous fun g : G => dense (MonoidAlgebra.of R G g)) :
183 letI : DistribMulAction G A :=
184 unitRepresentationDistribMulAction G RG A
185 (completedGroupAlgebraUnitRepresentation R G RG dense)
186 ContinuousSMul G A := by
187 exact unitRepresentation_continuousSMul G RG A
188 (completedGroupAlgebraUnitRepresentation R G RG dense) (by simpa using hdenseG)
190end CompletedGroupAlgebra