Source: ProCGroups.FiniteStepSolvableQuotients.Commutators.Basic

1import ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients

2import ProCGroups.ProC.GroupPredicates.Abelian

4/-!

5# The topological commutator subgroup

7This module identifies the first closed-derived term with the closure of the abstract commutator

8subgroup and records closedness and finite-width consequences.

9-/

11open scoped Topology commutatorElement

13namespace ProCGroups.FiniteStepSolvableQuotients

15universe u

17/-- The topological closure of the abstract commutator subgroup. -/

18abbrev topologicalCommutator

19 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Subgroup G :=

20 (commutator G).topologicalClosure

22/--

23The topological commutator subgroup agrees with the closed commutator of the top subgroup with

24itself.

25-/

26@[simp] theorem topologicalCommutator_eq_closedCommutator_top_top

27 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :

28 topologicalCommutator G = closedCommutator (⊤ : Subgroup G) ⊤ := by

29 simp only [topologicalCommutator, commutator, closedCommutator]

31/-- The first top-derived subgroup is the topological commutator subgroup. -/

32@[simp] theorem topDerivedTop_one_eq_topologicalCommutator

33 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :

34 topDerivedTop G 1 = topologicalCommutator G := by

35 simp only [topDerivedTop, closedDerivedSeries, closedCommutator, topologicalCommutator,

36 commutator]

38/-- The first closed derived subgroup of the whole group is the closed commutator subgroup. -/

39theorem closedDerivedSeries_top_one_eq_closedCommutator

40 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :

41 closedDerivedSeries (G := G) (⊤ : Subgroup G) 1 =

42 Subgroup.closedCommutator G := by

43 calc

44 closedDerivedSeries (G := G) (⊤ : Subgroup G) 1 = topDerivedTop G 1 := rfl

45 _ = topologicalCommutator G := topDerivedTop_one_eq_topologicalCommutator G

46 _ = Subgroup.closedCommutator G := rfl

48/--

49When the ordinary commutator subgroup is closed, it agrees with the topological commutator

50subgroup.

51-/

52@[simp] theorem topologicalCommutator_eq_commutator_of_isClosed

53 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]

54 (hclosed : IsClosed ((commutator G : Subgroup G) : Set G)) :

55 topologicalCommutator G = commutator G := by

56 ext x

57 change x ∈ closure ((commutator G : Set G)) ↔ x ∈ (commutator G : Set G)

58 rw [closure_eq_iff_isClosed.mpr hclosed]

60/-- In a compact Hausdorff topological group, the set of individual commutators is closed. -/

61theorem isClosed_commutatorSet

62 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

63 [CompactSpace G] [T2Space G] :

64 IsClosed (commutatorSet G : Set G) := by

65 let f : G × G → G := fun p => ⁅p.1, p.2⁆

66 have hf : Continuous f := by

67 change Continuous (fun p : G × G => p.1 * p.2 * p.1⁻¹ * p.2⁻¹)

68 fun_prop

69 have himage : f '' (Set.univ : Set (G × G)) = commutatorSet G := by

70 ext z

71 constructor

72 · rintro ⟨p, -, rfl⟩

73 exact commutator_mem_commutatorSet (g₁ := p.1) (g₂ := p.2)

74 · intro hz

75 rcases mem_commutatorSet_iff.mp hz with ⟨x, y, rfl⟩

76 exact ⟨(x, y), by simp only [Set.mem_univ], rfl⟩

77 simpa [himage] using (isCompact_univ.image hf).isClosed

79/-- Every algebraic commutator lies in the topological commutator subgroup. -/

80theorem commutator_subset_topologicalCommutator

81 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :

82 commutator G ≤ topologicalCommutator G :=

83 Subgroup.le_topologicalClosure _

85/-- The topological commutator subgroup of a commutative group is trivial. -/

86@[simp] theorem topologicalCommutator_eq_bot_of_commGroup

87 (G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :

88 topologicalCommutator G = ⊥ := by

89 have hcomm : commutator G = ⊥ := by

90 rw [commutator_eq_bot_iff_center_eq_top, CommGroup.center_eq_top]

91 rw [topologicalCommutator, hcomm]

92 ext x

93 change x ∈ closure ({(1 : G)} : Set G) ↔ x ∈ (⊥ : Subgroup G)

94 rw [closure_singleton]

95 simp only [Set.mem_singleton_iff, Subgroup.mem_bot]

97/-- A commutative topological group has trivial positive closed derived stages. -/

98theorem topDerivedTop_eq_bot_of_commGroup

99 {G : Type u} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G]

100 {m : ℕ} (hm : 1 ≤ m) :

101 topDerivedTop G m = ⊥ := by

102 have h1 : topDerivedTop G 1 = (⊥ : Subgroup G) := by

103 rw [topDerivedTop_one_eq_topologicalCommutator]

104 exact topologicalCommutator_eq_bot_of_commGroup G

105 have hle : topDerivedTop G m ≤ topDerivedTop G 1 :=

106 (topDerivedTop_antitone (G := G)) hm

107 have hlebot : topDerivedTop G m ≤ (⊥ : Subgroup G) := by

108 rw [← h1]

109 exact hle

110 exact le_antisymm hlebot bot_le

111

112/-- A procyclic group has trivial positive closed derived stages. -/

113theorem topDerivedTop_eq_bot_of_procyclic

114 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]

115 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

116 (hG : ProCGroups.ProC.HasCyclicOpenNormalBasis G) {m : ℕ} (hm : 1 ≤ m) :

117 topDerivedTop G m = ⊥ := by

118 have hcomm : ∀ a b : G, a * b = b * a :=

119 ProCGroups.ProC.HasAbelianOpenNormalBasis.isAbelian (G := G)

120 (ProCGroups.ProC.HasCyclicOpenNormalBasis.hasAbelianOpenNormalBasis (G := G) hG)

121 let base : Group G := inferInstance

122 letI : CommGroup G := { base with mul_comm := hcomm }

123 exact topDerivedTop_eq_bot_of_commGroup hm

124

125/--

126Images of a topologically cyclic source in a discrete quotient of a maximal solvable quotient

127are algebraic powers of the image of the chosen generator.

128-/

129theorem maxSolvQuot_leftFactor_image_mem_zpowers

130 {Ω A B : Type u}

131 [TopologicalSpace Ω] [Group Ω] [IsTopologicalGroup Ω]

132 [TopologicalSpace A] [Group A] [IsTopologicalGroup A]

133 [TopologicalSpace B] [Group B] [IsTopologicalGroup B] [DiscreteTopology B]

134 {m : ℕ}

135 (q : MaxSolvQuot Ω m →* B) (hq : Continuous q)

136 (ιC : A →ₜ* Ω) {x a : A}

137 (hxgen : ProCGroups.Generation.TopologicallyGenerates (G := A) ({x} : Set A)) :

138 q (continuousToMaxSolvQuot Ω m (ιC a)) ∈

139 Subgroup.zpowers (q (continuousToMaxSolvQuot Ω m (ιC x))) := by

140 let f : A →* B := (q.comp (continuousToMaxSolvQuot Ω m : Ω →* MaxSolvQuot Ω m)).comp ιC

141 have hf : Continuous f := by

142 exact hq.comp ((continuousToMaxSolvQuot Ω m).continuous_toFun.comp ιC.continuous_toFun)

143 simpa [f] using

144 ProCGroups.Generation.monoidHom_map_mem_zpowers_of_topologicallyGenerates_singleton

145 (A := A) f hf hxgen (a := a)

146

147/-- \(G\) can be written as a product of at most \(n\) commutators. -/

148def IsProductOfCommutatorsLE

149 {G : Type u} [Group G] (n : ℕ) (g : G) : Prop :=

150 ∃ l : List (G × G), l.length ≤ n ∧ (l.map fun p => ⁅p.1, p.2⁆).prod = g

151

152/-- The identity element gives a product-of-commutators witness of width zero. -/

153theorem isProductOfCommutatorsLE_one

154 {G : Type u} [Group G] (n : ℕ) :

155 IsProductOfCommutatorsLE n (1 : G) := by

156 refine ⟨[], Nat.zero_le _, ?_⟩

157 simp only [List.map_nil, List.prod_nil]

158

159/-- A single commutator gives a product-of-commutators witness of width one. -/

160theorem isProductOfCommutatorsLE_commutatorElement

161 {G : Type u} [Group G] (x y : G) :

162 IsProductOfCommutatorsLE 1 ⁅x, y⁆ := by

163 refine ⟨[(x, y)], by simp only [List.length_cons, List.length_nil, zero_add, le_refl], ?_⟩

164 simp only [List.map_cons, List.map_nil, List.prod_cons, List.prod_nil, mul_one]

165

166/--

167Multiplying two bounded commutator-product witnesses gives a witness with the sum of the allowed

168widths.

169-/

170theorem IsProductOfCommutatorsLE.mul

171 {G : Type u} [Group G]

172 {m n : ℕ} {g h : G}

173 (hg : IsProductOfCommutatorsLE m g)

174 (hh : IsProductOfCommutatorsLE n h) :

175 IsProductOfCommutatorsLE (m + n) (g * h) := by

176 rcases hg with ⟨lg, hlg, rfl⟩

177 rcases hh with ⟨lh, hlh, rfl⟩

178 refine ⟨lg ++ lh, by simpa using Nat.add_le_add hlg hlh, ?_⟩

179 simp only [List.map_append, List.prod_append]

180

181/-- A product of at most \(m\) commutators is also a product of at most any larger bound \(n\). -/

182theorem IsProductOfCommutatorsLE.mono

183 {G : Type u} [Group G]

184 {m n : ℕ} {g : G}

185 (hg : IsProductOfCommutatorsLE m g)

186 (hmn : m ≤ n) :

187 IsProductOfCommutatorsLE n g := by

188 rcases hg with ⟨l, hl, hprod⟩

189 exact ⟨l, le_trans hl hmn, hprod⟩

190

191/-- A product of commutators lying in the given subgroup belongs to the commutator subgroup. -/

192theorem mem_commutator_of_isProductOfCommutatorsLE

193 {G : Type u} [Group G]

194 {n : ℕ} {g : G}

195 (hg : IsProductOfCommutatorsLE n g) :

196 g ∈ commutator G := by

197 rcases hg with ⟨l, -, rfl⟩

198 induction l with

199 | nil =>

200 simp only [commutator, List.map_nil, List.prod_nil, one_mem]

201 | cons a t ih =>

202 have ha : ⁅a.1, a.2⁆ ∈ commutator G := by

203 rw [commutator_eq_closure]

204 exact Subgroup.subset_closure (commutator_mem_commutatorSet (g₁ := a.1) (g₂ := a.2))

205 exact Subgroup.mul_mem _ ha ih

206

207end ProCGroups.FiniteStepSolvableQuotients