ProCGroups/FiniteStepSolvableQuotients/Commutators/Basic.lean
1import ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients
2import ProCGroups.ProC.GroupPredicates.Abelian
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/FiniteStepSolvableQuotients/Commutators/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
15Develops topological derived series, maximal solvable quotients of bounded derived length, commutator closure formulas, and abelian-action consequences.
16-/
18open scoped Topology
20namespace ProCGroups.FiniteStepSolvableQuotients
22universe u
24/-- The topological closure of the abstract commutator subgroup. -/
25abbrev topologicalCommutator
26 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Subgroup G :=
29@[simp] theorem topologicalCommutator_eq_closedCommutator_top_top
30 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
31 topologicalCommutator G = closedCommutator (⊤ : Subgroup G) ⊤ := by
32 simp only [topologicalCommutator, commutator, closedCommutator]
34@[simp] theorem topDerivedTop_one_eq_topologicalCommutator
35 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
36 topDerivedTop G 1 = topologicalCommutator G := by
37 simp only [topDerivedTop, closedDerivedSeries, closedCommutator, topologicalCommutator, commutator]
39/-- The first closed derived subgroup of the whole group is the closed commutator subgroup. -/
41 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
42 closedDerivedSeries (G := G) (⊤ : Subgroup G) 1 =
43 Subgroup.closedCommutator G := by
44 calc
45 closedDerivedSeries (G := G) (⊤ : Subgroup G) 1 = topDerivedTop G 1 := rfl
47 _ = Subgroup.closedCommutator G := rfl
49@[simp] theorem topologicalCommutator_eq_commutator_of_isClosed
50 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
51 (hclosed : IsClosed ((commutator G : Subgroup G) : Set G)) :
52 topologicalCommutator G = commutator G := by
53 ext x
54 change x ∈ closure ((commutator G : Set G)) ↔ x ∈ (commutator G : Set G)
55 rw [closure_eq_iff_isClosed.mpr hclosed]
57/-- In a compact Hausdorff topological group, the set of individual commutators is closed. -/
58theorem isClosed_commutatorSet
59 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
60 [CompactSpace G] [T2Space G] :
61 IsClosed (commutatorSet G : Set G) := by
62 let f : G × G → G := fun p => ⁅p.1, p.2⁆
63 have hf : Continuous f := by
64 have hfst : Continuous fun p : G × G => p.1 := continuous_fst
65 have hsnd : Continuous fun p : G × G => p.2 := continuous_snd
66 simpa [f, commutatorElement_def, mul_assoc] using
67 (((hfst.mul hsnd).mul hfst.inv).mul hsnd.inv)
68 have himage : f '' (Set.univ : Set (G × G)) = commutatorSet G := by
69 ext z
70 constructor
71 · rintro ⟨p, -, rfl⟩
72 exact commutator_mem_commutatorSet (g₁ := p.1) (g₂ := p.2)
73 · intro hz
74 rcases mem_commutatorSet_iff.mp hz with ⟨x, y, rfl⟩
75 exact ⟨(x, y), by simp only [Set.mem_univ], rfl⟩
76 simpa [himage] using (isCompact_univ.image hf).isClosed
79 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
80 commutator G ≤ topologicalCommutator G :=
81 Subgroup.le_topologicalClosure _
83@[simp] theorem topologicalCommutator_eq_bot_of_commGroup
84 (G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
85 topologicalCommutator G = ⊥ := by
86 have hcomm : commutator G = ⊥ := by
87 rw [commutator_eq_bot_iff_center_eq_top, CommGroup.center_eq_top]
88 rw [topologicalCommutator, hcomm]
89 ext x
90 change x ∈ closure ({(1 : G)} : Set G) ↔ x ∈ (⊥ : Subgroup G)
91 rw [closure_singleton]
92 simp only [Set.mem_singleton_iff, Subgroup.mem_bot]
94/-- A commutative topological group has trivial positive closed derived stages. -/
96 {G : Type u} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G]
97 {m : ℕ} (hm : 1 ≤ m) :
98 topDerivedTop G m = ⊥ := by
99 have h1 : topDerivedTop G 1 = (⊥ : Subgroup G) := by
102 have hle : topDerivedTop G m ≤ topDerivedTop G 1 :=
103 (topDerivedTop_antitone (G := G)) hm
104 have hlebot : topDerivedTop G m ≤ (⊥ : Subgroup G) := by
105 rw [← h1]
106 exact hle
107 exact le_antisymm hlebot bot_le
109/-- A procyclic group has trivial positive closed derived stages. -/
111 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
112 (hG : ProCGroups.ProC.IsProcyclicGroup G) {m : ℕ} (hm : 1 ≤ m) :
113 topDerivedTop G m = ⊥ := by
114 letI : T2Space G := hG.t2Space
115 have hcomm : ∀ a b : G, a * b = b * a :=
117 (ProCGroups.ProC.IsProcyclicGroup.isProabelianGroup (G := G) hG)
118 let base : Group G := inferInstance
119 letI : CommGroup G := { base with mul_comm := hcomm }
120 exact topDerivedTop_eq_bot_of_commGroup hm
122/-- Images of a topologically cyclic source in a discrete quotient of a maximal solvable quotient
123are algebraic powers of the image of the chosen generator. -/
125 {Ω A B : Type u}
126 [TopologicalSpace Ω] [Group Ω] [IsTopologicalGroup Ω]
127 [TopologicalSpace A] [Group A] [IsTopologicalGroup A]
128 [TopologicalSpace B] [Group B] [IsTopologicalGroup B] [DiscreteTopology B]
129 {m : ℕ}
130 (q : MaxSolvQuot Ω m →* B) (hq : Continuous q)
131 (ιC : A →ₜ* Ω) {x a : A}
132 (hxgen : ProCGroups.Generation.TopologicallyGenerates (G := A) ({x} : Set A)) :
133 q (continuousToMaxSolvQuot Ω m (ιC a)) ∈
134 Subgroup.zpowers (q (continuousToMaxSolvQuot Ω m (ιC x))) := by
135 let f : A →* B := (q.comp (continuousToMaxSolvQuot Ω m : Ω →* MaxSolvQuot Ω m)).comp ιC
136 have hf : Continuous f := by
137 exact hq.comp ((continuousToMaxSolvQuot Ω m).continuous_toFun.comp ιC.continuous_toFun)
138 simpa [f] using
140 (A := A) f hf hxgen (a := a)
142/-- `g` can be written as a product of at most `n` commutators. -/
144 {G : Type u} [Group G] (n : ℕ) (g : G) : Prop :=
145 ∃ l : List (G × G), l.length ≤ n ∧ (l.map fun p => ⁅p.1, p.2⁆).prod = g
147theorem isProductOfCommutatorsLE_one
148 {G : Type u} [Group G] (n : ℕ) :
149 IsProductOfCommutatorsLE n (1 : G) := by
150 refine ⟨[], Nat.zero_le _, ?_⟩
151 simp only [List.map_nil, List.prod_nil]
154 {G : Type u} [Group G] (x y : G) :
155 IsProductOfCommutatorsLE 1 ⁅x, y⁆ := by
156 refine ⟨[(x, y)], by simp only [List.length_cons, List.length_nil, zero_add, le_refl], ?_⟩
157 simp only [List.map_cons, List.map_nil, List.prod_cons, List.prod_nil, mul_one]
159theorem IsProductOfCommutatorsLE.mul
160 {G : Type u} [Group G]
161 {m n : ℕ} {g h : G}
162 (hg : IsProductOfCommutatorsLE m g)
163 (hh : IsProductOfCommutatorsLE n h) :
164 IsProductOfCommutatorsLE (m + n) (g * h) := by
165 rcases hg with ⟨lg, hlg, rfl⟩
166 rcases hh with ⟨lh, hlh, rfl⟩
167 refine ⟨lg ++ lh, by simpa using Nat.add_le_add hlg hlh, ?_⟩
168 simp only [List.map_append, List.prod_append]
170/-- A product of at most `m` commutators is also a product of at most any larger bound `n`. -/
171theorem IsProductOfCommutatorsLE.mono
172 {G : Type u} [Group G]
173 {m n : ℕ} {g : G}
174 (hg : IsProductOfCommutatorsLE m g)
175 (hmn : m ≤ n) :
176 IsProductOfCommutatorsLE n g := by
177 rcases hg with ⟨l, hl, hprod⟩
178 exact ⟨l, le_trans hl hmn, hprod⟩
181 {G : Type u} [Group G]
182 {n : ℕ} {g : G}
183 (hg : IsProductOfCommutatorsLE n g) :
184 g ∈ commutator G := by
185 rcases hg with ⟨l, -, rfl⟩
186 induction l with
187 | nil =>
188 simp only [commutator, List.map_nil, List.prod_nil, one_mem]
189 | cons a t ih =>
190 have ha : ⁅a.1, a.2⁆ ∈ commutator G := by
191 rw [commutator_eq_closure]
192 exact Subgroup.subset_closure (commutator_mem_commutatorSet (g₁ := a.1) (g₂ := a.2))
193 exact Subgroup.mul_mem _ ha ih
195end ProCGroups.FiniteStepSolvableQuotients