CompletedGroupAlgebra/AllFiniteFunctoriality/StageMap.lean
1import CompletedGroupAlgebra.AllFiniteFunctoriality.Comap
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/AllFiniteFunctoriality/StageMap.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finite-stage maps for completed group algebra functoriality
13-/
15open scoped Topology
17namespace CompletedGroupAlgebra
19noncomputable section
21open ProCGroups
22open ProCGroups.ProC
24universe u v w
26variable (R : Type u) [CommRing R]
27variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30/-- The finite-stage map `R[G/φ⁻¹(V)] -> R[H/V]` induced by `φ : G -> H`. -/
32 (R : Type u) [CommRing R] (hG : ProCGroups.IsProfiniteGroup G)
33 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndex H) :
34 CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) →+*
35 CompletedGroupAlgebraStage R H V :=
36 MonoidAlgebra.mapDomainRingHom R
37 (completedGroupAlgebraComapQuotientMap (G := G) hG φ hφ V)
39/-- A surjective group homomorphism induces a surjective finite-stage algebra map. -/
41 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
42 (hφsurj : Function.Surjective φ) (V : CompletedGroupAlgebraIndex H) :
43 Function.Surjective
45 (G := G) (H := H) (R := R) hG φ hφ V) := by
46 simpa [completedGroupAlgebraFunctorialStageMap, MonoidAlgebra.mapDomainRingHom_apply] using
47 (Finsupp.mapDomain_surjective (M := R)
48 (completedGroupAlgebraComapQuotientMap_surjective
49 (G := G) hG φ hφ hφsurj V))
51/-- The finite-stage functorial map sends singleton coefficients to singleton coefficients. -/
52@[simp]
54 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
55 (V : CompletedGroupAlgebraIndex H)
56 (q : CompletedGroupAlgebraQuotient G
57 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) (r : R) :
58 completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
59 (MonoidAlgebra.single q r) =
60 MonoidAlgebra.single (completedGroupAlgebraComapQuotientMap (G := G) hG φ hφ V q) r := by
61 classical
62 simp only [completedGroupAlgebraFunctorialStageMap, MonoidAlgebra.single,
63 MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
65/-- The finite-stage functorial map preserves scalar algebra-map elements. -/
67 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
68 (V : CompletedGroupAlgebraIndex H) (r : R) :
69 completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
70 (algebraMap R
72 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) r) =
73 algebraMap R (CompletedGroupAlgebraStage R H V) r := by
74 simp only [completedGroupAlgebraFunctorialStageMap, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
75 RingHom.coe_id, Function.comp_apply, id_eq, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]
77/-- The finite-stage functorial map is continuous for the finite-stage topologies. -/
79 [TopologicalSpace R] [IsTopologicalRing R]
80 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
81 (V : CompletedGroupAlgebraIndex H) :
82 letI : TopologicalSpace
83 (CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) :=
84 (completedGroupAlgebraSystem R G).topologicalSpace
85 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)
86 letI : TopologicalSpace (CompletedGroupAlgebraStage R H V) :=
87 (completedGroupAlgebraSystem R H).topologicalSpace V
88 Continuous (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
89 hG φ hφ V) := by
90 letI : TopologicalSpace
91 (CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) :=
92 (completedGroupAlgebraSystem R G).topologicalSpace
93 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)
94 letI : TopologicalSpace (CompletedGroupAlgebraStage R H V) :=
95 (completedGroupAlgebraSystem R H).topologicalSpace V
97 (CompletedGroupAlgebraQuotient G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V))
99 (completedGroupAlgebraComapQuotientMap (G := G) hG φ hφ V)
101/-- Finite-stage functorial maps commute with transition maps. -/
102@[simp]
104 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
105 {V W : CompletedGroupAlgebraIndex H} (hVW : V ≤ W) :
106 (completedGroupAlgebraTransition R H hVW).comp
107 (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ W) =
108 (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V).comp
110 (completedGroupAlgebraComapIndex_mono (G := G) hG φ hφ hVW)) := by
113 ← MonoidAlgebra.mapDomainRingHom_comp, ← MonoidAlgebra.mapDomainRingHom_comp]
114 congr 1
115 apply MonoidHom.ext
116 intro q
117 rcases QuotientGroup.mk'_surjective
118 ((((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) hG φ hφ W)).1 :
119 OpenNormalSubgroup G) : Subgroup G)) q with
120 ⟨g, rfl⟩
121 rfl
123/-- The finite-stage functorial map agrees with the dense stage map after applying `φ`. -/
124@[simp]
126 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
127 (V : CompletedGroupAlgebraIndex H) :
128 (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V).comp
130 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) =
131 (completedGroupAlgebraStageMap R H V).comp
132 (MonoidAlgebra.mapDomainRingHom R φ) := by
134 completedGroupAlgebraStageMap, ← MonoidAlgebra.mapDomainRingHom_comp,
135 ← MonoidAlgebra.mapDomainRingHom_comp]
136 congr 1
138end