CompletedGroupAlgebra/InClassFunctoriality/ComapIndex.lean
1import CompletedGroupAlgebra.Basic.InClass.Index
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/InClassFunctoriality/ComapIndex.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
26universe u v w
28variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
29variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34/-- The inverse image of a `C`-quotient of `H` along a continuous homomorphism `G -> H`,
35again as a `C`-quotient of `G`, when `C` is hereditary. -/
36def completedGroupAlgebraComapIndexInClass
37 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
38 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
39 CompletedGroupAlgebraIndexInClass G C :=
40 let φc : G →ₜ* H := { toMonoidHom := φ, continuous_toFun := hφ }
41 OrderDual.toDual
42 (OpenNormalSubgroupInClass.comap (C := C) (G := G) hHer φc (OrderDual.ofDual V))
44omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
45/-- The comap of an open normal subgroup along a continuous homomorphism is again open normal. -/
46@[simp]
48 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
49 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
50 (((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
51 (G := G) (H := H) C hHer φ hφ V)).1 : OpenNormalSubgroup G) : Subgroup G) =
52 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ :=
53 rfl
55omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
56/-- Comap indices are monotone with respect to refinement of open normal subgroups. -/
57theorem completedGroupAlgebraComapIndexInClass_mono
58 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
59 (φ : G →* H) (hφ : Continuous φ)
60 {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
61 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V ≤
62 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W := by
63 change (((OrderDual.ofDual W).1 : OpenNormalSubgroup H) : Subgroup H).comap φ ≤
64 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ
65 exact Subgroup.comap_mono hVW
67/-- The quotient homomorphism `G/φ⁻¹(V) -> H/V` for a `C`-indexed quotient. -/
68def completedGroupAlgebraComapQuotientMapInClass
69 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
70 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
71 CompletedGroupAlgebraQuotientInClass G C
72 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) →*
73 CompletedGroupAlgebraQuotientInClass H C V :=
74 QuotientGroup.map _ _ φ (by
75 intro g hg
76 exact hg)
78/-- The quotient map attached to a comap index sends a coset to the coset of its image. -/
79@[simp]
80theorem completedGroupAlgebraComapQuotientMapInClass_mk
81 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
82 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) (g : G) :
83 completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V
84 (QuotientGroup.mk'
85 ((((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
86 (G := G) (H := H) C hHer φ hφ V)).1 : OpenNormalSubgroup G) :
87 Subgroup G)) g) =
88 QuotientGroup.mk' ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H))
89 (φ g) :=
90 rfl
92/-- A surjective group homomorphism induces a surjective map on the corresponding finite quotients. -/
93theorem completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
94 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
95 (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ)
96 (V : CompletedGroupAlgebraIndexInClass H C) :
97 Function.Surjective
98 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V) := by
99 intro q
100 rcases QuotientGroup.mk'_surjective
101 ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H)) q with
102 ⟨h, rfl⟩
103 rcases hφsurj h with ⟨g, rfl⟩
104 refine ⟨QuotientGroup.mk'
105 ((((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
106 (G := G) (H := H) C hHer φ hφ V)).1 : OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
107 rw [completedGroupAlgebraComapQuotientMapInClass_mk]
109@[simp]
110theorem completedGroupAlgebraComapQuotientMapInClass_compatible
111 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
112 (φ : G →* H) (hφ : Continuous φ)
113 {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
114 (OpenNormalSubgroupInClass.map
115 (C := C) (G := H)
116 (U := OrderDual.ofDual V) (V := OrderDual.ofDual W) hVW).comp
117 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ W) =
118 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V).comp
119 (OpenNormalSubgroupInClass.map
120 (C := C) (G := G)
121 (U := OrderDual.ofDual
122 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
123 (V := OrderDual.ofDual
124 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W))
125 (completedGroupAlgebraComapIndexInClass_mono
126 (G := G) (H := H) C hHer φ hφ hVW)) := by
127 ext q
128 rcases QuotientGroup.mk'_surjective
129 ((((OrderDual.ofDual
130 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W)).1 :
131 OpenNormalSubgroup G) : Subgroup G)) q with ⟨g, rfl⟩
132 rfl
134end