Source: ProCGroups.GroupTheory.CentralizerNormalizerCommensurator

1import ProCGroups.Generation.Basic

3/-!

4# Pro C Groups / Group Theory / Centralizers

6Centralizer lemmas and closed-cyclic-subgroup results used by the profinite applications.

7-/

9open scoped Pointwise

11namespace ProCGroups.GroupTheory

13universe u

15variable {G : Type u} [Group G]

17/-- The centralizer of a set of elements. -/

18abbrev centralizer (S : Set G) : Subgroup G :=

19 Subgroup.centralizer S

21/-- The centralizer of a single element. -/

22abbrev centralizerOf (g : G) : Subgroup G :=

23 centralizer ({g} : Set G)

25/-- Membership in the centralizer is equivalent to the displayed commutation condition. -/

26@[simp] theorem mem_centralizer_iff {S : Set G} {g : G} :

27 g ∈ centralizer S ↔ ∀ h ∈ S, h * g = g * h :=

28 Iff.rfl

31/--

32Membership in the centralizer of a subset is equivalent to the displayed commutation condition.

33-/

34@[simp] theorem mem_centralizerOf_iff {x g : G} :

35 x ∈ centralizerOf g ↔ x * g = g * x := by

36 simpa [centralizerOf, centralizer] using

37 (Subgroup.mem_centralizer_singleton_iff (g := g) (k := x))

39/-- Centralizing an element implies centralizing each of its natural powers. -/

40theorem mem_centralizerOf_pow_of_mem {x y : G} (hy : y ∈ centralizerOf x) (n : ℕ) :

41 y ∈ centralizerOf (x ^ n) := by

42 rw [mem_centralizerOf_iff] at hy ⊢

43 induction n with

44 | zero =>

45 simp only [pow_zero, mul_one, one_mul]

46 | succ n ih =>

47 calc

48 y * x ^ (n + 1) = (y * x ^ n) * x := by rw [pow_succ, mul_assoc]

49 _ = (x ^ n * y) * x := by rw [ih]

50 _ = x ^ n * (y * x) := by rw [mul_assoc]

51 _ = x ^ n * (x * y) := by rw [hy]

52 _ = x ^ (n + 1) * y := by rw [pow_succ, mul_assoc]

54/--

55Membership of an inverse in the centralizer of a subset is equivalent to the displayed

56commutation condition.

57-/

58theorem mem_centralizerOf_inv_iff {x y : G} :

59 y ∈ centralizerOf x⁻¹ ↔ y ∈ centralizerOf x := by

60 rw [mem_centralizerOf_iff, mem_centralizerOf_iff]

61 constructor

62 · intro h

63 have h' := congrArg (fun z => x * z * x) h

64 simpa [mul_assoc] using h'.symm

65 · intro h

66 have h' := congrArg (fun z => x⁻¹ * z * x⁻¹) h

67 simpa [mul_assoc] using h'.symm

69/--

70Replacing a nonzero integer power by its positive absolute value does not change the

71centralizer.

72-/

73theorem centralizerOf_zpow_eq_natAbs (x : G) {n : ℤ} (_hn : n ≠ 0) :

74 centralizerOf (x ^ n) = centralizerOf (x ^ (n.natAbs : ℤ)) := by

75 cases n with

76 | ofNat k =>

77 simp only [Int.ofNat_eq_natCast, zpow_natCast, Int.natAbs_natCast]

78 | negSucc k =>

79 ext y

80 simp only [Int.natAbs, zpow_negSucc, zpow_natCast]

81 exact mem_centralizerOf_inv_iff

83/--

84Centralizing a nonzero integer power is equivalent, for membership purposes, to centralizing the

85corresponding positive absolute power.

86-/

87theorem mem_centralizerOf_zpow_natAbs_of_mem_zpow {x y : G} {n : ℤ} (hn : n ≠ 0)

88 (hy : y ∈ centralizerOf (x ^ n)) :

89 y ∈ centralizerOf (x ^ (n.natAbs : ℤ)) := by

90 rwa [← centralizerOf_zpow_eq_natAbs x hn]

93/-- If c and \(c * d\) centralize x, then d centralizes x. -/

94theorem right_factor_mem_centralizerOf_of_mul_mem_and_left_mem {x c d : G}

95 (hc : c ∈ centralizerOf x) (hcd : c * d ∈ centralizerOf x) :

96 d ∈ centralizerOf x := by

97 rw [mem_centralizerOf_iff] at hc hcd ⊢

98 calc

99 d * x = c⁻¹ * (c * d * x) := by simp [mul_assoc]

100 _ = c⁻¹ * (x * (c * d)) := by rw [hcd]

101 _ = c⁻¹ * ((x * c) * d) := by simp [mul_assoc]

102 _ = c⁻¹ * ((c * x) * d) := by rw [← hc]

103 _ = x * d := by simp [mul_assoc]

104

105

106/-- In a Hausdorff topological group, the centralizer of one element is closed. -/

107theorem centralizerOf_isClosed

108 [TopologicalSpace G] [ContinuousMul G] [T2Space G] (g : G) :

109 IsClosed ((centralizerOf g : Subgroup G) : Set G) := by

110 change IsClosed ({g} : Set G).centralizer

111 exact Set.isClosed_centralizer (M := G) ({g} : Set G)

112

113

114/-- Topological generation preserves containment in a closed centralizer. -/

115theorem closedSubgroupGenerated_le_centralizer_of_subset

116 [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]

117 {S T : Set G} (hS : S ⊆ (centralizer T : Set G)) :

118 (ProCGroups.Generation.closedSubgroupGenerated (G := G) S : Subgroup G) ≤ centralizer T := by

119 have hclosure : Subgroup.closure S ≤ centralizer T := by

120 rw [Subgroup.closure_le]

121 exact hS

122 exact

123 Subgroup.topologicalClosure_minimal

124 _

125 hclosure

126 (by

127 change IsClosed T.centralizer

128 exact Set.isClosed_centralizer (M := G) T)

129

130/-- A subgroup and its topological closure have the same centralizer. -/

131theorem centralizer_eq_centralizer_topologicalClosure

132 [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] (S : Subgroup G) :

133 centralizer ((S.topologicalClosure : Subgroup G) : Set G) = centralizer (S : Set G) := by

134 apply le_antisymm

135 · exact Subgroup.centralizer_le (G := G) (Subgroup.le_topologicalClosure (s := S))

136 · intro g hg

137 rw [mem_centralizer_iff] at hg ⊢

138 have hclosure : (S.topologicalClosure : Subgroup G) ≤ centralizerOf g := by

139 exact

140 Subgroup.topologicalClosure_minimal

141 S

142 (by

143 intro x hx

144 exact mem_centralizerOf_iff.mpr (hg x hx))

145 (centralizerOf_isClosed (G := G) g)

146 intro x hx

147 exact mem_centralizerOf_iff.mp (hclosure hx)

148

149/--

150The closed subgroup topologically generated by \(g\) centralizes every integer power of \(g\).

151-/

152theorem closedSubgroupGenerated_singleton_le_centralizerOf_zpow

153 [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]

154 (g : G) (n : ℤ) :

155 (ProCGroups.Generation.closedSubgroupGenerated (G := G) ({g} : Set G) : Subgroup G) ≤

156 centralizerOf (g ^ n) := by

157 have hclosure :

158 Subgroup.closure ({g} : Set G) ≤ centralizerOf (g ^ n) := by

159 rw [Subgroup.closure_le]

160 intro y hy

161 rw [Set.mem_singleton_iff] at hy

162 subst y

163 exact mem_centralizerOf_iff.mpr

164 (by simpa using (Commute.zpow_zpow_self g (1 : ℤ) n).eq)

165 exact

166 Subgroup.topologicalClosure_minimal

167 _

168 hclosure

169 (centralizerOf_isClosed (G := G) (g ^ n))

170

171/--

172Every element in the closed subgroup topologically generated by \(x\) centralizes each integer

173power of \(x\).

174-/

175theorem mem_centralizerOf_zpow_of_mem_closedSubgroupGenerated

176 [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]

177 {x c : G} (n : ℤ)

178 (hc : c ∈ (ProCGroups.Generation.closedSubgroupGenerated (G := G) ({x} : Set G) :

179 Subgroup G)) :

180 c ∈ centralizerOf (x ^ n) :=

181 (closedSubgroupGenerated_singleton_le_centralizerOf_zpow (G := G) x n) hc

182

183/--

184If a single element topologically generates the group, the centralizer of any of its powers is

185the corresponding closed cyclic subgroup.

186-/

187theorem centralizerOf_zpow_eq_closedSubgroupGenerated_of_topologicallyGenerates

188 [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]

189 (x : G) (n : ℤ)

190 (hgen : ProCGroups.Generation.TopologicallyGenerates (G := G) ({x} : Set G)) :

191 centralizerOf (x ^ n) =

192 (ProCGroups.Generation.closedSubgroupGenerated (G := G) ({x} : Set G) : Subgroup G) := by

193 have hcyc :

194 (ProCGroups.Generation.closedSubgroupGenerated (G := G) ({x} : Set G) : Subgroup G) =

195 ⊤ := by

196 unfold ProCGroups.Generation.TopologicallyGenerates at hgen

197 simpa [ProCGroups.Generation.closedSubgroupGenerated] using hgen

198 have hcent_top : centralizerOf (x ^ n) = ⊤ := by

199 apply top_unique

200 rw [← hcyc]

201 exact closedSubgroupGenerated_singleton_le_centralizerOf_zpow (G := G) x n

202 simpa [hcyc] using hcent_top

203

204end ProCGroups.GroupTheory