Source: ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.UnitRepresentation
1import ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Comparison
3/-!
4# Unit representations in the in-class completion
6This file studies the continuous group-like unit representation in an in-class completed group
7algebra. Its image spans densely, and scalar restriction along it equips profinite modules with a
8continuous group action.
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]
28variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30/--
31The concrete class-indexed unit representation evaluates to the corresponding completed
32group-like element.
33-/
34@[simp]
35theorem completedGroupAlgebraUnitRepresentationInClassConcrete_val
36 (C : ProCGroups.FiniteGroupClass.{v})
37 (g : G) :
38 ((completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C R G)
39 (toCompletedGroupAlgebraInClassRingHom C R G) g :
40 (CompletedGroupAlgebraInClass C R G)ˣ) : CompletedGroupAlgebraInClass C R G) =
41 completedGroupAlgebraOfInClass C R G g :=
42 rfl
44/--
45The \(C\)-indexed canonical unit representation is continuous after forgetting to
46\(\widehat{R[G]}_{C}\).
47-/
48theorem continuous_completedGroupAlgebraUnitRepresentationInClassConcrete_val
49 (C : ProCGroups.FiniteGroupClass.{v}) :
50 Continuous fun g : G =>
51 ((completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C R G)
52 (toCompletedGroupAlgebraInClassRingHom C R G) g :
53 (CompletedGroupAlgebraInClass C R G)ˣ) : CompletedGroupAlgebraInClass C R G) := by
54 apply (continuous_completedGroupAlgebraOfInClass (R := R) (G := G) C).congr
55 intro g
56 exact (completedGroupAlgebraUnitRepresentationInClassConcrete_val
57 (R := R) (G := G) C g).symm
59/-- The dense abstract map lands in the span of class-indexed completed group-like elements. -/
60theorem toCompletedGroupAlgebraInClassRingHom_mem_span_completedGroupAlgebraOfInClass
61 (C : ProCGroups.FiniteGroupClass.{v})
62 (x : MonoidAlgebra R G) :
63 toCompletedGroupAlgebraInClassRingHom C R G x ∈
64 Submodule.span R (Set.range (completedGroupAlgebraOfInClass C R G)) := by
65 classical
66 refine MonoidAlgebra.induction_linear
67 (p := fun x : MonoidAlgebra R G =>
68 toCompletedGroupAlgebraInClassRingHom C R G x ∈
69 Submodule.span R (Set.range (completedGroupAlgebraOfInClass C R G)))
70 x ?_ ?_ ?_
71 · -- The zero case.
72 rw [show toCompletedGroupAlgebraInClassRingHom C R G (0 : MonoidAlgebra R G) =
73 (0 : CompletedGroupAlgebraInClass C R G) by
74 exact map_zero (toCompletedGroupAlgebraInClassRingHom C R G)]
75 exact Submodule.zero_mem _
76 · intro a b ha hb
77 rw [map_add]
78 exact Submodule.add_mem _ ha hb
79 · intro g r
80 have hsingle :
81 toCompletedGroupAlgebraInClassRingHom C R G (MonoidAlgebra.single g r) =
82 r • completedGroupAlgebraOfInClass C R G g := by
83 rw [← MonoidAlgebra.smul_of]
84 change toCompletedGroupAlgebraInClass C R G (r • MonoidAlgebra.of R G g) =
85 r • completedGroupAlgebraOfInClass C R G g
86 rw [toCompletedGroupAlgebraInClass_smul]
87 rfl
88 rw [hsingle]
89 exact Submodule.smul_mem _ r (Submodule.subset_span ⟨g, rfl⟩)
91/--
92The \(C\)-indexed completed group-like elements topologically generate \(\widehat{R[G]}_{C}\) as
93an \(R\)-module, for pro-\(C\) groups and formation classes.
94-/
95theorem completedGroupAlgebraOfInClass_dense_span
96 (C : ProCGroups.FiniteGroupClass.{v})
97 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
98 closure (Submodule.span R (Set.range (completedGroupAlgebraOfInClass C R G)) :
99 Set (CompletedGroupAlgebraInClass C R G)) = Set.univ := by
100 rw [Set.eq_univ_iff_forall]
101 intro y
102 have hy :
103 y ∈ closure (Set.range (toCompletedGroupAlgebraInClassRingHom C R G)) := by
104 have hdense : DenseRange (toCompletedGroupAlgebraInClassRingHom C R G) := by
105 change DenseRange (toCompletedGroupAlgebraInClass C R G)
106 exact denseRange_toCompletedGroupAlgebraInClass (R := R) (G := G) C hForm hG
107 rw [hdense.closure_range]
108 exact Set.mem_univ y
109 exact closure_mono (by
110 intro z hz
111 rcases hz with ⟨x, rfl⟩
112 exact toCompletedGroupAlgebraInClassRingHom_mem_span_completedGroupAlgebraOfInClass
113 (R := R) (G := G) C x) hy
115/--
116A continuous module over the \(C\)-indexed completed group algebra inherits the natural
117continuous \(G\)-module structure via the group-like units.
118-/
119theorem completedGroupAlgebraInClass_module_induces_continuous_gmodule
120 (C : ProCGroups.FiniteGroupClass.{v})
121 (A : Type (max u v)) [AddCommGroup A] [TopologicalSpace A]
122 [Module (CompletedGroupAlgebraInClass C R G) A]
123 [ContinuousSMul (CompletedGroupAlgebraInClass C R G) A] :
124 letI : DistribMulAction G A :=
125 unitRepresentationDistribMulAction G (CompletedGroupAlgebraInClass C R G) A
126 (completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C R G)
127 (toCompletedGroupAlgebraInClassRingHom C R G))
128 ContinuousSMul G A := by
129 exact unitRepresentation_continuousSMul G (CompletedGroupAlgebraInClass C R G) A
130 (completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C R G)
131 (toCompletedGroupAlgebraInClassRingHom C R G))
132 (continuous_completedGroupAlgebraUnitRepresentationInClassConcrete_val (R := R) (G := G) C )
134end
136end CompletedGroupAlgebra