Source: ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Comap
1import ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Index
3/-!
4# Completed Group Algebra / All Finite Functoriality / Comap
6This module constructs the inverse-image finite quotient attached to a continuous group
7homomorphism and the induced quotient homomorphism. It is the index-level input for all-finite
8functoriality and has no dependency on augmentation theory.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
20universe v
22variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
23variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
25/--
26The inverse image of an open-finite quotient of \(H\) along a continuous homomorphism \(G\to
27H\), regarded as an open-finite quotient of the profinite group \(G\). This is the index-level
28operation underlying Lemma 5.3.5(e)'s functoriality in the group variable.
29-/
30def completedGroupAlgebraComapIndex
31 (φ : G →* H) (hφ : Continuous φ)
32 (V : CompletedGroupAlgebraIndex H) : CompletedGroupAlgebraIndex G := by
33 let V₀ : OpenNormalSubgroup H := (OrderDual.ofDual V).1
34 let W : OpenNormalSubgroup G := ProCGroups.OpenNormalSubgroup.comap φ hφ V₀
35 refine OrderDual.toDual ⟨W, ?_⟩
36 let f : G ⧸ (W : Subgroup G) →* H ⧸ (V₀ : Subgroup H) :=
37 QuotientGroup.map _ _ φ (by
38 intro g hg
39 simpa [W, V₀] using hg)
40 have hf : Function.Injective f := by
41 intro x y hxy
42 rcases QuotientGroup.mk'_surjective (W : Subgroup G) x with ⟨a, rfl⟩
43 rcases QuotientGroup.mk'_surjective (W : Subgroup G) y with ⟨b, rfl⟩
44 apply QuotientGroup.eq.2
45 change φ (a⁻¹ * b) ∈ (V₀ : Subgroup H)
46 have hv : (φ a)⁻¹ * φ b ∈ (V₀ : Subgroup H) := QuotientGroup.eq.1 hxy
47 simpa using hv
48 letI : Finite (H ⧸ (V₀ : Subgroup H)) := (OrderDual.ofDual V).2
49 exact Finite.of_injective f hf
51omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
52/-- The subgroup underlying the comap index is the subgroup-theoretic comap. -/
53@[simp]
54theorem completedGroupAlgebraComapIndex_subgroup
55 (φ : G →* H) (hφ : Continuous φ)
56 (V : CompletedGroupAlgebraIndex H) :
57 (((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) φ hφ V)).1 :
58 OpenNormalSubgroup G) : Subgroup G) =
59 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ :=
60 rfl
62omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
63/-- Comap of all-finite completed-group-algebra indices is monotone. -/
64theorem completedGroupAlgebraComapIndex_mono
65 (φ : G →* H) (hφ : Continuous φ)
66 {V W : CompletedGroupAlgebraIndex H} (hVW : V ≤ W) :
67 completedGroupAlgebraComapIndex (G := G) φ hφ V ≤
68 completedGroupAlgebraComapIndex (G := G) φ hφ W := by
69 change (((OrderDual.ofDual W).1 : OpenNormalSubgroup H) : Subgroup H).comap φ ≤
70 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ
71 exact Subgroup.comap_mono hVW
73/--
74The quotient homomorphism \(G/\varphi^{-1}(V) \to H/V\) induced by a continuous homomorphism
75\(\varphi: G \to H\).
76-/
77def completedGroupAlgebraComapQuotientMap
78 (φ : G →* H) (hφ : Continuous φ)
79 (V : CompletedGroupAlgebraIndex H) :
80 CompletedGroupAlgebraQuotient G (completedGroupAlgebraComapIndex (G := G) φ hφ V) →*
81 CompletedGroupAlgebraQuotient H V :=
82 QuotientGroup.map _ _ φ (by
83 intro g hg
84 exact hg)
86/--
87The quotient map associated with the inverse-image subgroup sends the class of \(g\in G\) to the
88class of \(\varphi(g)\in H\).
89-/
90@[simp]
91theorem completedGroupAlgebraComapQuotientMap_mk
92 (φ : G →* H) (hφ : Continuous φ)
93 (V : CompletedGroupAlgebraIndex H) (g : G) :
94 completedGroupAlgebraComapQuotientMap (G := G) φ hφ V
95 (QuotientGroup.mk'
96 ((((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) φ hφ V)).1 :
97 OpenNormalSubgroup G) : Subgroup G)) g) =
98 QuotientGroup.mk'
99 ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H)) (φ g) :=
100 rfl
102/-- A surjective homomorphism induces a surjective map on the comap quotients. -/
103theorem completedGroupAlgebraComapQuotientMap_surjective
104 (φ : G →* H) (hφ : Continuous φ)
105 (hφsurj : Function.Surjective φ) (V : CompletedGroupAlgebraIndex H) :
106 Function.Surjective (completedGroupAlgebraComapQuotientMap (G := G) φ hφ V) := by
107 intro q
108 rcases QuotientGroup.mk'_surjective
109 ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H)) q with
110 ⟨h, rfl⟩
111 rcases hφsurj h with ⟨g, rfl⟩
112 refine ⟨QuotientGroup.mk'
113 ((((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) φ hφ V)).1 :
114 OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
115 rw [completedGroupAlgebraComapQuotientMap_mk]
117end
119end CompletedGroupAlgebra