Yamaguchi Lean 4 Library
CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/UnitRepresentation.lean
CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/UnitRepresentation/Source

CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/UnitRepresentation.lean

1import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/UnitRepresentation.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Unit representations and induced group actions
14This module packages unit-valued representations of finite group algebras and the induced continuous scalar actions used by the profinite-module layer.
15-/
17open scoped Topology
18open ProCGroups
22universe u v w z
24/-- The canonical embedding of a group into the units of its abstract group algebra. -/
26 (R : Type u) (G : Type v) [CommRing R] [Group G] :
27 G →* (MonoidAlgebra R G)ˣ where
28 toFun g :=
29 { val := MonoidAlgebra.of R G g
30 inv := MonoidAlgebra.of R G g⁻¹
31 val_inv := by
32 rw [← map_mul]
33 simp only [MonoidAlgebra.of, mul_inv_cancel, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]
34 inv_val := by
35 rw [← map_mul]
36 simp only [MonoidAlgebra.of, inv_mul_cancel, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]}
37 map_one' := by
38 ext x
39 simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, Units.val_one, MonoidAlgebra.one_def]
40 map_mul' := by
41 intro g h
42 ext x
43 simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, Units.val_mul, MonoidAlgebra.single_mul_single,
44 mul_one]
46/-- The value of the abstract unit representation is the corresponding group-like basis
47element. -/
48@[simp]
50 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
51 ((groupAlgebraUnitRepresentation R G g : (MonoidAlgebra R G)ˣ) :
52 MonoidAlgebra R G) = MonoidAlgebra.of R G g :=
53 rfl
55/-- A completed group algebra model receives the canonical unit representation of `G`
56through the dense abstract group algebra map. -/
58 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
59 (dense : MonoidAlgebra R G →+* RG) : G →* RGˣ :=
60 (Units.map dense.toMonoidHom).comp (groupAlgebraUnitRepresentation R G)
62/-- The value of the completed unit representation is the dense image of the group-like basis
63element. -/
64@[simp]
66 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
67 (dense : MonoidAlgebra R G →+* RG) (g : G) :
68 ((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) =
69 dense (MonoidAlgebra.of R G g) :=
70 rfl
72/-- The completed unit representation has augmentation `1`. -/
74 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
75 [Group G] [Ring RG] [TopologicalSpace RG]
76 {dense : RingHom (MonoidAlgebra R G) RG}
77 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) (g : G) :
79 ((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) = 1 := by
80 have h := congrArg (fun f : RingHom (MonoidAlgebra R G) R => f (MonoidAlgebra.of R G g))
82 simpa using h
84/-- The completed group-like difference `g - 1` lies in the completed augmentation ideal. -/
86 (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
87 [Group G] [Ring RG] [TopologicalSpace RG]
88 {dense : RingHom (MonoidAlgebra R G) RG}
89 (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) (g : G) :
90 ((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) - 1 ∈
93 (((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) - 1) = 0
95 sub_self]
97/-- Pull back a ring-module structure along a unit representation of a group. This is the
98algebraic core of Proposition 5.3.6(a). -/
100 (G : Type u) (S : Type v) (A : Type w) [Group G] [Ring S] [AddCommGroup A]
101 [Module S A] (ρ : G →* Sˣ) : DistribMulAction G A where
102 smul g a := ((ρ g : Sˣ) : S) • a
103 one_smul := by
104 intro a
105 change (((ρ (1 : G) : Sˣ) : S) • a) = a
107 exact one_smul S a
108 mul_smul := by
109 intro g h a
110 change (((ρ (g * h) : Sˣ) : S) • a) =
111 (((ρ g : Sˣ) : S) • (((ρ h : Sˣ) : S) • a))
113 exact mul_smul (((ρ g : Sˣ) : S)) (((ρ h : Sˣ) : S)) a
114 smul_zero := by
115 intro g
116 change (((ρ g : Sˣ) : S) • (0 : A)) = 0
117 exact smul_zero (((ρ g : Sˣ) : S))
118 smul_add := by
119 intro g a b
120 change (((ρ g : Sˣ) : S) • (a + b)) =
121 ((ρ g : Sˣ) : S) • a + ((ρ g : Sˣ) : S) • b
122 exact smul_add (((ρ g : Sˣ) : S)) a b
124/-- The pulled-back action is continuous whenever the unit representation is continuous after
125forgetting to the coefficient ring. -/
127 (G : Type u) (S : Type v) (A : Type w) [Group G] [TopologicalSpace G] [Ring S]
128 [TopologicalSpace S] [AddCommGroup A] [TopologicalSpace A] [Module S A]
129 [ContinuousSMul S A] (ρ : G →* Sˣ)
130 (hρ : Continuous fun g : G => ((ρ g : Sˣ) : S)) :
131 letI : DistribMulAction G A := unitRepresentationDistribMulAction G S A ρ
132 ContinuousSMul G A := by
133 letI : DistribMulAction G A := unitRepresentationDistribMulAction G S A ρ
134 refine ContinuousSMul.mk ?_
136 have hpair : Continuous fun p : G × A => (((ρ p.1 : Sˣ) : S), p.2) :=
137 (hρ.comp continuous_fst).prodMk continuous_snd
138 exact (show Continuous (fun p : S × A => p.1 • p.2) from continuous_smul).comp hpair
140/-- Finite-stage version of Proposition 5.3.6(a): a module over the finite group algebra inherits
141the continuous `G`-module structure coming from the canonical group-like units. -/
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
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
160 exact unitRepresentation_continuousSMul G (MonoidAlgebra R G) A
161 (groupAlgebraUnitRepresentation R G) continuous_of_discreteTopology
163/-- Proposition 5.3.6(a), model-independent form: a module over a completed group algebra
164inherits the natural algebraic `G`-module structure. -/
166 (R : Type u) (G : Type v) (RG A : Type w) [CommRing R] [Group G] [Ring RG]
167 [AddCommGroup A] [Module RG A] (dense : MonoidAlgebra R G →+* RG) :
168 Nonempty (DistribMulAction G A) := by
172/-- Topological version of the unit-representation construction, once the canonical unit
173representation is known to be continuous after forgetting to the completed group algebra model. -/
175 (R : Type u) (G : Type v) (RG A : Type w) [CommRing R] [TopologicalSpace G]
176 [Group G] [Ring RG] [TopologicalSpace RG] [AddCommGroup A] [TopologicalSpace A]
177 [Module RG A] [ContinuousSMul RG A] (dense : MonoidAlgebra R G →+* RG)
178 (hdenseG : Continuous fun g : G => dense (MonoidAlgebra.of R G g)) :
179 letI : DistribMulAction G A :=
182 ContinuousSMul G A := by
184 (completedGroupAlgebraUnitRepresentation R G RG dense) (by simpa using hdenseG)