CompletedGroupAlgebra/AllFiniteFunctoriality/Map.lean
1import CompletedGroupAlgebra.AllFiniteFunctoriality.StageMap
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/AllFiniteFunctoriality/Map.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed group algebra functorial maps
13-/
15open scoped Topology
17namespace CompletedGroupAlgebra
19noncomputable section
21open ProCGroups
22open ProCGroups.ProC
24universe u v w
26variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
27variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30/-- Lemma 5.3.5(e), map construction: a continuous homomorphism of profinite groups
31`φ : G -> H` induces a continuous ring homomorphism `[[R G]] -> [[R H]]`. -/
33 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
34 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
35 Carrier R G →+* Carrier R H where
36 toFun x := ⟨fun V =>
37 completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
39 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x), by
40 intro V W hVW
41 change completedGroupAlgebraTransition R H hVW
42 (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ W
44 (completedGroupAlgebraComapIndex (G := G) hG φ hφ W) x)) =
45 completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
47 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)
48 have hcomp := congrFun
49 (congrArg DFunLike.coe
50 (completedGroupAlgebraFunctorialStageMap_transition (R := R) (G := G) (H := H)
51 hG φ hφ hVW))
53 (completedGroupAlgebraComapIndex (G := G) hG φ hφ W) x)
54 rw [RingHom.comp_apply, RingHom.comp_apply] at hcomp
55 rw [← completedGroupAlgebraProjection_compatible (R := R) (G := G) x
56 (completedGroupAlgebraComapIndex_mono (G := G) hG φ hφ hVW)]
57 exact hcomp⟩
58 map_zero' := by
59 apply (completedGroupAlgebraSystem R H).ext
60 intro V
61 exact map_zero (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
62 hG φ hφ V)
63 map_one' := by
64 apply (completedGroupAlgebraSystem R H).ext
65 intro V
66 exact map_one (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
67 hG φ hφ V)
68 map_add' x y := by
69 apply (completedGroupAlgebraSystem R H).ext
70 intro V
71 exact map_add (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
72 hG φ hφ V)
74 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)
76 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) y)
77 map_mul' x y := by
78 apply (completedGroupAlgebraSystem R H).ext
79 intro V
80 exact map_mul (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
81 hG φ hφ V)
83 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)
85 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) y)
87/-- Projection of the completed functorial map is computed by the corresponding stage map. -/
88@[simp]
90 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
91 (V : CompletedGroupAlgebraIndex H) (x : Carrier R G) :
93 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x) =
94 completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
96 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x) :=
97 rfl
99/-- Lemma 5.3.5(e), algebra form: a continuous homomorphism of profinite groups induces an
100`R`-algebra homomorphism on completed group algebras. -/
102 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
103 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
104 Carrier R G →ₐ[R] Carrier R H where
105 toRingHom := completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
106 commutes' := by
107 intro r
108 apply (completedGroupAlgebraSystem R H).ext
109 intro V
110 change completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
111 (algebraMap R
113 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) r) =
114 algebraMap R (CompletedGroupAlgebraStage R H V) r
116 (R := R) (G := G) (H := H) hG φ hφ V r
118/-- The algebra-hom version of the completed functorial map has the same underlying function. -/
119@[simp]
121 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
122 (x : Carrier R G) :
123 completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG φ hφ x =
124 completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x :=
125 rfl
127/-- The induced completed map is continuous. -/
129 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
130 Continuous (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ) := by
131 let A := Carrier R G
132 letI : ∀ V : CompletedGroupAlgebraIndex H,
133 TopologicalSpace (CompletedGroupAlgebraStage R H V) :=
134 fun V => (completedGroupAlgebraSystem R H).topologicalSpace V
135 have hval : Continuous fun x : A =>
136 ((completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x) :
137 (V : CompletedGroupAlgebraIndex H) → (completedGroupAlgebraSystem R H).X V) := by
138 change Continuous fun x : A =>
139 fun V : CompletedGroupAlgebraIndex H =>
140 completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
142 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)
143 apply continuous_pi
144 intro V
145 letI : TopologicalSpace
146 (CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) :=
147 (completedGroupAlgebraSystem R G).topologicalSpace
148 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)
149 exact (continuous_completedGroupAlgebraFunctorialStageMap (R := R) (G := G) (H := H)
150 hG φ hφ V).comp
151 ((completedGroupAlgebraSystem R G).continuous_projection
152 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V))
153 exact Continuous.subtype_mk hval fun x =>
154 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x).2
156/-- The completed functorial map agrees with the abstract group-algebra map on the dense map. -/
158 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
159 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ).comp
160 (toCompletedGroupAlgebraRingHom R G) =
161 (toCompletedGroupAlgebraRingHom R H).comp (MonoidAlgebra.mapDomainRingHom R φ) := by
162 apply RingHom.ext
163 intro x
164 apply (completedGroupAlgebraSystem R H).ext
165 intro V
166 have hstage := congrFun
167 (congrArg DFunLike.coe
168 (completedGroupAlgebraFunctorialStageMap_comp_stageMap (R := R) (G := G) (H := H)
169 hG φ hφ V))
170 x
171 change completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
173 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x) =
174 completedGroupAlgebraStageMap R H V (MonoidAlgebra.mapDomainRingHom R φ x)
175 exact hstage
177end