Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.Core
1import Mathlib.GroupTheory.PresentedGroup
2import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorMap
4/-!
5# Semantic equivalence of presentations
7This module packages the algebraic content of a Tietze equivalence: mutually
8inverse maps between groups presented by relators. `Presentation` remembers
9the generator type, while `PresentationEquivCertificate` composes and reverses
10the resulting semantic certificates.
12Concrete, inspectable move sequences are defined separately in
13`Tietze.Script`.
14-/
16universe u v w
18namespace ReidemeisterSchreier.Discrete.Presentations
20variable {G H K : Type*} [Group G] [Group H] [Group K]
22/-- A reusable semantic Tietze certificate between two relator presentations. -/
23structure TietzeEquiv
24 {X Y : Type*} (R : Set (FreeGroup X)) (S : Set (FreeGroup Y)) where
25 /-- Mutually inverse maps between the two free groups, modulo their relator normal closures. -/
26 toMutualMapData : RelatorQuotientMutualMapData R S
28namespace TietzeEquiv
30variable {X Y Z : Type*}
31variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
32variable {T : Set (FreeGroup Z)}
34/-- The identity mutual map gives a reflexive Tietze equivalence. -/
35def refl (R : Set (FreeGroup X)) : TietzeEquiv R R where
36 toMutualMapData := RelatorQuotientMutualMapData.refl R
38/-- Reversing the mutual maps gives the symmetric Tietze equivalence. -/
39def symm (D : TietzeEquiv R S) : TietzeEquiv S R where
40 toMutualMapData := D.toMutualMapData.symm
42/-- Composing mutual maps gives the transitive composite of Tietze equivalences. -/
43def trans (D₁ : TietzeEquiv R S) (D₂ : TietzeEquiv S T) :
44 TietzeEquiv R T where
45 toMutualMapData := D₁.toMutualMapData.trans D₂.toMutualMapData
47/-- Mutual relator-quotient map data define a Tietze equivalence. -/
48def ofMutualMapData (D : RelatorQuotientMutualMapData R S) :
49 TietzeEquiv R S where
50 toMutualMapData := D
52/--
53A Tietze equivalence is induced by a relator-equivalence comparison between the two relator
54sets.
55-/
56def ofRelatorEquivalent
57 {R S : Set (FreeGroup X)}
58 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
59 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
60 TietzeEquiv R S where
61 toMutualMapData :=
62 relatorQuotientMutualMapDataOfRelatorEquivalent hR_to_S hS_to_R
64/-- Equal normal closures give a Tietze equivalence between the two relator sets. -/
65def ofNormalClosureEq
66 {R S : Set (FreeGroup X)}
67 (h : Subgroup.normalClosure R = Subgroup.normalClosure S) :
68 TietzeEquiv R S where
69 toMutualMapData := relatorQuotientMutualMapDataOfNormalClosureEq h
71/--
72Compatible generator maps in both directions define a Tietze equivalence between the two relator
73quotients.
74-/
75def ofGeneratorMaps
76 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
77 (toGenerator : X → FreeGroup Y)
78 (invGenerator : Y → FreeGroup X)
79 (hR :
80 ∀ r ∈ R,
81 FreeGroup.lift toGenerator r ∈ Subgroup.normalClosure S)
82 (hS :
83 ∀ s ∈ S,
84 FreeGroup.lift invGenerator s ∈ Subgroup.normalClosure R)
85 (hinv_to :
86 ∀ x : X,
87 RelatorEquivalent R
88 (FreeGroup.lift invGenerator (toGenerator x))
89 (FreeGroup.of x))
90 (hto_inv :
91 ∀ y : Y,
92 RelatorEquivalent S
93 (FreeGroup.lift toGenerator (invGenerator y))
94 (FreeGroup.of y)) :
95 TietzeEquiv R S :=
96 TietzeEquiv.ofMutualMapData
97 (relatorQuotientMutualMapDataOfGeneratorMaps
98 toGenerator invGenerator hR hS hinv_to hto_inv)
100/--
101Generator maps that preserve relators up to relator equivalence induce the corresponding
102presented-group map.
103-/
104def ofGeneratorMapsRelatorEquivalent
105 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
106 (toGenerator : X → FreeGroup Y)
107 (invGenerator : Y → FreeGroup X)
108 (hR :
109 ∀ r ∈ R,
110 RelatorEquivalent S (FreeGroup.lift toGenerator r) 1)
111 (hS :
112 ∀ s ∈ S,
113 RelatorEquivalent R (FreeGroup.lift invGenerator s) 1)
114 (hinv_to :
115 ∀ x : X,
116 RelatorEquivalent R
117 (FreeGroup.lift invGenerator (toGenerator x))
118 (FreeGroup.of x))
119 (hto_inv :
120 ∀ y : Y,
121 RelatorEquivalent S
122 (FreeGroup.lift toGenerator (invGenerator y))
123 (FreeGroup.of y)) :
124 TietzeEquiv R S :=
125 TietzeEquiv.ofMutualMapData
126 (relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent
127 toGenerator invGenerator hR hS hinv_to hto_inv)
129/--
130A Tietze certificate from generator maps when both relator sets are indexed unions of named
131relator families.
132-/
133def ofGeneratorMapsRelatorEquivalent_iUnion
134 {ι κ : Sort*}
135 {R : ι → Set (FreeGroup X)} {S : κ → Set (FreeGroup Y)}
136 (toGenerator : X → FreeGroup Y)
137 (invGenerator : Y → FreeGroup X)
138 (hR :
139 ∀ i : ι, ∀ r ∈ R i,
140 RelatorEquivalent (Set.iUnion S) (FreeGroup.lift toGenerator r) 1)
141 (hS :
142 ∀ k : κ, ∀ s ∈ S k,
143 RelatorEquivalent (Set.iUnion R) (FreeGroup.lift invGenerator s) 1)
144 (hinv_to :
145 ∀ x : X,
146 RelatorEquivalent (Set.iUnion R)
147 (FreeGroup.lift invGenerator (toGenerator x))
148 (FreeGroup.of x))
149 (hto_inv :
150 ∀ y : Y,
151 RelatorEquivalent (Set.iUnion S)
152 (FreeGroup.lift toGenerator (invGenerator y))
153 (FreeGroup.of y)) :
154 TietzeEquiv (Set.iUnion R) (Set.iUnion S) :=
155 TietzeEquiv.ofMutualMapData
156 (relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion
157 toGenerator invGenerator hR hS hinv_to hto_inv)
159/--
160A Tietze equivalence is obtained from generator maps whose doubly indexed source relators map to
161relator-equivalent target relators.
162-/
163def ofGeneratorMapsRelatorEquivalent_iUnion₂
164 {ι κ : Sort*} {α : ι → Sort*} {β : κ → Sort*}
165 {R : ∀ i : ι, α i → Set (FreeGroup X)}
166 {S : ∀ k : κ, β k → Set (FreeGroup Y)}
167 (toGenerator : X → FreeGroup Y)
168 (invGenerator : Y → FreeGroup X)
169 (hR :
170 ∀ i : ι, ∀ a : α i, ∀ r ∈ R i a,
171 RelatorEquivalent
172 (Set.iUnion fun k : κ => Set.iUnion (S k))
173 (FreeGroup.lift toGenerator r) 1)
174 (hS :
175 ∀ k : κ, ∀ b : β k, ∀ s ∈ S k b,
176 RelatorEquivalent
177 (Set.iUnion fun i : ι => Set.iUnion (R i))
178 (FreeGroup.lift invGenerator s) 1)
179 (hinv_to :
180 ∀ x : X,
181 RelatorEquivalent
182 (Set.iUnion fun i : ι => Set.iUnion (R i))
183 (FreeGroup.lift invGenerator (toGenerator x))
184 (FreeGroup.of x))
185 (hto_inv :
186 ∀ y : Y,
187 RelatorEquivalent
188 (Set.iUnion fun k : κ => Set.iUnion (S k))
189 (FreeGroup.lift toGenerator (invGenerator y))
190 (FreeGroup.of y)) :
191 TietzeEquiv
192 (Set.iUnion fun i : ι => Set.iUnion (R i))
193 (Set.iUnion fun k : κ => Set.iUnion (S k)) :=
194 TietzeEquiv.ofMutualMapData
195 (relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion₂
196 toGenerator invGenerator hR hS hinv_to hto_inv)
198/-- A Tietze equivalence induces an isomorphism of the corresponding relator quotients. -/
199noncomputable def quotientEquiv (D : TietzeEquiv R S) :
200 FreeGroup X ⧸ Subgroup.normalClosure R ≃*
201 FreeGroup Y ⧸ Subgroup.normalClosure S :=
202 quotientEquivOfRelatorQuotientMutualMapData R S D.toMutualMapData
204/-- A Tietze equivalence induces an isomorphism of presented groups. -/
205noncomputable def presentedEquiv (D : TietzeEquiv R S) :
206 PresentedGroup R ≃* PresentedGroup S :=
207 quotientEquivOfRelatorQuotientMutualMapData R S D.toMutualMapData
209end TietzeEquiv
211/--
212A free-group equivalence gives a Tietze equivalence between a relator set and its pullback
213relator set.
214-/
215def freeGroupPullbackRelatorTietzeEquiv
216 {X Y : Type*} (e : FreeGroup X ≃* FreeGroup Y)
217 (S : Set (FreeGroup Y)) :
218 TietzeEquiv (freeGroupPullbackRelatorSet e S) S :=
219 TietzeEquiv.ofMutualMapData
220 (relatorQuotientMutualMapDataOfNormalClosureMapEq
221 (freeGroupPullbackRelatorSet e S) S e
222 (map_normalClosure_freeGroupPullbackRelatorSet e S))
224/--
225A presentation packaged with its generator type. This is a light wrapper for writing long Tietze
226scripts whose intermediate presentations may have different generator types.
227-/
228structure Presentation where
229 /-- The type of generators of the presentation. -/
230 Generator : Type u
231 /-- The set of relators in the free group on `Generator`. -/
232 relators : Set (FreeGroup Generator)
234namespace Presentation
236/-- This constructs a presentation from the given relator family. -/
237def ofRelators {X : Type u} (R : Set (FreeGroup X)) : Presentation.{u} where
238 Generator := X
239 relators := R
241end Presentation
243/-- A semantic equivalence certificate between packaged presentations. -/
244structure PresentationEquivCertificate
245 (P : Presentation.{u}) (Q : Presentation.{v}) where
246 /-- The Tietze equivalence between the relator sets of the two presentations. -/
247 toTietzeEquiv : TietzeEquiv P.relators Q.relators
249namespace PresentationEquivCertificate
251/--
252A Tietze equivalence between the relator sets gives a scriptable Tietze certificate between the
253packaged presentations.
254-/
255def ofTietzeEquiv {P : Presentation.{u}} {Q : Presentation.{v}}
256 (D : TietzeEquiv P.relators Q.relators) :
257 PresentationEquivCertificate P Q where
258 toTietzeEquiv := D
260/-- Mutual maps modulo relators determine a Tietze script between the two presentations. -/
261def ofMutualMapData {P : Presentation.{u}} {Q : Presentation.{v}}
262 (D : RelatorQuotientMutualMapData P.relators Q.relators) :
263 PresentationEquivCertificate P Q :=
264 ofTietzeEquiv (TietzeEquiv.ofMutualMapData D)
266/-- Every packaged presentation has its identity semantic equivalence certificate. -/
267def refl (P : Presentation.{u}) : PresentationEquivCertificate P P :=
268 ofTietzeEquiv (TietzeEquiv.refl P.relators)
270/-- Reversing a presentation certificate gives a certificate in the opposite direction. -/
271def symm {P : Presentation.{u}} {Q : Presentation.{v}}
272 (D : PresentationEquivCertificate P Q) :
273 PresentationEquivCertificate Q P :=
274 ofTietzeEquiv D.toTietzeEquiv.symm
276/-- Presentation equivalence certificates compose through an intermediate presentation. -/
277def trans {P : Presentation.{u}} {Q : Presentation.{v}}
278 {U : Presentation.{w}}
279 (D₁ : PresentationEquivCertificate P Q) (D₂ : PresentationEquivCertificate Q U) :
280 PresentationEquivCertificate P U :=
281 ofTietzeEquiv (D₁.toTietzeEquiv.trans D₂.toTietzeEquiv)
283/-- A Tietze script induces an isomorphism of the packaged presented groups. -/
284noncomputable def presentedEquiv
285 {P : Presentation.{u}} {Q : Presentation.{v}}
286 (D : PresentationEquivCertificate P Q) :
287 PresentedGroup P.relators ≃* PresentedGroup Q.relators :=
288 D.toTietzeEquiv.presentedEquiv
290/-- A Tietze script induces an isomorphism of the packaged relator quotients. -/
291noncomputable def quotientEquiv
292 {P : Presentation.{u}} {Q : Presentation.{v}}
293 (D : PresentationEquivCertificate P Q) :
294 FreeGroup P.Generator ⧸ Subgroup.normalClosure P.relators ≃*
295 FreeGroup Q.Generator ⧸ Subgroup.normalClosure Q.relators :=
296 D.toTietzeEquiv.quotientEquiv
298end PresentationEquivCertificate
300namespace TietzeEquiv
302/-- Package a Tietze equivalence as a scriptable Tietze certificate. -/
303def toCertificate
304 {X Y : Type*} {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
305 (D : TietzeEquiv R S) :
306 PresentationEquivCertificate (Presentation.ofRelators R) (Presentation.ofRelators S) :=
307 PresentationEquivCertificate.ofTietzeEquiv D
309end TietzeEquiv
311end ReidemeisterSchreier.Discrete.Presentations