Source: ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.ComapIndex
1import ProCGroups.CompletedGroupAlgebra.Basic.InClass.Index
3/-!
4# Pulling back in-class quotient indices
6An open-normal quotient index on the target pulls back along a continuous group homomorphism to
7an index on the source. This file defines that comap, the induced finite quotient map, and its
8monotonicity, compatibility, and surjectivity properties.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
19open ProCGroups.InverseSystems
21universe u v w
23variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
24variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
25variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
27variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
29/--
30The inverse image of a \(C\)-quotient of \(H\) along a continuous homomorphism \(G\to H\), again
31as a \(C\)-quotient of \(G\), when \(C\) is hereditary.
32-/
33def completedGroupAlgebraComapIndexInClass
34 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
35 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
36 CompletedGroupAlgebraIndexInClass G C :=
37 let φc : G →ₜ* H := { toMonoidHom := φ, continuous_toFun := hφ }
38 OrderDual.toDual
39 (OpenNormalSubgroupInClass.comap (C := C) (G := G) hHer φc (OrderDual.ofDual V))
41omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
42/-- The comap of an open normal subgroup along a continuous homomorphism is again open normal. -/
43@[simp]
44theorem completedGroupAlgebraComapIndexInClass_subgroup
45 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
46 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
47 (((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
48 (G := G) (H := H) C hHer φ hφ V)).1 : OpenNormalSubgroup G) : Subgroup G) =
49 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ :=
50 rfl
52omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
53/-- Comap indices are monotone with respect to refinement of open normal subgroups. -/
54theorem completedGroupAlgebraComapIndexInClass_mono
55 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
56 (φ : G →* H) (hφ : Continuous φ)
57 {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
58 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V ≤
59 completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W := by
60 change (((OrderDual.ofDual W).1 : OpenNormalSubgroup H) : Subgroup H).comap φ ≤
61 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ
62 exact Subgroup.comap_mono hVW
64/-- The quotient homomorphism \(G/\varphi^{-1}(V) \to H/V\) for a \(C\)-indexed quotient. -/
65def completedGroupAlgebraComapQuotientMapInClass
66 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
67 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
68 CompletedGroupAlgebraQuotientInClass G C
69 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) →*
70 CompletedGroupAlgebraQuotientInClass H C V :=
71 QuotientGroup.map _ _ φ (by
72 intro g hg
73 exact hg)
75/-- The quotient map attached to a comap index sends a coset to the coset of its image. -/
76@[simp]
77theorem completedGroupAlgebraComapQuotientMapInClass_mk
78 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
79 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) (g : G) :
80 completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V
81 (QuotientGroup.mk'
82 ((((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
83 (G := G) (H := H) C hHer φ hφ V)).1 : OpenNormalSubgroup G) :
84 Subgroup G)) g) =
85 QuotientGroup.mk' ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H))
86 (φ g) :=
87 rfl
89/--
90A surjective group homomorphism induces a surjective map on the corresponding finite quotients.
91-/
92theorem completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
93 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
94 (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ)
95 (V : CompletedGroupAlgebraIndexInClass H C) :
96 Function.Surjective
97 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V) := by
98 intro q
99 rcases QuotientGroup.mk'_surjective
100 ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H)) q with
101 ⟨h, rfl⟩
102 rcases hφsurj h with ⟨g, rfl⟩
103 refine ⟨QuotientGroup.mk'
104 ((((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
105 (G := G) (H := H) C hHer φ hφ V)).1 : OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
106 rw [completedGroupAlgebraComapQuotientMapInClass_mk]
108/--
109The class-restricted completed group-algebra pullback quotient map is compatible with transition
110maps and coordinate projections for the completed group algebra.
111-/
112@[simp]
113theorem completedGroupAlgebraComapQuotientMapInClass_compatible
114 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
115 (φ : G →* H) (hφ : Continuous φ)
116 {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
117 (OpenNormalSubgroupInClass.map
118 (C := C) (G := H)
119 (U := OrderDual.ofDual V) (V := OrderDual.ofDual W) hVW).comp
120 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ W) =
121 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V).comp
122 (OpenNormalSubgroupInClass.map
123 (C := C) (G := G)
124 (U := OrderDual.ofDual
125 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
126 (V := OrderDual.ofDual
127 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W))
128 (completedGroupAlgebraComapIndexInClass_mono
129 (G := G) (H := H) C hHer φ hφ hVW)) := by
130 ext q
131 rcases QuotientGroup.mk'_surjective
132 ((((OrderDual.ofDual
133 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W)).1 :
134 OpenNormalSubgroup G) : Subgroup G)) q with ⟨g, rfl⟩
135 rfl
137end
139end CompletedGroupAlgebra