Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.Script
1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion
3/-!
4# Verified Tietze move scripts
6`ElementaryTietzeMove` records genuine presentation transformations with
7indexed source and target presentations. `VerifiedTietzeScript` is the typed
8sequence of those moves; it evaluates to a semantic
9`PresentationEquivCertificate` and exposes an inspectable trace, move count,
10and weighted cost.
12Semantic equivalence constructors live in the Tietze core and operation
13modules. They are not re-exported here as a parallel family of “script”
14wrappers.
15-/
17universe u
19namespace ReidemeisterSchreier.Discrete.Presentations
22/-- An inspectable, indexed Tietze move whose endpoints are determined by the
23mathematical construction which produces its semantic certificate.
25In particular, the generator moves do not accept an equivalence or a desired
26conclusion as an extra field: their certificates are computed from the
27generator-adjunction and generator-elimination constructions in this library. -/
28inductive ElementaryTietzeMove :
29 Presentation.{u} → Presentation.{u} → Type (u + 1) where
30 /-- Replace a relator set by another set generating the same normal closure. -/
31 | replaceRelators
32 {X : Type u} {R S : Set (FreeGroup X)}
33 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
34 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
35 ElementaryTietzeMove
36 (Presentation.ofRelators R) (Presentation.ofRelators S)
37 /-- Rename every generator through an equivalence of generator types. -/
38 | renameGenerators
39 {X Y : Type u} (R : Set (FreeGroup X)) (e : X ≃ Y) :
40 ElementaryTietzeMove
41 (Presentation.ofRelators R)
42 (Presentation.ofRelators (FreeGroup.freeGroupCongr e '' R))
43 /-- Adjoin generators together with relators identifying them with prescribed words. -/
44 | adjoinGenerators
45 {X Y : Type u} (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
46 ElementaryTietzeMove
47 (Presentation.ofRelators R)
48 (Presentation.ofRelators (Presented.adjoinGeneratorsRelators R word))
49 /-- Eliminate a family of generators by substituting their defining words. -/
50 | substituteDefinedGenerators
51 {X Y : Type u} (R : Set (FreeGroup (Sum X Y)))
52 (word : Y → FreeGroup X) :
53 ElementaryTietzeMove
54 (Presentation.ofRelators
55 (Presented.relatorsWithDefinedGenerators R word))
56 (Presentation.ofRelators
57 (Presented.relatorsAfterSubstitutingDefinedGenerators R word))
58 /-- Delete a family of generators whose defining relators make them trivial. -/
59 | deleteTrivialGenerators
60 {X Y : Type u} (R : Set (FreeGroup (Sum X Y))) :
61 ElementaryTietzeMove
62 (Presentation.ofRelators (Presented.relatorsWithTrivialGenerators R))
63 (Presentation.ofRelators
64 (Presented.relatorsAfterDeletingTrivialGenerators R))
65 /--
66 Transport to a sum decomposition of the generator type and then substitute the defining words.
67 -/
68 | substituteDefinedGeneratorsAlongEquiv
69 {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
70 (word : Y → FreeGroup X) :
71 ElementaryTietzeMove
72 (Presentation.ofRelators
73 (Presented.relatorsWithDefinedGeneratorsAlongEquiv R e word))
74 (Presentation.ofRelators
75 (Presented.relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word))
76 /-- Transport to a sum decomposition and then delete the generators made trivial by relators. -/
77 | deleteTrivialGeneratorsAlongEquiv
78 {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
79 ElementaryTietzeMove
80 (Presentation.ofRelators
81 (Presented.relatorsWithTrivialGeneratorsAlongEquiv R e))
82 (Presentation.ofRelators
83 (Presented.relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e))
85namespace ElementaryTietzeMove
87/-- Stable tags for script traces and cost functions. -/
88inductive Kind where
89 /-- A relator-set replacement. -/
90 | replaceRelators
91 /-- A renaming of generators. -/
92 | renameGenerators
93 /-- An adjunction of generators with defining relators. -/
94 | adjoinGenerators
95 /-- A substitution eliminating generators with specified defining words. -/
96 | substituteDefinedGenerators
97 /-- A deletion of generators made trivial by their defining relators. -/
98 | deleteTrivialGenerators
99deriving DecidableEq, Repr
101/-- Inspect the mathematical kind of an elementary move. -/
102def kind {P Q : Presentation.{u}} : ElementaryTietzeMove P Q → Kind
103 | .replaceRelators _ _ => .replaceRelators
104 | .renameGenerators _ _ => .renameGenerators
105 | .adjoinGenerators _ _ => .adjoinGenerators
106 | .substituteDefinedGenerators _ _ => .substituteDefinedGenerators
107 | .deleteTrivialGenerators _ => .deleteTrivialGenerators
108 | .substituteDefinedGeneratorsAlongEquiv _ _ _ => .substituteDefinedGenerators
109 | .deleteTrivialGeneratorsAlongEquiv _ _ => .deleteTrivialGenerators
111/-- Evaluate one indexed move using its source-producing semantic
112construction. -/
113def toCertificate {P Q : Presentation.{u}}
114 (m : ElementaryTietzeMove P Q) : PresentationEquivCertificate P Q := by
115 cases m with
116 | replaceRelators hR_to_S hS_to_R =>
117 exact (Presented.replaceRelatorsTietzeEquiv hR_to_S hS_to_R).toCertificate
118 | renameGenerators R e =>
119 exact (Presented.renameGeneratorsTietzeEquiv R e).toCertificate
120 | adjoinGenerators R word =>
121 exact (Presented.adjoinGeneratorsTietzeEquiv R word).toCertificate
122 | substituteDefinedGenerators R word =>
123 exact (Presented.substituteDefinedGeneratorsTietzeEquiv R word).toCertificate
124 | deleteTrivialGenerators R =>
125 exact (Presented.deleteTrivialGeneratorsTietzeEquiv R).toCertificate
126 | substituteDefinedGeneratorsAlongEquiv R e word =>
127 exact
128 (Presented.substituteDefinedGeneratorsAlongEquivTietzeEquiv R e word).toCertificate
129 | deleteTrivialGeneratorsAlongEquiv R e =>
130 exact (Presented.deleteTrivialGeneratorsAlongEquivTietzeEquiv R e).toCertificate
132end ElementaryTietzeMove
134/-- A well-typed sequence of genuine Tietze moves. The indexed intermediate
135presentations make an ill-typed move chain unrepresentable. -/
136inductive VerifiedTietzeScript :
137 Presentation.{u} → Presentation.{u} → Type (u + 1) where
138 /-- The empty script at a presentation. -/
139 | nil (P : Presentation.{u}) : VerifiedTietzeScript P P
140 /-- Prepend an elementary move to a verified script beginning at its target presentation. -/
141 | cons {P Q R : Presentation.{u}}
142 (head : ElementaryTietzeMove P Q)
143 (tail : VerifiedTietzeScript Q R) : VerifiedTietzeScript P R
145namespace VerifiedTietzeScript
147/-- A one-move verified script. -/
148def singleton {P Q : Presentation.{u}} (m : ElementaryTietzeMove P Q) :
149 VerifiedTietzeScript P Q :=
150 .cons m (.nil Q)
152/-- A verified relator-replacement move. -/
153def replaceRelators
154 {X : Type u} {R S : Set (FreeGroup X)}
155 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
156 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
157 VerifiedTietzeScript
158 (Presentation.ofRelators R) (Presentation.ofRelators S) :=
159 singleton (.replaceRelators hR_to_S hS_to_R)
161/-- Rename the complete generator family by an equivalence. -/
162def renameGenerators
163 {X Y : Type u} (R : Set (FreeGroup X)) (e : X ≃ Y) :
164 VerifiedTietzeScript
165 (Presentation.ofRelators R)
166 (Presentation.ofRelators (FreeGroup.freeGroupCongr e '' R)) :=
167 singleton (.renameGenerators R e)
169/-- Adjoin a family of generators together with the defining words which make
170the extension a Tietze equivalence. -/
171def adjoinGenerators
172 {X Y : Type u} (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
173 VerifiedTietzeScript
174 (Presentation.ofRelators R)
175 (Presentation.ofRelators (Presented.adjoinGeneratorsRelators R word)) :=
176 singleton (.adjoinGenerators R word)
178/-- Eliminate a family of generators whose defining words have been included
179in the relator family. -/
180def substituteDefinedGenerators
181 {X Y : Type u} (R : Set (FreeGroup (Sum X Y)))
182 (word : Y → FreeGroup X) :
183 VerifiedTietzeScript
184 (Presentation.ofRelators (Presented.relatorsWithDefinedGenerators R word))
185 (Presentation.ofRelators
186 (Presented.relatorsAfterSubstitutingDefinedGenerators R word)) :=
187 singleton (.substituteDefinedGenerators R word)
189/-- Delete a family of generators carrying the relators `y = 1`. -/
190def deleteTrivialGenerators
191 {X Y : Type u} (R : Set (FreeGroup (Sum X Y))) :
192 VerifiedTietzeScript
193 (Presentation.ofRelators (Presented.relatorsWithTrivialGenerators R))
194 (Presentation.ofRelators (Presented.relatorsAfterDeletingTrivialGenerators R)) :=
195 singleton (.deleteTrivialGenerators R)
197/-- Eliminate a family of defined generators after an explicit splitting of
198an arbitrary generator type. -/
199def substituteDefinedGeneratorsAlongEquiv
200 {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
201 (word : Y → FreeGroup X) :
202 VerifiedTietzeScript
203 (Presentation.ofRelators
204 (Presented.relatorsWithDefinedGeneratorsAlongEquiv R e word))
205 (Presentation.ofRelators
206 (Presented.relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word)) :=
207 singleton (.substituteDefinedGeneratorsAlongEquiv R e word)
209/-- Delete trivial generators after an explicit splitting of an arbitrary
210generator type. -/
211def deleteTrivialGeneratorsAlongEquiv
212 {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
213 VerifiedTietzeScript
214 (Presentation.ofRelators
215 (Presented.relatorsWithTrivialGeneratorsAlongEquiv R e))
216 (Presentation.ofRelators
217 (Presented.relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e)) :=
218 singleton (.deleteTrivialGeneratorsAlongEquiv R e)
220/-- Delete exactly the generators selected by a decidable predicate. -/
221def deleteTrivialGeneratorsOfPredicate
222 {Z : Type u} (R : Set (FreeGroup Z)) (delete : Z → Prop)
223 [DecidablePred delete] :
224 VerifiedTietzeScript
225 (Presentation.ofRelators
226 (Presented.relatorsWithTrivialGeneratorsOfPredicate R delete))
227 (Presentation.ofRelators
228 (Presented.relatorsAfterDeletingTrivialGeneratorsOfPredicate R delete)) :=
229 deleteTrivialGeneratorsAlongEquiv R
230 (X := Presented.GeneratorPartition.Kept delete)
231 (Y := Presented.GeneratorPartition.Deleted delete)
232 (Presented.GeneratorPartition.equiv delete)
234/-- Concatenate two verified scripts. -/
235def trans {P Q R : Presentation.{u}}
236 (s : VerifiedTietzeScript P Q) (t : VerifiedTietzeScript Q R) :
237 VerifiedTietzeScript P R :=
238 match s with
239 | .nil _ => t
240 | .cons head tail => .cons head (tail.trans t)
242/-- Evaluate a complete move sequence to its semantic certificate. -/
243def toCertificate {P Q : Presentation.{u}}
244 (s : VerifiedTietzeScript P Q) : PresentationEquivCertificate P Q :=
245 match s with
246 | .nil P => PresentationEquivCertificate.refl P
247 | .cons head tail =>
248 PresentationEquivCertificate.trans head.toCertificate tail.toCertificate
250/-- The inspectable sequence of move kinds. -/
251def trace {P Q : Presentation.{u}}
252 (s : VerifiedTietzeScript P Q) : List ElementaryTietzeMove.Kind :=
253 match s with
254 | .nil _ => []
255 | .cons head tail => head.kind :: tail.trace
257/-- The number of elementary moves in a verified script. -/
258def moveCount {P Q : Presentation.{u}} (s : VerifiedTietzeScript P Q) : ℕ :=
259 s.trace.length
261/-- A customizable additive script cost. -/
262def cost {P Q : Presentation.{u}}
263 (s : VerifiedTietzeScript P Q)
264 (weight : ElementaryTietzeMove.Kind → ℕ) : ℕ :=
265 (s.trace.map weight).sum
267/-- The empty verified script has an empty move trace. -/
268@[simp] theorem trace_nil (P : Presentation.{u}) :
269 (VerifiedTietzeScript.nil P).trace = [] := rfl
271/-- The trace of a script begins with the kind of its head move. -/
272@[simp] theorem trace_cons
273 {P Q R : Presentation.{u}} (head : ElementaryTietzeMove P Q)
274 (tail : VerifiedTietzeScript Q R) :
275 (VerifiedTietzeScript.cons head tail).trace = head.kind :: tail.trace := rfl
277/-- A singleton script records exactly the kind of its sole move. -/
278@[simp] theorem trace_singleton
279 {P Q : Presentation.{u}} (move : ElementaryTietzeMove P Q) :
280 (singleton move).trace = [move.kind] := rfl
282/-- The empty verified script contains no moves. -/
283@[simp] theorem moveCount_nil (P : Presentation.{u}) :
284 (VerifiedTietzeScript.nil P).moveCount = 0 := rfl
286/-- Prepending a move increases the length of a verified script by one. -/
287@[simp] theorem moveCount_cons
288 {P Q R : Presentation.{u}} (head : ElementaryTietzeMove P Q)
289 (tail : VerifiedTietzeScript Q R) :
290 (VerifiedTietzeScript.cons head tail).moveCount = tail.moveCount + 1 := by
291 simp [moveCount, trace, Nat.add_comm]
293/-- A singleton verified script contains one move. -/
294@[simp] theorem moveCount_singleton
295 {P Q : Presentation.{u}} (move : ElementaryTietzeMove P Q) :
296 (singleton move).moveCount = 1 := rfl
298/-- Concatenating verified scripts adds their move counts. -/
299@[simp] theorem moveCount_trans
300 {P Q R : Presentation.{u}} (s : VerifiedTietzeScript P Q)
301 (t : VerifiedTietzeScript Q R) :
302 (s.trans t).moveCount = s.moveCount + t.moveCount := by
303 induction s with
304 | nil => simp [trans, moveCount, trace]
305 | cons head tail ih =>
306 simp [trans, ih, Nat.add_assoc, Nat.add_comm]
308/-- The empty verified script has zero cost for every weighting. -/
309@[simp] theorem cost_nil
310 (weight : ElementaryTietzeMove.Kind → ℕ) (P : Presentation.{u}) :
311 (VerifiedTietzeScript.nil P).cost weight = 0 := rfl
313/-- The cost of a nonempty script is the head move's weight plus the tail cost. -/
314@[simp] theorem cost_cons
315 (weight : ElementaryTietzeMove.Kind → ℕ)
316 {P Q R : Presentation.{u}} (head : ElementaryTietzeMove P Q)
317 (tail : VerifiedTietzeScript Q R) :
318 (VerifiedTietzeScript.cons head tail).cost weight =
319 weight head.kind + tail.cost weight := rfl
321/-- The cost of a singleton script is the weight assigned to its sole move. -/
322@[simp] theorem cost_singleton
323 (weight : ElementaryTietzeMove.Kind → ℕ)
324 {P Q : Presentation.{u}} (move : ElementaryTietzeMove P Q) :
325 (singleton move).cost weight = weight move.kind := by
326 simp [singleton]
328end VerifiedTietzeScript
330end ReidemeisterSchreier.Discrete.Presentations