ProCGroups/ProC/GroupPredicates/Abelian.lean
1import ProCGroups.ProC.GroupPredicates.Standard
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/ProC/GroupPredicates/Abelian.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Pro-C groups and open normal quotients
14Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
15-/
17open Set
18open scoped Topology Pointwise
20namespace ProCGroups.ProC
22universe u v
24open InverseSystems
26section
28variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30namespace IsProabelianGroup
32/-- Every proabelian group is abelian. -/
33theorem isAbelian (hG : IsProabelianGroup G) : ∀ a b : G, a * b = b * a := by
34 letI : CompactSpace G := IsProCGroup.compactSpace hG
35 letI : T2Space G := IsProCGroup.t2Space hG
36 letI : TotallyDisconnectedSpace G := IsProCGroup.totallyDisconnectedSpace hG
37 intro a b
38 have hcomm_mem : ∀ U : OpenNormalSubgroup G, a * b * a⁻¹ * b⁻¹ ∈ (U : Subgroup G) := by
39 intro U
40 have hab :
41 QuotientGroup.mk' (U : Subgroup G) a * QuotientGroup.mk' (U : Subgroup G) b =
42 QuotientGroup.mk' (U : Subgroup G) b * QuotientGroup.mk' (U : Subgroup G) a :=
43 (hG.quotient_mem FiniteGroupClass.abelian_formation U).2 _ _
44 refine (QuotientGroup.eq_one_iff (N := (U : Subgroup G)) _).1 ?_
45 have h :=
46 congrArg (fun z : G ⧸ (U : Subgroup G) =>
47 z * ((QuotientGroup.mk' (U : Subgroup G) a)⁻¹ *
48 (QuotientGroup.mk' (U : Subgroup G) b)⁻¹)) hab
50 have hcomm_one : a * b * a⁻¹ * b⁻¹ = 1 := by
51 apply IsProfiniteGroup.eq_one_of_mem_all_openNormalSubgroups (G := G)
52 intro U
53 exact hcomm_mem U
54 have h1 : a * b * a⁻¹ = b := by
55 have h := congrArg (fun x : G => x * b) hcomm_one
56 simpa [mul_assoc] using h
57 have h2 : a * b = b * a := by
58 have h := congrArg (fun x : G => x * a) h1
59 simpa [mul_assoc] using h
60 exact h2
63end
65end ProCGroups.ProC