Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.KernelQuotient

1import Mathlib.GroupTheory.Complement

2import Mathlib.GroupTheory.GroupAction.ConjAct

3import Mathlib.GroupTheory.QuotientGroup.Basic

4import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.Script

6/-!

7# Reidemeister Schreier / Discrete / Presentations / Kernel Quotient

9This module identifies a presented free-group kernel with its relator

10quotient. It packages the canonical surjection, computes its kernel, and

11derives quotient equivalences for the conjugate and transversal relators.

12-/

14namespace ReidemeisterSchreier.Discrete.Presentations

16/-- The kernel of the map from the presented group is the image of the free-group lift kernel. -/

17theorem presentedGroup_toGroup_ker_eq_map_freeGroupLift_ker

18 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

19 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :

20 (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker =

21 Subgroup.map (PresentedGroup.mk rels) (FreeGroup.lift f).ker := by

22 exact QuotientGroup.ker_lift (Subgroup.normalClosure rels) (FreeGroup.lift f)

23 (PresentedGroup.to_group_eq_one_of_mem_closure hrels)

25/--

26The Reidemeister--Schreier map is determined on generators and respects the rewritten relator

27relations.

28-/

29def presentedFreeKernelToPresentedKernelHom

30 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

31 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :

32 (FreeGroup.lift f).ker →*

33 (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker where

34 toFun k :=

35 ⟨PresentedGroup.mk rels k, by

36 change FreeGroup.lift f (k : FreeGroup X) = 1

37 exact k.property⟩

38 map_one' := by

39 ext

40 simp only [OneMemClass.coe_one, map_one]

41 map_mul' k l := by

42 ext

43 simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]

45/-- Every element of the presented kernel lifts to an element of the free-group lift kernel. -/

46theorem presentedFreeKernelToPresentedKernelHom_surjective

47 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

48 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :

49 Function.Surjective (presentedFreeKernelToPresentedKernelHom hrels) := by

50 intro y

51 have hy :

52 (y : PresentedGroup rels) ∈

53 Subgroup.map (PresentedGroup.mk rels) (FreeGroup.lift f).ker := by

54 rw [← presentedGroup_toGroup_ker_eq_map_freeGroupLift_ker hrels]

55 exact y.property

56 rcases hy with ⟨x, hx, hxy⟩

57 refine ⟨⟨x, hx⟩, ?_⟩

58 ext

59 exact hxy

61/-- The kernel of the restricted map to the presented kernel is the pullback of the relator normal closure. -/

62theorem presentedFreeKernelToPresentedKernelHom_ker_eq_comap_normalClosure

63 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

64 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :

65 (presentedFreeKernelToPresentedKernelHom hrels).ker =

66 Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels) := by

67 ext k

68 constructor

69 · intro hk

70 rw [MonoidHom.mem_ker] at hk

71 have hkval := congrArg Subtype.val hk

72 change PresentedGroup.mk rels (k : FreeGroup X) = 1 at hkval

73 exact PresentedGroup.mk_eq_one_iff.mp hkval

74 · intro hk

75 rw [MonoidHom.mem_ker]

76 apply Subtype.ext

77 change PresentedGroup.mk rels (k : FreeGroup X) = 1

78 exact PresentedGroup.mk_eq_one_iff.mpr hk

80/-- Quotienting the free lift kernel by the pulled-back relator closure gives the presented kernel. -/

81noncomputable def presentedFreeKernelRelatorQuotientEquivPresentedKernel

82 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

83 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :

84 (FreeGroup.lift f).ker ⧸

85 Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels) ≃*

86 (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker :=

87 (QuotientGroup.quotientMulEquivOfEq

88 (presentedFreeKernelToPresentedKernelHom_ker_eq_comap_normalClosure hrels).symm).trans

89 (QuotientGroup.quotientKerEquivOfSurjective

90 (φ := presentedFreeKernelToPresentedKernelHom hrels)

91 (presentedFreeKernelToPresentedKernelHom_surjective hrels))

93/-- The relators in the free lift kernel obtained by conjugating defining relators by arbitrary words. -/

94def freeKernelConjugateRelatorSet

95 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A} :

96 Set (FreeGroup.lift f).ker :=

97 { z | ∃ g : FreeGroup X, ∃ r ∈ rels, (z : FreeGroup X) = g * r * g⁻¹ }

99/-- The conjugate relators obtained using only conjugating words from a chosen transversal. -/

100def freeKernelTransversalRelatorSet

101 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

102 (T : Set (FreeGroup X)) :

103 Set (FreeGroup.lift f).ker :=

104 { z | ∃ t ∈ T, ∃ r ∈ rels, (z : FreeGroup X) = t * r * t⁻¹ }

105

106/-- Every transversal conjugate relator is an unrestricted conjugate relator. -/

107theorem freeKernelTransversalRelatorSet_subset_conjugateRelatorSet

108 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

109 (T : Set (FreeGroup X)) :

110 freeKernelTransversalRelatorSet (f := f) (rels := rels) T ⊆

111 freeKernelConjugateRelatorSet (f := f) (rels := rels) := by

112 intro z hz

113 rcases hz with ⟨t, _ht, r, hr, hzval⟩

114 exact ⟨t, r, hr, hzval⟩

115

116/--

117The normal closure of the free-kernel transversal relator set equals the normal closure of the

118corresponding conjugate relator set.

119-/

120theorem freeKernelTransversalRelatorSet_normalClosure_eq_conjugateRelatorSet

121 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

122 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}

123 (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T) :

124 Subgroup.normalClosure (freeKernelTransversalRelatorSet (f := f) (rels := rels) T) =

125 Subgroup.normalClosure (freeKernelConjugateRelatorSet (f := f) (rels := rels)) := by

126 let L : Subgroup (FreeGroup X) := (FreeGroup.lift f).ker

127 let Sₜ : Set L := freeKernelTransversalRelatorSet (f := f) (rels := rels) T

128 let S : Set L := freeKernelConjugateRelatorSet (f := f) (rels := rels)

129 refine le_antisymm ?_ ?_

130 · exact Subgroup.normalClosure_le_normal

131 (fun z hz => Subgroup.subset_normalClosure

132 (freeKernelTransversalRelatorSet_subset_conjugateRelatorSet T hz))

133 · refine Subgroup.normalClosure_le_normal ?_

134 intro z hz

135 rcases hz with ⟨g, r, hr, hzval⟩

136 rcases (hT.existsUnique g).exists with ⟨kt, hkt⟩

137 let k : L := ⟨kt.1.1, kt.1.2⟩

138 let t : FreeGroup X := kt.2.1

139 have ht : t ∈ T := kt.2.2

140 have hg : (k : FreeGroup X) * t = g := hkt

141 have hwL : t * r * t⁻¹ ∈ L := by

142 change FreeGroup.lift f (t * r * t⁻¹) = 1

143 simp only [map_mul, hrels r hr, mul_one, map_inv, mul_inv_cancel]

144 let w : L := ⟨t * r * t⁻¹, hwL⟩

145 have hwSₜ : w ∈ Sₜ := by

146 refine ⟨t, ht, r, hr, ?_⟩

147 rfl

148 let N : Subgroup L := Subgroup.normalClosure Sₜ

149 have hwN : w ∈ N := Subgroup.subset_normalClosure hwSₜ

150 have hconj : k * w * k⁻¹ ∈ N := by

151 simpa [MulAut.conj_apply] using (Subgroup.normalClosure_normal.conj_mem w hwN k)

152 have hzconj : z = k * w * k⁻¹ := by

153 apply Subtype.ext

154 change (z : FreeGroup X) =

155 (k : FreeGroup X) * (w : FreeGroup X) * (k : FreeGroup X)⁻¹

156 rw [hzval, ← hg]

157 change ((k : FreeGroup X) * t) * r * ((k : FreeGroup X) * t)⁻¹ =

158 (k : FreeGroup X) * (t * r * t⁻¹) * (k : FreeGroup X)⁻¹

159 group

160 simpa [Sₜ, N, hzconj] using hconj

161

162/-- Every conjugate relator in the free lift kernel lies over the original relator normal closure. -/

163theorem freeKernelConjugateRelatorSet_subset_comap_normalClosure

164 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A} :

165 freeKernelConjugateRelatorSet (f := f) (rels := rels) ⊆

166 Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels) := by

167 intro z hz

168 rcases hz with ⟨g, r, hr, hz⟩

169 change (z : FreeGroup X) ∈ Subgroup.normalClosure rels

170 rw [hz]

171 exact Subgroup.conjugatesOfSet_subset_normalClosure

172 (Group.mem_conjugatesOfSet_iff.mpr ⟨r, hr, isConj_iff.2 ⟨g, rfl⟩⟩)

173

174/-- The normal closure of the conjugate relators is contained in the pulled-back relator closure. -/

175theorem freeKernelConjugateRelatorSet_normalClosure_le_comap_normalClosure

176 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A} :

177 Subgroup.normalClosure (freeKernelConjugateRelatorSet (f := f) (rels := rels)) ≤

178 Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels) := by

179 exact Subgroup.normalClosure_le_normal

180 (freeKernelConjugateRelatorSet_subset_comap_normalClosure (f := f) (rels := rels))

181

182/-- Arbitrary conjugate relators normally generate the pullback of the original relator closure. -/

183theorem freeKernelConjugateRelatorSet_normalClosure_eq_comap_normalClosure

184 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

185 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :

186 Subgroup.normalClosure (freeKernelConjugateRelatorSet (f := f) (rels := rels)) =

187 Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels) := by

188 let L : Subgroup (FreeGroup X) := (FreeGroup.lift f).ker

189 let S : Set L := freeKernelConjugateRelatorSet (f := f) (rels := rels)

190 let N : Subgroup L := Subgroup.normalClosure S

191 have hle :

192 N ≤ Subgroup.comap L.subtype (Subgroup.normalClosure rels) := by

193 simpa [L, S, N] using

194 freeKernelConjugateRelatorSet_normalClosure_le_comap_normalClosure (f := f) (rels := rels)

195 have hconj :

196 ∀ (g : FreeGroup X) (n : L), n ∈ N →

197 MulAut.conjNormal (H := L) g n ∈ N := by

198 intro g

199 let θ : MulAut L := MulAut.conjNormal (H := L) g

200 have hSmap : S ⊆ Subgroup.comap θ.toMonoidHom N := by

201 intro z hz

202 rcases hz with ⟨a, r, hr, hzval⟩

203 refine Subgroup.subset_normalClosure ?_

204 refine ⟨g * a, r, hr, ?_⟩

205 calc

206 ↑((MulEquiv.toMonoidHom θ) z) = g * (z : FreeGroup X) * g⁻¹ := by

207 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulAut.conjNormal_apply, θ]

208 _ = g * a * r * (g * a)⁻¹ := by

209 rw [hzval]

210 group

211 have hNmap : N ≤ Subgroup.comap θ.toMonoidHom N := by

212 simpa [N] using Subgroup.normalClosure_le_normal hSmap

213 exact fun n hn => hNmap hn

214 let H : Subgroup (FreeGroup X) := Subgroup.map L.subtype N

215 have hHnormal : H.Normal := by

216 refine ⟨?_⟩

217 intro x hx g

218 rcases hx with ⟨n, hn, rfl⟩

219 refine ⟨MulAut.conjNormal (H := L) g n, hconj g n hn, ?_⟩

220 exact MulAut.conjNormal_apply g n

221 have hrels_le_H : rels ⊆ H := by

222 intro r hr

223 have hrL : r ∈ L := by

224 exact MonoidHom.mem_ker.mpr (hrels r hr)

225 let z : L := ⟨r, hrL⟩

226 have hzS : z ∈ S := by

227 refine ⟨1, r, hr, ?_⟩

228 simp only [one_mul, inv_one, mul_one, z]

229 refine ⟨z, Subgroup.subset_normalClosure hzS, ?_⟩

230 rfl

231 have hnormalClosure_le_H : Subgroup.normalClosure rels ≤ H := by

232 exact Subgroup.normalClosure_le_normal hrels_le_H

233 refine le_antisymm hle ?_

234 intro k hk

235 have hkH : (k : FreeGroup X) ∈ H := hnormalClosure_le_H hk

236 rcases hkH with ⟨n, hn, hnval⟩

237 have hkn : k = n := Subtype.ext hnval.symm

238 simpa [hkn] using hn

239

240/-- Transversal conjugate relators normally generate the pullback of the original relator closure. -/

241theorem freeKernelTransversalRelatorSet_normalClosure_eq_comap_normalClosure

242 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

243 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}

244 (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T) :

245 Subgroup.normalClosure (freeKernelTransversalRelatorSet (f := f) (rels := rels) T) =

246 Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels) :=

247 (freeKernelTransversalRelatorSet_normalClosure_eq_conjugateRelatorSet hrels hT).trans

248 (freeKernelConjugateRelatorSet_normalClosure_eq_comap_normalClosure hrels)

249

250/-- The quotient of the free lift kernel by transversal relators is equivalent to the presented kernel. -/

251noncomputable def presentedFreeKernelTransversalRelatorQuotientEquivPresentedKernel

252 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

253 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}

254 (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T) :

255 (FreeGroup.lift f).ker ⧸

256 Subgroup.normalClosure (freeKernelTransversalRelatorSet (f := f) (rels := rels) T) ≃*

257 (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker :=

258 (QuotientGroup.quotientMulEquivOfEq

259 (freeKernelTransversalRelatorSet_normalClosure_eq_comap_normalClosure hrels hT)).trans

260 (presentedFreeKernelRelatorQuotientEquivPresentedKernel hrels)

261

262/-- Pulling transversal relators back to a free basis gives a relator quotient equivalent to the presented kernel. -/

263noncomputable def presentedFreeKernelSchreierRelatorQuotientEquivPresentedKernel

264 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

265 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}

266 (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T)

267 {Y : Type*} (e : FreeGroup Y ≃* (FreeGroup.lift f).ker) :

268 FreeGroup Y ⧸

269 Subgroup.normalClosure

270 (freeGroupPullbackRelatorSet e

271 (freeKernelTransversalRelatorSet (f := f) (rels := rels) T)) ≃*

272 (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker :=

273 (freeGroupPullbackRelatorQuotientEquiv e

274 (freeKernelTransversalRelatorSet (f := f) (rels := rels) T)).trans

275 (presentedFreeKernelTransversalRelatorQuotientEquivPresentedKernel hrels hT)

276

277/--

278Membership in the free-group pullback relator set is equivalent to the displayed relator

279condition.

280-/

281@[simp] theorem mem_freeGroupPullbackRelatorSet_iff

282 {Y G : Type*} [Group G] {e : FreeGroup Y ≃* G} {S : Set G} {y : FreeGroup Y} :

283 y ∈ freeGroupPullbackRelatorSet e S ↔ e y ∈ S := by

284 constructor

285 · rintro ⟨s, hs, hsy⟩

286 have hs_eq : s = e y := by

287 calc

288 s = e (e.symm s) := by simp only [MulEquiv.apply_symm_apply]

289 _ = e y := congrArg e hsy

290 simpa [hs_eq] using hs

291 · intro hy

292 exact ⟨e y, hy, by simp only [MulEquiv.symm_apply_apply]⟩

293

294/-- A conjugate of a defining relator by a transversal word belongs to the transversal relator set. -/

295theorem freeKernelTransversalRelatorSet_mem

296 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

297 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1)

298 {T : Set (FreeGroup X)} {t : FreeGroup X} (ht : t ∈ T)

299 {r : FreeGroup X} (hr : r ∈ rels) :

300 (⟨t * r * t⁻¹, by

301 change FreeGroup.lift f (t * r * t⁻¹) = 1

302 simp only [map_mul, hrels r hr, mul_one, map_inv, mul_inv_cancel]⟩ : (FreeGroup.lift f).ker) ∈

303 freeKernelTransversalRelatorSet (f := f) (rels := rels) T := by

304 exact ⟨t, ht, r, hr, rfl⟩

305

306/-- The inverse image of a relator belongs to its pullback relator set. -/

307theorem freeGroupPullbackRelator_mem

308 {Y G : Type*} [Group G] (e : FreeGroup Y ≃* G) {S : Set G} {s : G}

309 (hs : s ∈ S) :

310 e.symm s ∈ freeGroupPullbackRelatorSet e S := by

311 exact (mem_freeGroupPullbackRelatorSet_iff (e := e) (S := S) (y := e.symm s)).2

312 (by simpa using hs)

313

314/-- A pullback of an original relator lies in the normal closure of the pulled-back relator set. -/

315theorem freeGroupPullbackRelator_mem_normalClosure

316 {Y G : Type*} [Group G] (e : FreeGroup Y ≃* G) {S : Set G} {s : G}

317 (hs : s ∈ S) :

318 e.symm s ∈ Subgroup.normalClosure (freeGroupPullbackRelatorSet e S) :=

319 Subgroup.subset_normalClosure (freeGroupPullbackRelator_mem e hs)

320

321/--

322A pulled-back transversal relator lies in the normal closure of the pulled-back transversal

323relator set.

324-/

325theorem freeGroupPullback_transversalRelator_mem_normalClosure

326 {X A Y : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

327 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1)

328 {T : Set (FreeGroup X)} (e : FreeGroup Y ≃* (FreeGroup.lift f).ker)

329 {t : FreeGroup X} (ht : t ∈ T) {r : FreeGroup X} (hr : r ∈ rels) :

330 e.symm

331 (⟨t * r * t⁻¹, by

332 change FreeGroup.lift f (t * r * t⁻¹) = 1

333 simp only [map_mul, hrels r hr, mul_one, map_inv, mul_inv_cancel]⟩ : (FreeGroup.lift

334 f).ker) ∈

335 Subgroup.normalClosure

336 (freeGroupPullbackRelatorSet e

337 (freeKernelTransversalRelatorSet (f := f) (rels := rels) T)) :=

338 freeGroupPullbackRelator_mem_normalClosure e

339 (freeKernelTransversalRelatorSet_mem hrels ht hr)

340

341/--

342A kernel word whose image lies in the target normal closure lies in the normal closure of the

343transversal relators.

344-/

345theorem freeKernelElement_mem_transversalRelator_normalClosure_of_mem_normalClosure

346 {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

347 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}

348 (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T)

349 {k : (FreeGroup.lift f).ker}

350 (hk : (k : FreeGroup X) ∈ Subgroup.normalClosure rels) :

351 k ∈ Subgroup.normalClosure

352 (freeKernelTransversalRelatorSet (f := f) (rels := rels) T) := by

353 rw [freeKernelTransversalRelatorSet_normalClosure_eq_comap_normalClosure hrels hT]

354 exact hk

355

356/--

357A pulled-back free-group word lies in the source normal closure when its image lies in the

358target normal closure.

359-/

360theorem freeGroupPullback_mem_normalClosure_of_image_mem

361 {Y G : Type*} [Group G] (e : FreeGroup Y ≃* G) (S : Set G)

362 {y : FreeGroup Y} (hy : e y ∈ Subgroup.normalClosure S) :

363 y ∈ Subgroup.normalClosure (freeGroupPullbackRelatorSet e S) := by

364 have hyMap :

365 e y ∈

366 Subgroup.map e.toMonoidHom

367 (Subgroup.normalClosure (freeGroupPullbackRelatorSet e S)) := by

368 rw [map_normalClosure_freeGroupPullbackRelatorSet e S]

369 exact hy

370 rcases hyMap with ⟨z, hz, hzmap⟩

371 have hzy : z = y := e.injective hzmap

372 simpa [hzy] using hz

373

374/--

375A pulled-back transversal relator lies in the source normal closure whenever the original word

376lies in the target normal closure.

377-/

378theorem freeGroupPullback_transversalRelator_mem_normalClosure_of_mem_normalClosure

379 {X A Y : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}

380 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}

381 (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T)

382 (e : FreeGroup Y ≃* (FreeGroup.lift f).ker) {k : (FreeGroup.lift f).ker}

383 (hk : (k : FreeGroup X) ∈ Subgroup.normalClosure rels) :

384 e.symm k ∈

385 Subgroup.normalClosure

386 (freeGroupPullbackRelatorSet e

387 (freeKernelTransversalRelatorSet (f := f) (rels := rels) T)) := by

388 have hkSchreier :

389 k ∈ Subgroup.normalClosure

390 (freeKernelTransversalRelatorSet (f := f) (rels := rels) T) :=

391 freeKernelElement_mem_transversalRelator_normalClosure_of_mem_normalClosure hrels hT hk

392 apply freeGroupPullback_mem_normalClosure_of_image_mem e

393 (freeKernelTransversalRelatorSet (f := f) (rels := rels) T)

394 simpa using hkSchreier

395

396end ReidemeisterSchreier.Discrete.Presentations