CompletedGroupAlgebra/InClassFunctoriality/GroupLike.lean
1import CompletedGroupAlgebra.InClassFunctoriality.Maps
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/InClassFunctoriality/GroupLike.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 `C`-indexed inverse-limit construction satisfies the completed-group-algebra property
36package whenever `G` is pro-`C`. -/
38 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
39 (hForm : ProCGroups.FiniteGroupClass.Formation C)
40 (hR : IsProfiniteRing R) (hG : IsProCGroup C G) :
41 IsCompletedGroupAlgebraModel R G (CompletedGroupAlgebraInClass C hC R G) := by
42 refine ⟨hR, hG.1, completedGroupAlgebraInClass_isProfiniteRing
43 (R := R) (G := G) C hC hR, ?_⟩
44 refine ⟨TopologicalSpace.induced (toCompletedGroupAlgebraInClass C hC R G)
45 (inferInstance : TopologicalSpace (CompletedGroupAlgebraInClass C hC R G)), ?_⟩
46 letI : TopologicalSpace (MonoidAlgebra R G) :=
47 TopologicalSpace.induced (toCompletedGroupAlgebraInClass C hC R G)
48 (inferInstance : TopologicalSpace (CompletedGroupAlgebraInClass C hC R G))
49 exact ⟨toCompletedGroupAlgebraInClassRingHom C hC R G,
50 denseRange_toCompletedGroupAlgebraInClass (R := R) (G := G) C hC hForm hG,
51 by
52 change Continuous (toCompletedGroupAlgebraInClass C hC R G)
53 exact continuous_induced_dom⟩
55/-- The image of a group element in the `C`-indexed completed group algebra. -/
57 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
58 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
59 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
60 (g : G) : CompletedGroupAlgebraInClass C hC R G :=
61 toCompletedGroupAlgebraInClass C hC R G (MonoidAlgebra.of R G g)
63/-- Projection of a class-indexed completed group-like element to a finite quotient stage. -/
64@[simp]
66 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
67 (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
68 completedGroupAlgebraProjectionInClass C hC R G U
69 (completedGroupAlgebraOfInClass C hC R G g) =
70 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1 := by
73 completedGroupAlgebraStageMapInClass_of]
75/-- The class-indexed completed group-like element attached to one is the unit. -/
76@[simp]
78 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
79 completedGroupAlgebraOfInClass C hC R G 1 =
80 (1 : CompletedGroupAlgebraInClass C hC R G) := by
81 apply (completedGroupAlgebraSystemInClass C hC R G).ext
82 intro U
83 change completedGroupAlgebraProjectionInClass C hC R G U
84 (completedGroupAlgebraOfInClass C hC R G 1) =
85 completedGroupAlgebraProjectionInClass C hC R G U
86 (1 : CompletedGroupAlgebraInClass C hC R G)
88 change MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U 1)
89 (1 : R) =
90 completedGroupAlgebraProjectionRingHomInClass C hC R G U
91 (1 : CompletedGroupAlgebraInClass C hC R G)
93 change MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U 1)
94 (1 : R) = 1
95 rfl
97/-- Class-indexed completed group-like elements multiply according to the group law. -/
98@[simp 900]
100 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
101 (g h : G) :
102 completedGroupAlgebraOfInClass C hC R G (g * h) =
103 completedGroupAlgebraOfInClass C hC R G g *
104 completedGroupAlgebraOfInClass C hC R G h := by
105 apply (completedGroupAlgebraSystemInClass C hC R G).ext
106 intro U
107 change completedGroupAlgebraProjectionInClass C hC R G U
108 (completedGroupAlgebraOfInClass C hC R G (g * h)) =
109 completedGroupAlgebraProjectionInClass C hC R G U
110 (completedGroupAlgebraOfInClass C hC R G g *
111 completedGroupAlgebraOfInClass C hC R G h)
113 have hmul :
114 completedGroupAlgebraProjectionInClass C hC R G U
115 (completedGroupAlgebraOfInClass C hC R G g *
116 completedGroupAlgebraOfInClass C hC R G h) =
117 completedGroupAlgebraProjectionInClass C hC R G U
118 (completedGroupAlgebraOfInClass C hC R G g) *
119 completedGroupAlgebraProjectionInClass C hC R G U
120 (completedGroupAlgebraOfInClass C hC R G h) := by
121 exact map_mul (completedGroupAlgebraProjectionRingHomInClass C hC R G U)
122 (completedGroupAlgebraOfInClass C hC R G g)
123 (completedGroupAlgebraOfInClass C hC R G h)
125 change MonoidAlgebra.single
126 (openNormalSubgroupInClassProj (C := C) (G := G) U (g * h)) (1 : R) =
127 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1 *
128 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U h) 1
131/-- The class-indexed finite-stage group-like map is continuous. -/
133 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
134 (U : CompletedGroupAlgebraIndexInClass G C) :
135 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
136 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
137 Continuous fun g : G => completedGroupAlgebraStageMapInClass C R G U
138 (MonoidAlgebra.of R G g) := by
139 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
141 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
142 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
143 letI : DiscreteTopology (CompletedGroupAlgebraQuotientInClass G C U) :=
144 QuotientGroup.discreteTopology
145 (ProCGroups.openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
146 have hbasis :
147 Continuous fun q : CompletedGroupAlgebraQuotientInClass G C U =>
148 (MonoidAlgebra.of R (CompletedGroupAlgebraQuotientInClass G C U) q :
149 CompletedGroupAlgebraStageInClass C R G U) :=
150 continuous_of_discreteTopology
151 have hproj :
152 Continuous fun g : G => openNormalSubgroupInClassProj (C := C) (G := G) U g := by
153 change Continuous
154 (QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G))
155 exact continuous_quotient_mk'
156 simpa [MonoidAlgebra.of, completedGroupAlgebraStageMapInClass_single] using hbasis.comp hproj
158/-- The class-indexed completed group-like map is continuous. -/
160 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
161 Continuous (completedGroupAlgebraOfInClass C hC R G) := by
162 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C,
163 TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
164 fun U => (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
165 have hval : Continuous fun g : G =>
166 fun U : CompletedGroupAlgebraIndexInClass G C =>
167 (show CompletedGroupAlgebraStageInClass C R G U from
168 (completedGroupAlgebraOfInClass C hC R G g).1 U) := by
169 change Continuous fun g : G =>
170 fun U : CompletedGroupAlgebraIndexInClass G C =>
171 completedGroupAlgebraStageMapInClass C R G U (MonoidAlgebra.of R G g)
172 apply continuous_pi
173 intro U
174 exact continuous_completedGroupAlgebraStageMapInClass_of (R := R) (G := G) C hC U
175 exact Continuous.subtype_mk hval fun g => (completedGroupAlgebraOfInClass C hC R G g).2
177end