CompletedGroupAlgebra/InClassFunctoriality/UnitRepresentation.lean
1import CompletedGroupAlgebra.InClassFunctoriality.Comparison
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/InClassFunctoriality/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# Functoriality of completed group algebras
14The completed group algebra is presented as an inverse limit of finite group algebras, together with canonical augmentation, augmentation ideal, finite-stage maps, functoriality, and profinite module universal properties.
15-/
16open scoped Topology
18namespace CompletedGroupAlgebra
20noncomputable section
22open ProCGroups
23open ProCGroups.ProC
24open ProCGroups.InverseSystems
25open ProCGroups.Completion
27universe u v w
29variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
35/-- The concrete class-indexed unit representation evaluates to the corresponding completed group-like element. -/
36@[simp]
38 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
39 (g : G) :
40 ((completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C hC R G)
41 (toCompletedGroupAlgebraInClassRingHom C hC R G) g :
42 (CompletedGroupAlgebraInClass C hC R G)ˣ) : CompletedGroupAlgebraInClass C hC R G) =
43 completedGroupAlgebraOfInClass C hC R G g :=
44 rfl
46/-- The `C`-indexed canonical unit representation is continuous after forgetting to
47`[[R G]]_C`. -/
49 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
50 Continuous fun g : G =>
51 ((completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C hC R G)
52 (toCompletedGroupAlgebraInClassRingHom C hC R G) g :
53 (CompletedGroupAlgebraInClass C hC R G)ˣ) : CompletedGroupAlgebraInClass C hC R G) := by
54 simpa using continuous_completedGroupAlgebraOfInClass (R := R) (G := G) C hC
56/-- The dense abstract map lands in the span of class-indexed completed group-like elements. -/
58 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
59 (x : MonoidAlgebra R G) :
60 toCompletedGroupAlgebraInClassRingHom C hC R G x ∈
61 Submodule.span R (Set.range (completedGroupAlgebraOfInClass C hC R G)) := by
62 classical
63 induction x using Finsupp.induction with
65 rw [show toCompletedGroupAlgebraInClassRingHom C hC R G (0 : MonoidAlgebra R G) =
66 (0 : CompletedGroupAlgebraInClass C hC R G) by
67 exact map_zero (toCompletedGroupAlgebraInClassRingHom C hC R G)]
68 exact Submodule.zero_mem _
69 | single_add g r x _ _ ih =>
71 refine Submodule.add_mem _ ?_ ih
72 have hsingle :
73 toCompletedGroupAlgebraInClassRingHom C hC R G (MonoidAlgebra.single g r) =
74 r • completedGroupAlgebraOfInClass C hC R G g := by
75 rw [show MonoidAlgebra.single g r =
76 r • MonoidAlgebra.of R G g by
77 simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.smul_single, smul_eq_mul, mul_one]]
78 change toCompletedGroupAlgebraInClass C hC R G (r • MonoidAlgebra.of R G g) =
79 r • completedGroupAlgebraOfInClass C hC R G g
81 rfl
82 rw [hsingle]
83 exact Submodule.smul_mem _ r (Submodule.subset_span ⟨g, rfl⟩)
85/-- The `C`-indexed completed group-like elements topologically generate `[[R G]]_C` as an
88 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
89 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
90 closure (Submodule.span R (Set.range (completedGroupAlgebraOfInClass C hC R G)) :
91 Set (CompletedGroupAlgebraInClass C hC R G)) = Set.univ := by
92 rw [Set.eq_univ_iff_forall]
93 intro y
94 have hy :
95 y ∈ closure (Set.range (toCompletedGroupAlgebraInClassRingHom C hC R G)) := by
96 have hdense : DenseRange (toCompletedGroupAlgebraInClassRingHom C hC R G) := by
97 change DenseRange (toCompletedGroupAlgebraInClass C hC R G)
98 exact denseRange_toCompletedGroupAlgebraInClass (R := R) (G := G) C hC hForm hG
99 rw [hdense.closure_range]
100 exact Set.mem_univ y
101 exact closure_mono (by
102 intro z hz
103 rcases hz with ⟨x, rfl⟩
105 (R := R) (G := G) C hC x) hy
107/-- A continuous module over the `C`-indexed completed group algebra inherits the natural
108continuous `G`-module structure via the group-like units. -/
110 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
111 (A : Type (max u v)) [AddCommGroup A] [TopologicalSpace A]
112 [Module (CompletedGroupAlgebraInClass C hC R G) A]
113 [ContinuousSMul (CompletedGroupAlgebraInClass C hC R G) A] :
114 letI : DistribMulAction G A :=
115 unitRepresentationDistribMulAction G (CompletedGroupAlgebraInClass C hC R G) A
116 (completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C hC R G) (toCompletedGroupAlgebraInClassRingHom C hC R G))
117 ContinuousSMul G A := by
118 exact unitRepresentation_continuousSMul G (CompletedGroupAlgebraInClass C hC R G) A
119 (completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C hC R G) (toCompletedGroupAlgebraInClassRingHom C hC R G))
120 (continuous_completedGroupAlgebraUnitRepresentationInClassConcrete_val (R := R) (G := G) C hC)
122end