Yamaguchi Lean 4 Library
ProCGroups/ProC/Kernels.lean
ProCGroups/ProC/Kernels/Source

ProCGroups/ProC/Kernels.lean

1import Mathlib.GroupTheory.Abelianization.Defs
2import ProCGroups.Abelian.TopologicalAbelianization
3import ProCGroups.ProC.Subgroups.Closed
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/ProC/Kernels.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Pro-C groups and open normal quotients
16Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
17-/
19namespace ProCGroups.ProC
21noncomputable section
23open scoped Pointwise
25universe u v
27variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30/-- The kernel subgroup of a continuous homomorphism. -/
31abbrev ProfiniteKernelSubgroup (psi : ContinuousMonoidHom G H) : Subgroup G :=
32 psi.toMonoidHom.ker
34omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
35/-- The kernel of a continuous homomorphism into a `T1` topological group is closed. -/
36theorem isClosed_profiniteKernelSubgroup [T1Space H] (psi : ContinuousMonoidHom G H) :
37 IsClosed ((ProfiniteKernelSubgroup psi : Subgroup G) : Set G) := by
38 simpa [ProfiniteKernelSubgroup, MonoidHom.mem_ker] using
39 (isClosed_singleton (x := (1 : H))).preimage psi.continuous_toFun
41/-- The topological kernel abelianization
42`ker psi / closure([ker psi, ker psi])`. -/
43abbrev ProfiniteKernelAbelianization (psi : ContinuousMonoidHom G H) : Type u :=
44 TopologicalAbelianization (ProfiniteKernelSubgroup psi)
46/-- Additive notation for the topological kernel abelianization. -/
47abbrev ProfiniteKernelAbelianizationAdd (psi : ContinuousMonoidHom G H) : Type u :=
50/-- Pro-`C` notation for the topological kernel abelianization.
52The `ProC` parameter records the ambient pro-`C` theory in theorem statements; the underlying type
53is the ordinary topological abelianization of the closed kernel. -/
55 (ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H) : Type u :=
56 let _proCMarker : ProCGroupPredicate.{u} := ProC
59/-- Additive notation for the pro-`C` kernel abelianization. -/
61 (ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H) : Type u :=
62 Additive (ProCKernelAbelianization ProC psi)
64/-- Canonical quotient map from the algebraic kernel abelianization to the topological kernel
65abelianization. -/
67 (psi : ContinuousMonoidHom G H) :
68 Abelianization (ProfiniteKernelSubgroup psi) →*
70 QuotientGroup.lift
72 (QuotientGroup.mk'
74 (by
75 intro x hx
76 exact
77 (QuotientGroup.eq_one_iff
81/-- Additive form of the quotient from `(ker psi)^ab` to the topological kernel
82abelianization. -/
84 (psi : ContinuousMonoidHom G H) :
85 Additive (Abelianization (ProfiniteKernelSubgroup psi)) →+
88 (G := G) (H := H) psi).toAdditive
90omit [IsTopologicalGroup H] in
91/-- The canonical quotient map sends the class of a kernel element to its class modulo the
92topological closure of the commutator subgroup. -/
93@[simp]
95 (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi) :
97 (G := G) (H := H) psi (Additive.ofMul (Abelianization.of n)) =
98 Additive.ofMul
99 (QuotientGroup.mk'
101 rfl
103omit [IsTopologicalGroup H] in
104/-- The canonical map from the algebraic kernel abelianization to the topological one is
105surjective. -/
107 (psi : ContinuousMonoidHom G H) :
108 Function.Surjective
110 (G := G) (H := H) psi) := by
111 intro x
112 change ∃ y : Additive (Abelianization (ProfiniteKernelSubgroup psi)),
113 Additive.ofMul
115 (G := G) (H := H) psi (Additive.toMul y)) = x
116 rcases QuotientGroup.mk'_surjective
118 (Additive.toMul x) with
119 ⟨n, hn⟩
120 refine ⟨Additive.ofMul (Abelianization.of n), ?_⟩
121 apply Additive.toMul.injective
122 simpa using hn
124omit [IsTopologicalGroup H] in
125/-- The closed kernel of a morphism out of a pro-`C` group is pro-`C`. -/
127 (ProC : ProCGroupPredicate.{u})
128 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
129 [ProC.DeterminedByFiniteQuotients] [ProCGroup ProC G]
130 [T1Space H] (psi : ContinuousMonoidHom G H) :
132 ProCGroup.of_isClosed_subgroup ProC (ProfiniteKernelSubgroup psi)
135omit [IsTopologicalGroup H] in
136/-- The closed kernel of a morphism between pro-`C` groups is pro-`C`.
138This form avoids an extra public `[T1Space H]` assumption because the pro-`C` target is Hausdorff. -/
140 (ProC : ProCGroupPredicate.{u})
141 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
142 [ProC.DeterminedByFiniteQuotients] [ProCGroup ProC G]
143 {H0 : Type u} [Group H0] [TopologicalSpace H0] [IsTopologicalGroup H0]
144 [ProCGroup ProC H0] (psi : ContinuousMonoidHom G H0) :
146 letI : T1Space H0 := ProCGroup.t1Space ProC H0
147 exact proCGroup_profiniteKernelSubgroup (G := G) (H := H0) ProC psi
149/-- Public namespace form: the kernel of a morphism of pro-`C` groups is pro-`C`. -/
150theorem ProCGroup.profiniteKernelSubgroup
151 (ProC : ProCGroupPredicate.{u})
152 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
153 [ProC.DeterminedByFiniteQuotients]
154 {G H0 : Type u}
155 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
156 [Group H0] [TopologicalSpace H0] [IsTopologicalGroup H0]
157 [ProCGroup ProC G] [ProCGroup ProC H0]
158 (psi : ContinuousMonoidHom G H0) :
161 (G := G) (H0 := H0) ProC psi
163omit [IsTopologicalGroup H] in
164/-- The topological kernel abelianization of a morphism out of a pro-`C` group is pro-`C`. -/
166 (ProC : ProCGroupPredicate.{u})
167 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
168 [ProC.DeterminedByFiniteQuotients] [ProCGroup ProC G]
169 [T1Space H] (psi : ContinuousMonoidHom G H) :
170 ProCGroup ProC (ProCKernelAbelianization ProC psi) := by
171 let N : Subgroup G := ProfiniteKernelSubgroup psi
172 letI : ProCGroup ProC N :=
173 proCGroup_profiniteKernelSubgroup (G := G) (H := H) ProC psi
175 exact ProCGroup.quotient_closedNormalSubgroup ProC
179omit [IsTopologicalGroup H] in
180/-- The topological kernel abelianization of a morphism between pro-`C` groups is pro-`C`,
181without an extra public `[T1Space H]` assumption. -/
183 (ProC : ProCGroupPredicate.{u})
184 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
185 [ProC.DeterminedByFiniteQuotients] [ProCGroup ProC G]
186 {H0 : Type u} [Group H0] [TopologicalSpace H0] [IsTopologicalGroup H0]
187 [ProCGroup ProC H0] (psi : ContinuousMonoidHom G H0) :
188 ProCGroup ProC (ProCKernelAbelianization ProC psi) := by
189 letI : T1Space H0 := ProCGroup.t1Space ProC H0
190 exact proCGroup_profiniteKernelAbelianization (G := G) (H := H0) ProC psi
192/-- Public namespace form: the topological `N^ab(C)` of a morphism of pro-`C` groups is pro-`C`. -/
193theorem ProCGroup.profiniteKernelAbelianization
194 (ProC : ProCGroupPredicate.{u})
195 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
196 [ProC.DeterminedByFiniteQuotients]
197 {G H0 : Type u}
198 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
199 [Group H0] [TopologicalSpace H0] [IsTopologicalGroup H0]
200 [ProCGroup ProC G] [ProCGroup ProC H0]
201 (psi : ContinuousMonoidHom G H0) :
204 (G := G) (H0 := H0) ProC psi
206end
208end ProCGroups.ProC