Source: ProCGroups.ProC.GroupPredicates.Abelian
1import ProCGroups.ProC.InverseLimits.Predicates
3/-!
4# Abelian open-normal quotient bases
6This file proves that a profinite group with an abelian open-normal quotient basis is itself
7abelian. The proof tests commutators in all open normal quotients and then uses profinite
8separation.
9-/
11open Set
12open scoped Topology Pointwise
14namespace ProCGroups.ProC
16universe u v
18open InverseSystems
20section
22variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
23 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
25namespace HasAbelianOpenNormalBasis
27omit [T2Space G] in
28/-- A profinite group with an abelian open-normal quotient basis is abelian. -/
29theorem isAbelian (hG : HasAbelianOpenNormalBasis G) : ∀ a b : G, a * b = b * a := by
30 intro a b
31 have hcomm_mem : ∀ U : OpenNormalSubgroup G, a * b * a⁻¹ * b⁻¹ ∈ (U : Subgroup G) := by
32 intro U
33 have hab :
34 QuotientGroup.mk' (U : Subgroup G) a * QuotientGroup.mk' (U : Subgroup G) b =
35 QuotientGroup.mk' (U : Subgroup G) b * QuotientGroup.mk' (U : Subgroup G) a :=
36 (hG.quotient_mem FiniteGroupClass.abelian_formation U).2 _ _
37 refine (QuotientGroup.eq_one_iff (N := (U : Subgroup G)) _).1 ?_
38 have h :=
39 congrArg (fun z : G ⧸ (U : Subgroup G) =>
40 z * ((QuotientGroup.mk' (U : Subgroup G) a)⁻¹ *
41 (QuotientGroup.mk' (U : Subgroup G) b)⁻¹)) hab
42 simpa [map_mul, mul_assoc] using h
43 have hcomm_one : a * b * a⁻¹ * b⁻¹ = 1 := by
44 apply ProfiniteGrp.eq_one_of_mem_all_openNormalSubgroups (G := G)
45 intro U
46 exact hcomm_mem U
47 have h1 : a * b * a⁻¹ = b := by
48 have h := congrArg (fun x : G => x * b) hcomm_one
49 simpa [mul_assoc] using h
50 have h2 : a * b = b * a := by
51 have h := congrArg (fun x : G => x * a) h1
52 simpa [mul_assoc] using h
53 exact h2
55end HasAbelianOpenNormalBasis
56end
58end ProCGroups.ProC