ReidemeisterSchreier/Discrete/Presentations/KernelQuotient.lean

1import ReidemeisterSchreier.Discrete.Presentations.Tietze.Script

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations/KernelQuotient.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

10-/

11/-!

12# Discrete group presentations

14Kernel-quotient presentations, relator normal closures, and presentation equivalences used by Reidemeister-Schreier rewriting.

15-/

17namespace ReidemeisterSchreier.Discrete.Presentations

19open scoped BigOperators

21theorem presentedGroup_toGroup_ker_eq_map_freeGroupLift_ker

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

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

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

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

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

27 (PresentedGroup.to_group_eq_one_of_mem_closure hrels)

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]

45theorem presentedFreeKernelToPresentedKernelHom_surjective

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

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

48 Function.Surjective (presentedFreeKernelToPresentedKernelHom hrels) := by

49 intro y

50 have hy :

51 (y : PresentedGroup rels) ∈

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

53 rw [← presentedGroup_toGroup_ker_eq_map_freeGroupLift_ker hrels]

54 exact y.property

55 rcases hy with ⟨x, hx, hxy⟩

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

57 ext

58 exact hxy

60theorem presentedFreeKernelToPresentedKernelHom_ker_eq_comap_normalClosure

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

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

63 (presentedFreeKernelToPresentedKernelHom hrels).ker =

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

65 ext k

66 constructor

67 · intro hk

68 rw [MonoidHom.mem_ker] at hk

69 have hkval := congrArg Subtype.val hk

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

71 exact PresentedGroup.mk_eq_one_iff.mp hkval

72 · intro hk

73 rw [MonoidHom.mem_ker]

74 apply Subtype.ext

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

76 exact PresentedGroup.mk_eq_one_iff.mpr hk

78noncomputable def presentedFreeKernelRelatorQuotientEquivPresentedKernel

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

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

81 (FreeGroup.lift f).ker ⧸

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

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

84 (QuotientGroup.quotientMulEquivOfEq

85 (presentedFreeKernelToPresentedKernelHom_ker_eq_comap_normalClosure hrels).symm).trans

86 (QuotientGroup.quotientKerEquivOfSurjective

87 (φ := presentedFreeKernelToPresentedKernelHom hrels)

88 (presentedFreeKernelToPresentedKernelHom_surjective hrels))

90def freeKernelConjugateRelatorSet

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

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

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

95def freeKernelTransversalRelatorSet

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

97 (T : Set (FreeGroup X)) :

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

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

100

101theorem freeKernelTransversalRelatorSet_subset_conjugateRelatorSet

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

103 (T : Set (FreeGroup X)) :

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

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

106 intro z hz

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

108 exact ⟨t, r, hr, hzval⟩

109

110theorem freeKernelTransversalRelatorSet_normalClosure_eq_conjugateRelatorSet

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

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

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

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

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

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

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

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

119 refine le_antisymm ?_ ?_

120 · exact Subgroup.normalClosure_le_normal

121 (fun z hz => Subgroup.subset_normalClosure

122 (freeKernelTransversalRelatorSet_subset_conjugateRelatorSet T hz))

123 · refine Subgroup.normalClosure_le_normal ?_

124 intro z hz

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

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

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

128 let t : FreeGroup X := kt.2.1

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

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

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

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

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

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

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

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

137 rfl

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

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

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

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

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

143 apply Subtype.ext

144 change (z : FreeGroup X) =

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

146 rw [hzval, ← hg]

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

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

149 group

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

151

152theorem freeKernelConjugateRelatorSet_subset_comap_normalClosure

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

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

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

156 intro z hz

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

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

159 rw [hz]

160 exact Subgroup.conjugatesOfSet_subset_normalClosure

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

162

163theorem freeKernelConjugateRelatorSet_normalClosure_le_comap_normalClosure

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

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

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

167 exact Subgroup.normalClosure_le_normal

168 (freeKernelConjugateRelatorSet_subset_comap_normalClosure (f := f) (rels := rels))

169

170theorem freeKernelConjugateRelatorSet_normalClosure_eq_comap_normalClosure

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

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

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

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

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

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

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

178 have hle :

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

180 simpa [L, S, N] using

181 freeKernelConjugateRelatorSet_normalClosure_le_comap_normalClosure (f := f) (rels := rels)

182 have hconj :

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

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

185 intro g

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

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

188 intro z hz

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

190 refine Subgroup.subset_normalClosure ?_

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

192 calc

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

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

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

196 rw [hzval]

197 group

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

199 simpa [N] using Subgroup.normalClosure_le_normal hSmap

200 exact fun n hn => hNmap hn

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

202 have hHnormal : H.Normal := by

203 refine ⟨?_⟩

204 intro x hx g

205 rcases hx with ⟨n, hn, rfl⟩

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

207 exact MulAut.conjNormal_apply g n

208 have hrels_le_H : rels ⊆ H := by

209 intro r hr

210 have hrL : r ∈ L := by

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

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

213 have hzS : z ∈ S := by

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

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

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

217 rfl

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

219 exact Subgroup.normalClosure_le_normal hrels_le_H

220 refine le_antisymm hle ?_

221 intro k hk

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

223 rcases hkH with ⟨n, hn, hnval⟩

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

225 simpa [hkn] using hn

226

227theorem freeKernelTransversalRelatorSet_normalClosure_eq_comap_normalClosure

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

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

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

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

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

233 (freeKernelTransversalRelatorSet_normalClosure_eq_conjugateRelatorSet hrels hT).trans

234 (freeKernelConjugateRelatorSet_normalClosure_eq_comap_normalClosure hrels)

235

236noncomputable def presentedFreeKernelTransversalRelatorQuotientEquivPresentedKernel

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

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

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

240 (FreeGroup.lift f).ker ⧸

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

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

243 (QuotientGroup.quotientMulEquivOfEq

244 (freeKernelTransversalRelatorSet_normalClosure_eq_comap_normalClosure hrels hT)).trans

245 (presentedFreeKernelRelatorQuotientEquivPresentedKernel hrels)

246

247noncomputable def presentedFreeKernelSchreierRelatorQuotientEquivPresentedKernel

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

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

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

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

252 FreeGroup Y ⧸

253 Subgroup.normalClosure

254 (freeGroupPullbackRelatorSet e

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

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

257 (freeGroupPullbackRelatorQuotientEquiv e

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

259 (presentedFreeKernelTransversalRelatorQuotientEquivPresentedKernel hrels hT)

260

261@[simp] theorem mem_freeGroupPullbackRelatorSet_iff

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

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

264 constructor

265 · rintro ⟨s, hs, hsy⟩

266 have hs_eq : s = e y := by

267 calc

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

269 _ = e y := congrArg e hsy

270 simpa [hs_eq] using hs

271 · intro hy

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

273

274theorem freeKernelTransversalRelatorSet_mem

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

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

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

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

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

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

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

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

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

284

285theorem freeGroupPullbackRelator_mem

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

287 (hs : s ∈ S) :

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

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

290 (by simpa using hs)

291

292theorem freeGroupPullbackRelator_mem_normalClosure

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

294 (hs : s ∈ S) :

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

296 Subgroup.subset_normalClosure (freeGroupPullbackRelator_mem e hs)

297

298theorem freeGroupPullback_transversalRelator_mem_normalClosure

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

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

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

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

303 e.symm

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

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

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

307 Subgroup.normalClosure

308 (freeGroupPullbackRelatorSet e

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

310 freeGroupPullbackRelator_mem_normalClosure e

311 (freeKernelTransversalRelatorSet_mem hrels ht hr)

312

313theorem freeKernelElement_mem_transversalRelator_normalClosure_of_mem_normalClosure

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

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

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

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

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

319 k ∈ Subgroup.normalClosure

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

321 rw [freeKernelTransversalRelatorSet_normalClosure_eq_comap_normalClosure hrels hT]

322 exact hk

323

324theorem freeGroupPullback_mem_normalClosure_of_image_mem

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

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

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

328 have hyMap :

329 e y ∈

330 Subgroup.map e.toMonoidHom

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

332 rw [map_normalClosure_freeGroupPullbackRelatorSet e S]

333 exact hy

334 rcases hyMap with ⟨z, hz, hzmap⟩

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

336 simpa [hzy] using hz

337

338theorem freeGroupPullback_transversalRelator_mem_normalClosure_of_mem_normalClosure

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

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

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

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

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

344 e.symm k ∈

345 Subgroup.normalClosure

346 (freeGroupPullbackRelatorSet e

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

348 have hkSchreier :

349 k ∈ Subgroup.normalClosure

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

351 freeKernelElement_mem_transversalRelator_normalClosure_of_mem_normalClosure hrels hT hk

352 apply freeGroupPullback_mem_normalClosure_of_image_mem e

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

354 simpa using hkSchreier

355

356end ReidemeisterSchreier.Discrete.Presentations