Source: ProCGroups.ProC.Kernels
1import Mathlib.GroupTheory.Abelianization.Defs
2import ProCGroups.Abelian.TopologicalAbelianization
3import ProCGroups.ProC.Subgroups.Closed
5/-!
6# Profinite kernels and their abelianizations
8This file equips kernels of continuous maps between profinite groups with their closed profinite
9topology and constructs the corresponding topological abelianization. It also transfers
10open-normal quotient bases in a finite-group class to these kernel constructions.
11-/
13namespace ProCGroups.ProC
15noncomputable section
17open scoped Pointwise
19universe u v
21variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
22variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
24/-- The kernel subgroup of a continuous homomorphism. -/
25abbrev ProfiniteKernelSubgroup (psi : ContinuousMonoidHom G H) : Subgroup G :=
26 psi.toMonoidHom.ker
28omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
29/-- The kernel of a continuous homomorphism into a \(T_1\) topological group is closed. -/
30theorem isClosed_profiniteKernelSubgroup [T1Space H] (psi : ContinuousMonoidHom G H) :
31 IsClosed ((ProfiniteKernelSubgroup psi : Subgroup G) : Set G) := by
32 change IsClosed (psi ⁻¹' ({1} : Set H))
33 exact (isClosed_singleton (x := (1 : H))).preimage psi.continuous_toFun
35/-- The topological kernel abelianization \(\ker \psi / \overline{[\ker \psi, \ker \psi]}\). -/
36abbrev ProfiniteKernelAbelianization (psi : ContinuousMonoidHom G H) : Type u :=
37 TopologicalAbelianization (ProfiniteKernelSubgroup psi)
39/-- Additive notation for the topological kernel abelianization. -/
40abbrev ProfiniteKernelAbelianizationAdd (psi : ContinuousMonoidHom G H) : Type u :=
41 Additive (ProfiniteKernelAbelianization psi)
43/--
44The canonical quotient map from the algebraic kernel abelianization to the topological kernel
45abelianization.
46-/
47def kernelAbelianizationToProfiniteKernelAbelianizationHom
48 (psi : ContinuousMonoidHom G H) :
49 Abelianization (ProfiniteKernelSubgroup psi) →*
50 ProfiniteKernelAbelianization psi :=
51 QuotientGroup.lift
52 (commutator (ProfiniteKernelSubgroup psi))
53 (QuotientGroup.mk'
54 (Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)))
55 (by
56 intro x hx
57 exact
58 (QuotientGroup.eq_one_iff
59 (N := Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) x).2
60 (Subgroup.commutator_le_closedCommutator (ProfiniteKernelSubgroup psi) hx))
62/--
63Additive form of the quotient from \((\ker \psi)^{ab}\) to the topological kernel
64abelianization.
65-/
66def kernelAbelianizationToProfiniteKernelAbelianization
67 (psi : ContinuousMonoidHom G H) :
68 Additive (Abelianization (ProfiniteKernelSubgroup psi)) →+
69 ProfiniteKernelAbelianizationAdd psi :=
70 (kernelAbelianizationToProfiniteKernelAbelianizationHom
71 (G := G) (H := H) psi).toAdditive
73omit [IsTopologicalGroup H] in
74/--
75The canonical quotient map sends the class of a kernel element to its class modulo the
76topological closure of the commutator subgroup.
77-/
78@[simp]
79theorem kernelAbelianizationToProfiniteKernelAbelianization_of
80 (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi) :
81 kernelAbelianizationToProfiniteKernelAbelianization
82 (G := G) (H := H) psi (Additive.ofMul (Abelianization.of n)) =
83 Additive.ofMul
84 (QuotientGroup.mk'
85 (Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) n) := by
86 rfl
88omit [IsTopologicalGroup H] in
89/--
90The canonical map from the algebraic kernel abelianization to the topological one is surjective.
91-/
92theorem kernelAbelianizationToProfiniteKernelAbelianization_surjective
93 (psi : ContinuousMonoidHom G H) :
94 Function.Surjective
95 (kernelAbelianizationToProfiniteKernelAbelianization
96 (G := G) (H := H) psi) := by
97 intro x
98 change ∃ y : Additive (Abelianization (ProfiniteKernelSubgroup psi)),
99 Additive.ofMul
100 (kernelAbelianizationToProfiniteKernelAbelianizationHom
101 (G := G) (H := H) psi (Additive.toMul y)) = x
102 rcases QuotientGroup.mk'_surjective
103 (Subgroup.closedCommutator (ProfiniteKernelSubgroup psi))
104 (Additive.toMul x) with
105 ⟨n, hn⟩
106 refine ⟨Additive.ofMul (Abelianization.of n), ?_⟩
107 apply Additive.toMul.injective
108 change
109 QuotientGroup.mk'
110 (Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) n =
111 Additive.toMul x
112 exact hn
114omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
115/-- The closed kernel of a morphism out of a group with an open-normal \(C\)-basis again has such a
116basis. -/
117theorem HasOpenNormalBasisInClass.profiniteKernelSubgroup
118 {C : FiniteGroupClass.{u}}
119 (hHer : FiniteGroupClass.Hereditary C) (hG : HasOpenNormalBasisInClass C G)
120 [T1Space H] (psi : ContinuousMonoidHom G H) :
121 HasOpenNormalBasisInClass C (ProfiniteKernelSubgroup psi) :=
122 HasOpenNormalBasisInClass.of_isClosed_subgroup
123 C.isomClosed hHer.subgroupClosed hG (ProfiniteKernelSubgroup psi)
124 (isClosed_profiniteKernelSubgroup psi)
126omit [IsTopologicalGroup H] in
127/-- The topological kernel abelianization of a morphism out of a group with an open-normal
128\(C\)-basis again has such a basis. -/
129theorem HasOpenNormalBasisInClass.profiniteKernelAbelianization
130 {C : FiniteGroupClass.{u}}
131 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
132 (hC : FiniteGroupClass.FullFormation C) (hG : HasOpenNormalBasisInClass C G)
133 [T1Space H] (psi : ContinuousMonoidHom G H) :
134 HasOpenNormalBasisInClass C (ProfiniteKernelAbelianization psi) := by
135 let N : Subgroup G := ProfiniteKernelSubgroup psi
136 letI : IsClosed (N : Set G) := isClosed_profiniteKernelSubgroup psi
137 letI : CompactSpace N :=
138 (show IsClosed (N : Set G) from inferInstance).isClosedEmbedding_subtypeVal.compactSpace
139 letI : T2Space N := by infer_instance
140 letI : TotallyDisconnectedSpace N := by infer_instance
141 have hN : HasOpenNormalBasisInClass C N :=
142 HasOpenNormalBasisInClass.profiniteKernelSubgroup hC.hereditary hG psi
143 change HasOpenNormalBasisInClass C (N ⧸ Subgroup.closedCommutator N)
144 exact quotient_closedNormalSubgroup
145 hC.isomClosed hC.quotientClosed hN
148end
150end ProCGroups.ProC