CompletedGroupAlgebra/InClassFunctoriality/StageMaps.lean
1import CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps
2import CompletedGroupAlgebra.InClassFunctoriality.ComapIndex
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/CompletedGroupAlgebra/InClassFunctoriality/StageMaps.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Functoriality of completed group algebras
15The 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.
16-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
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]
33/-- The `C`-indexed finite-stage map `R[G/φ⁻¹(V)] -> R[H/V]` induced by `φ : G -> H`. -/
35 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
36 (R : Type u) [CommRing R] (φ : G →* H) (hφ : Continuous φ)
37 (V : CompletedGroupAlgebraIndexInClass H C) :
38 CompletedGroupAlgebraStageInClass C R G
39 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) →+*
40 CompletedGroupAlgebraStageInClass C R H V :=
41 MonoidAlgebra.mapDomainRingHom R
42 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V)
44omit [TopologicalSpace R] [IsTopologicalRing R] in
45/-- A surjective group homomorphism induces a surjective finite-stage group-algebra map. -/
47 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
48 (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ)
49 (V : CompletedGroupAlgebraIndexInClass H C) :
50 Function.Surjective
52 (G := G) (H := H) C hHer (R := R) φ hφ V) := by
54 MonoidAlgebra.mapDomainRingHom_apply] using
55 (Finsupp.mapDomain_surjective (M := R)
56 (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
57 (G := G) (H := H) C hHer φ hφ hφsurj V))
59omit [TopologicalSpace R] [IsTopologicalRing R] in
60/-- The functorial finite-stage map sends singleton coefficients to singleton coefficients. -/
61@[simp]
63 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
64 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C)
65 (q : CompletedGroupAlgebraQuotientInClass G C
66 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) (r : R) :
68 (G := G) (H := H) C hHer (R := R) φ hφ V (MonoidAlgebra.single q r) =
69 MonoidAlgebra.single
70 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H)
71 C hHer φ hφ V q) r := by
72 classical
73 simp only [completedGroupAlgebraFunctorialStageMapInClass, MonoidAlgebra.single,
74 MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
76omit [TopologicalSpace R] [IsTopologicalRing R] in
77/-- The functorial finite-stage map preserves coefficient algebra-map elements. -/
79 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
80 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) (r : R) :
82 (G := G) (H := H) C hHer (R := R) φ hφ V
83 (algebraMap R
84 (CompletedGroupAlgebraStageInClass C R G
85 (completedGroupAlgebraComapIndexInClass
86 (G := G) (H := H) C hHer φ hφ V)) r) =
87 algebraMap R (CompletedGroupAlgebraStageInClass C R H V) r := by
88 simp only [completedGroupAlgebraFunctorialStageMapInClass, MonoidAlgebra.coe_algebraMap,
89 Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq, MonoidAlgebra.mapDomainRingHom_apply,
92omit [TopologicalSpace R] [IsTopologicalRing R] in
93/-- Functorial finite-stage maps commute with coefficient change. -/
94@[simp]
96 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
97 (S : Type w) [CommRing S] (f : R →+* S)
98 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
99 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := H) C S f V).comp
101 (G := G) (H := H) C hHer (R := R) φ hφ V) =
103 (G := G) (H := H) C hHer (R := S) φ hφ V).comp
104 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f
105 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) := by
106 exact MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom
107 (f := f)
108 (g := completedGroupAlgebraComapQuotientMapInClass
109 (G := G) (H := H) C hHer φ hφ V)
111/-- The functorial finite-stage group-algebra map is continuous for the finite-stage topologies. -/
113 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
114 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
115 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
116 letI : TopologicalSpace
117 (CompletedGroupAlgebraStageInClass C R G
118 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) :=
119 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace
120 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
121 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R H V) :=
122 (completedGroupAlgebraSystemInClass C hC R H).topologicalSpace V
123 Continuous (completedGroupAlgebraFunctorialStageMapInClass
124 (G := G) (H := H) C hHer (R := R) φ hφ V) := by
125 letI : Finite (CompletedGroupAlgebraQuotientInClass G C
126 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) :=
128 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
129 letI : Finite (CompletedGroupAlgebraQuotientInClass H C V) :=
131 letI : TopologicalSpace
132 (CompletedGroupAlgebraStageInClass C R G
133 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) :=
134 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace
135 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
136 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R H V) :=
137 (completedGroupAlgebraSystemInClass C hC R H).topologicalSpace V
139 (CompletedGroupAlgebraQuotientInClass G C
140 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
141 (CompletedGroupAlgebraQuotientInClass H C V)
142 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V)
144omit [TopologicalSpace R] [IsTopologicalRing R] in
145/-- Functorial finite-stage maps commute with transition maps. -/
146@[simp]
148 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
149 (φ : G →* H) (hφ : Continuous φ)
150 {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
151 (completedGroupAlgebraTransitionInClass C R H hVW).comp
153 (G := G) (H := H) C hHer (R := R) φ hφ W) =
155 (G := G) (H := H) C hHer (R := R) φ hφ V).comp
156 (completedGroupAlgebraTransitionInClass C R G
157 (completedGroupAlgebraComapIndexInClass_mono
158 (G := G) (H := H) C hHer φ hφ hVW)) := by
159 rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraFunctorialStageMapInClass,
160 completedGroupAlgebraFunctorialStageMapInClass, completedGroupAlgebraTransitionInClass,
161 ← MonoidAlgebra.mapDomainRingHom_comp, ← MonoidAlgebra.mapDomainRingHom_comp]
162 congr 1
163 apply MonoidHom.ext
164 intro q
165 rcases QuotientGroup.mk'_surjective
166 ((((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
167 (G := G) (H := H) C hHer φ hφ W)).1 : OpenNormalSubgroup G) : Subgroup G)) q with
168 ⟨g, rfl⟩
169 rfl
171omit [TopologicalSpace R] [IsTopologicalRing R] in
172/-- Functorial finite-stage maps commute with a group transition followed by coefficient change. -/
174 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
175 (S : Type w) [CommRing S] (f : R →+* S)
176 (φ : G →* H) (hφ : Continuous φ)
177 {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
178 ((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := H) C S f V).comp
179 (completedGroupAlgebraTransitionInClass C R H hVW)).comp
181 (G := G) (H := H) C hHer (R := R) φ hφ W) =
183 (G := G) (H := H) C hHer (R := S) φ hφ V).comp
184 ((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f
185 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)).comp
186 (completedGroupAlgebraTransitionInClass C R G
187 (completedGroupAlgebraComapIndexInClass_mono
188 (G := G) (H := H) C hHer φ hφ hVW))) := by
189 rw [RingHom.comp_assoc]
191 rw [← RingHom.comp_assoc]
193 rw [RingHom.comp_assoc]
195omit [TopologicalSpace R] [IsTopologicalRing R] in
196/-- The functorial finite-stage map agrees with the stage map after passing to the comap quotient. -/
197@[simp]
199 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
200 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
202 (G := G) (H := H) C hHer (R := R) φ hφ V).comp
203 (completedGroupAlgebraStageMapInClass C R G
204 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) =
205 (completedGroupAlgebraStageMapInClass C R H V).comp
206 (MonoidAlgebra.mapDomainRingHom R φ) := by
207 rw [completedGroupAlgebraFunctorialStageMapInClass, completedGroupAlgebraStageMapInClass,
208 completedGroupAlgebraStageMapInClass, ← MonoidAlgebra.mapDomainRingHom_comp,
209 ← MonoidAlgebra.mapDomainRingHom_comp]
210 congr 1
212end