ReidemeisterSchreier/Discrete/Presentations/Tietze/Core.lean

1import Mathlib.GroupTheory.PresentedGroup

2import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorMap

4/-

5PUBLIC_PAGE_SNAPSHOT

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

7lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations/Tietze/Core.lean

8translation_root: data/translation

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

10placement: after imports, never before imports

11-/

12/-!

13# Tietze transformations

15Presentation-level Tietze moves for adding and deleting generators, replacing relators, comparing quotient presentations, and recording executable Tietze scripts.

16-/

18universe u v w

20namespace ReidemeisterSchreier.Discrete.Presentations

22variable {G H K : Type*} [Group G] [Group H] [Group K]

24/-- A reusable Tietze certificate between two presentations. This is the

25scriptable layer: certificates can be reversed and composed while retaining the

26underlying normal-closure data. -/

27structure TietzeEquiv

28 {X Y : Type*} (R : Set (FreeGroup X)) (S : Set (FreeGroup Y)) where

29 toMutualMapData : RelatorQuotientMutualMapData R S

31namespace TietzeEquiv

33variable {X Y Z : Type*}

34variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}

35variable {T : Set (FreeGroup Z)}

37def refl (R : Set (FreeGroup X)) : TietzeEquiv R R where

38 toMutualMapData := RelatorQuotientMutualMapData.refl R

40def symm (D : TietzeEquiv R S) : TietzeEquiv S R where

41 toMutualMapData := D.toMutualMapData.symm

43def trans (D₁ : TietzeEquiv R S) (D₂ : TietzeEquiv S T) :

44 TietzeEquiv R T where

45 toMutualMapData := D₁.toMutualMapData.trans D₂.toMutualMapData

47def ofMutualMapData (D : RelatorQuotientMutualMapData R S) :

48 TietzeEquiv R S where

49 toMutualMapData := D

51def ofRelatorEquivalent

52 {R S : Set (FreeGroup X)}

53 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)

54 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :

55 TietzeEquiv R S where

56 toMutualMapData :=

57 relatorQuotientMutualMapDataOfRelatorEquivalent hR_to_S hS_to_R

59def ofNormalClosureEq

60 {R S : Set (FreeGroup X)}

61 (h : Subgroup.normalClosure R = Subgroup.normalClosure S) :

62 TietzeEquiv R S where

63 toMutualMapData := relatorQuotientMutualMapDataOfNormalClosureEq h

65def ofGeneratorMaps

66 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}

67 (toGenerator : X → FreeGroup Y)

68 (invGenerator : Y → FreeGroup X)

69 (hR :

70 ∀ r ∈ R,

71 FreeGroup.lift toGenerator r ∈ Subgroup.normalClosure S)

72 (hS :

73 ∀ s ∈ S,

74 FreeGroup.lift invGenerator s ∈ Subgroup.normalClosure R)

75 (hinv_to :

76 ∀ x : X,

77 RelatorEquivalent R

78 (FreeGroup.lift invGenerator (toGenerator x))

79 (FreeGroup.of x))

80 (hto_inv :

81 ∀ y : Y,

82 RelatorEquivalent S

83 (FreeGroup.lift toGenerator (invGenerator y))

84 (FreeGroup.of y)) :

85 TietzeEquiv R S :=

86 TietzeEquiv.ofMutualMapData

87 (relatorQuotientMutualMapDataOfGeneratorMaps

88 toGenerator invGenerator hR hS hinv_to hto_inv)

90def ofGeneratorMapsRelatorEquivalent

91 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}

92 (toGenerator : X → FreeGroup Y)

93 (invGenerator : Y → FreeGroup X)

94 (hR :

95 ∀ r ∈ R,

96 RelatorEquivalent S (FreeGroup.lift toGenerator r) 1)

97 (hS :

98 ∀ s ∈ S,

99 RelatorEquivalent R (FreeGroup.lift invGenerator s) 1)

100 (hinv_to :

101 ∀ x : X,

102 RelatorEquivalent R

103 (FreeGroup.lift invGenerator (toGenerator x))

104 (FreeGroup.of x))

105 (hto_inv :

106 ∀ y : Y,

107 RelatorEquivalent S

108 (FreeGroup.lift toGenerator (invGenerator y))

109 (FreeGroup.of y)) :

110 TietzeEquiv R S :=

111 TietzeEquiv.ofMutualMapData

112 (relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent

113 toGenerator invGenerator hR hS hinv_to hto_inv)

114

115/-- Tietze certificate from generator maps when both relator sets are indexed

116unions. Use this when a presentation has named relator families and each

117family has its own calculation. -/

118def ofGeneratorMapsRelatorEquivalent_iUnion

119 {ι κ : Sort*}

120 {R : ι → Set (FreeGroup X)} {S : κ → Set (FreeGroup Y)}

121 (toGenerator : X → FreeGroup Y)

122 (invGenerator : Y → FreeGroup X)

123 (hR :

124 ∀ i : ι, ∀ r ∈ R i,

125 RelatorEquivalent (Set.iUnion S) (FreeGroup.lift toGenerator r) 1)

126 (hS :

127 ∀ k : κ, ∀ s ∈ S k,

128 RelatorEquivalent (Set.iUnion R) (FreeGroup.lift invGenerator s) 1)

129 (hinv_to :

130 ∀ x : X,

131 RelatorEquivalent (Set.iUnion R)

132 (FreeGroup.lift invGenerator (toGenerator x))

133 (FreeGroup.of x))

134 (hto_inv :

135 ∀ y : Y,

136 RelatorEquivalent (Set.iUnion S)

137 (FreeGroup.lift toGenerator (invGenerator y))

138 (FreeGroup.of y)) :

139 TietzeEquiv (Set.iUnion R) (Set.iUnion S) :=

140 TietzeEquiv.ofMutualMapData

141 (relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion

142 toGenerator invGenerator hR hS hinv_to hto_inv)

143

144/-- Two-level family variant of `ofGeneratorMapsRelatorEquivalent_iUnion`. -/

145def ofGeneratorMapsRelatorEquivalent_iUnion₂

146 {ι κ : Sort*} {α : ι → Sort*} {β : κ → Sort*}

147 {R : ∀ i : ι, α i → Set (FreeGroup X)}

148 {S : ∀ k : κ, β k → Set (FreeGroup Y)}

149 (toGenerator : X → FreeGroup Y)

150 (invGenerator : Y → FreeGroup X)

151 (hR :

152 ∀ i : ι, ∀ a : α i, ∀ r ∈ R i a,

153 RelatorEquivalent

154 (Set.iUnion fun k : κ => Set.iUnion (S k))

155 (FreeGroup.lift toGenerator r) 1)

156 (hS :

157 ∀ k : κ, ∀ b : β k, ∀ s ∈ S k b,

158 RelatorEquivalent

159 (Set.iUnion fun i : ι => Set.iUnion (R i))

160 (FreeGroup.lift invGenerator s) 1)

161 (hinv_to :

162 ∀ x : X,

163 RelatorEquivalent

164 (Set.iUnion fun i : ι => Set.iUnion (R i))

165 (FreeGroup.lift invGenerator (toGenerator x))

166 (FreeGroup.of x))

167 (hto_inv :

168 ∀ y : Y,

169 RelatorEquivalent

170 (Set.iUnion fun k : κ => Set.iUnion (S k))

171 (FreeGroup.lift toGenerator (invGenerator y))

172 (FreeGroup.of y)) :

173 TietzeEquiv

174 (Set.iUnion fun i : ι => Set.iUnion (R i))

175 (Set.iUnion fun k : κ => Set.iUnion (S k)) :=

176 TietzeEquiv.ofMutualMapData

177 (relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion₂

178 toGenerator invGenerator hR hS hinv_to hto_inv)

179

180noncomputable def quotientEquiv (D : TietzeEquiv R S) :

181 FreeGroup X ⧸ Subgroup.normalClosure R ≃*

182 FreeGroup Y ⧸ Subgroup.normalClosure S :=

183 quotientEquivOfRelatorQuotientMutualMapData R S D.toMutualMapData

184

185noncomputable def presentedEquiv (D : TietzeEquiv R S) :

186 PresentedGroup R ≃* PresentedGroup S :=

187 quotientEquivOfRelatorQuotientMutualMapData R S D.toMutualMapData

188

189end TietzeEquiv

190

191def freeGroupPullbackRelatorTietzeEquiv

192 {X Y : Type*} (e : FreeGroup X ≃* FreeGroup Y)

193 (S : Set (FreeGroup Y)) :

194 TietzeEquiv (freeGroupPullbackRelatorSet e S) S :=

195 TietzeEquiv.ofMutualMapData

196 (relatorQuotientMutualMapDataOfNormalClosureMapEq

197 (freeGroupPullbackRelatorSet e S) S e

198 (map_normalClosure_freeGroupPullbackRelatorSet e S))

199

200/-- A presentation packaged with its generator type. This is a light wrapper

201for writing long Tietze scripts whose intermediate presentations may have

202different generator types. -/

203structure Presentation where

204 Generator : Type u

205 relators : Set (FreeGroup Generator)

206

207namespace Presentation

208

209def ofRelators {X : Type u} (R : Set (FreeGroup X)) : Presentation.{u} where

210 Generator := X

211 relators := R

212

213end Presentation

214

215/-- A scriptable Tietze certificate between packaged presentations. The data is

216still exactly a `TietzeEquiv`; this wrapper only remembers the intermediate

217presentation objects so long chains can be composed without unpacking generator

218types by hand. -/

219structure TietzeScript (P : Presentation.{u}) (Q : Presentation.{v}) where

220 toTietzeEquiv : TietzeEquiv P.relators Q.relators

221

222namespace TietzeScript

223

224def ofTietzeEquiv {P : Presentation.{u}} {Q : Presentation.{v}}

225 (D : TietzeEquiv P.relators Q.relators) :

226 TietzeScript P Q where

227 toTietzeEquiv := D

228

229def ofMutualMapData {P : Presentation.{u}} {Q : Presentation.{v}}

230 (D : RelatorQuotientMutualMapData P.relators Q.relators) :

231 TietzeScript P Q :=

232 ofTietzeEquiv (TietzeEquiv.ofMutualMapData D)

233

234def refl (P : Presentation.{u}) : TietzeScript P P :=

235 ofTietzeEquiv (TietzeEquiv.refl P.relators)

236

237def symm {P : Presentation.{u}} {Q : Presentation.{v}}

238 (D : TietzeScript P Q) :

239 TietzeScript Q P :=

240 ofTietzeEquiv D.toTietzeEquiv.symm

241

242def trans {P : Presentation.{u}} {Q : Presentation.{v}}

243 {U : Presentation.{w}}

244 (D₁ : TietzeScript P Q) (D₂ : TietzeScript Q U) :

245 TietzeScript P U :=

246 ofTietzeEquiv (D₁.toTietzeEquiv.trans D₂.toTietzeEquiv)

247

248noncomputable def presentedEquiv

249 {P : Presentation.{u}} {Q : Presentation.{v}}

250 (D : TietzeScript P Q) :

251 PresentedGroup P.relators ≃* PresentedGroup Q.relators :=

252 D.toTietzeEquiv.presentedEquiv

253

254noncomputable def quotientEquiv

255 {P : Presentation.{u}} {Q : Presentation.{v}}

256 (D : TietzeScript P Q) :

257 FreeGroup P.Generator ⧸ Subgroup.normalClosure P.relators ≃*

258 FreeGroup Q.Generator ⧸ Subgroup.normalClosure Q.relators :=

259 D.toTietzeEquiv.quotientEquiv

260

261end TietzeScript

262

263namespace TietzeEquiv

264

265def toScript

266 {X Y : Type*} {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}

267 (D : TietzeEquiv R S) :

268 TietzeScript (Presentation.ofRelators R) (Presentation.ofRelators S) :=

269 TietzeScript.ofTietzeEquiv D

270

271end TietzeEquiv

272

273end ReidemeisterSchreier.Discrete.Presentations