Source: ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.CleanedSymbols
1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.KernelQuotient
2import ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Tau
5/-!
6# Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Cleaned Symbols
8This module separates degenerate Schreier symbols from genuine generators and
9sets up the relator families needed to delete the trivial generators from the
10finite-quotient presentation.
11-/
13namespace ReidemeisterSchreier.Discrete
15open ReidemeisterSchreier.Discrete.Presentations
17variable {X Q : Type*} [Group Q] [Fintype Q]
19namespace FiniteQuotientSchreierData
21variable (D : FiniteQuotientSchreierData X Q)
22variable [DecidableEq X]
24omit [DecidableEq X] in
25/--
26Predicate saying that a finite Schreier symbol is degenerate and should be deleted from the
27cleaned presentation.
28-/
29def IsDegenerateSchreierSymbol (z : FiniteSchreierSymbol X Q) : Prop :=
30 D.quotientSection (D.transition z.1 z.2) =
31 D.quotientSection z.1 * FreeGroup.of z.2
33omit [DecidableEq X] in
34/--
35The set of degenerate finite-quotient Schreier relators killed when deleting degenerate symbols.
36-/
37def degenerateSchreierRelators :
38 Set (FreeGroup (FiniteSchreierSymbol X Q)) :=
39 { q | ∃ s : Q, ∃ x : X,
40 D.quotientSection (D.transition s x) = D.quotientSection s * FreeGroup.of x ∧
41 q = FreeGroup.of (s, x) }
43/--
44The finite-quotient presentation relators are the Schreier relators together with the degenerate
45Schreier-generator relators.
46-/
47def presentationRelators (R : Set (FreeGroup X)) :
48 Set (FreeGroup (FiniteSchreierSymbol X Q)) :=
49 D.schreierRelators R ∪ D.degenerateSchreierRelators
51omit [DecidableEq X] in
52/-- The type of finite Schreier symbols kept after deleting degenerate symbols. -/
53abbrev NondegenerateSchreierSymbol :=
54 Presented.GeneratorPartition.Kept D.IsDegenerateSchreierSymbol
56omit [DecidableEq X] in
57/-- The type of finite Schreier symbols marked for deletion as degenerate. -/
58abbrev DegenerateSchreierSymbol :=
59 Presented.GeneratorPartition.Deleted D.IsDegenerateSchreierSymbol
61omit [DecidableEq X] in
62/--
63The trivial-generator relators selected by the degeneracy predicate are exactly the degenerate
64Schreier relators.
65-/
66theorem trivialGeneratorRelatorsOfPredicate_isDegenerateSchreierSymbol
67 [DecidablePred D.IsDegenerateSchreierSymbol] :
68 Presented.trivialGeneratorRelatorsOfPredicate D.IsDegenerateSchreierSymbol =
69 D.degenerateSchreierRelators := by
70 ext q
71 constructor
72 · intro hq
73 rcases hq with ⟨p, hp, hpq⟩
74 rcases hp with ⟨y, rfl⟩
75 rcases y with ⟨⟨s, x⟩, hy⟩
76 refine ⟨s, x, hy, ?_⟩
77 rw [← hpq]
78 simp only [FreeGroup.freeGroupCongr, MulEquiv.symm_mk, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk,
79 FreeGroup.map.of, Presented.GeneratorPartition.equiv_symm_inr]
80 · rintro ⟨s, x, hdeg, rfl⟩
81 refine ⟨FreeGroup.of (Sum.inr
82 (⟨(s, x), hdeg⟩ : D.DegenerateSchreierSymbol)), ?_, ?_⟩
83 · exact ⟨⟨(s, x), hdeg⟩, rfl⟩
84 · simp only [FreeGroup.freeGroupCongr, MulEquiv.symm_mk, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk,
85 FreeGroup.map.of, Presented.GeneratorPartition.equiv_symm_inr]
87/--
88Adding trivial-generator relators for degenerate Schreier symbols gives the presentation
89relators.
90-/
91theorem relatorsWithTrivialGeneratorsOfPredicate_isDegenerateSchreierSymbol
92 (R : Set (FreeGroup X))
93 [DecidablePred D.IsDegenerateSchreierSymbol] :
94 Presented.relatorsWithTrivialGeneratorsOfPredicate
95 (D.schreierRelators R) D.IsDegenerateSchreierSymbol =
96 D.presentationRelators R := by
97 change D.schreierRelators R ∪
98 Presented.trivialGeneratorRelatorsOfPredicate D.IsDegenerateSchreierSymbol =
99 D.schreierRelators R ∪ D.degenerateSchreierRelators
100 rw [D.trivialGeneratorRelatorsOfPredicate_isDegenerateSchreierSymbol]
102/--
103The raw finite Reidemeister--Schreier relators after deleting the degenerate Schreier generators
104with relators \(s(q,x)=1\).
105-/
106def presentationRelatorsAfterDeletingDegenerateSchreierGenerators
107 (R : Set (FreeGroup X))
108 [DecidablePred D.IsDegenerateSchreierSymbol] :
109 Set (FreeGroup D.NondegenerateSchreierSymbol) :=
110 Presented.relatorsAfterDeletingTrivialGeneratorsOfPredicate
111 (D.schreierRelators R) D.IsDegenerateSchreierSymbol
113/--
114Deleting degenerate finite Schreier generators gives a Tietze equivalence with the cleaned
115presentation.
116-/
117def deleteDegenerateSchreierGeneratorsScript
118 (R : Set (FreeGroup X))
119 [DecidablePred D.IsDegenerateSchreierSymbol] :
120 VerifiedTietzeScript
121 (Presentation.ofRelators (D.presentationRelators R))
122 (Presentation.ofRelators
123 (D.presentationRelatorsAfterDeletingDegenerateSchreierGenerators R)) := by
124 let hRelators :=
125 D.relatorsWithTrivialGeneratorsOfPredicate_isDegenerateSchreierSymbol R
126 exact
127 (VerifiedTietzeScript.replaceRelators
128 (fun r hr => RelatorEquivalent.of_mem (by simpa only [hRelators] using hr))
129 (fun r hr => RelatorEquivalent.of_mem (by simpa only [hRelators] using hr))).trans
130 (VerifiedTietzeScript.deleteTrivialGeneratorsOfPredicate
131 (D.schreierRelators R) D.IsDegenerateSchreierSymbol)
133/-- The cleaned-symbol construction first identifies the proved-equal relator
134families and then performs one indexed generator-deletion move. This theorem
135makes the maintained concrete consumer visible to trace and cost clients. -/
136theorem deleteDegenerateSchreierGeneratorsScript_trace
137 (R : Set (FreeGroup X))
138 [DecidablePred D.IsDegenerateSchreierSymbol] :
139 (D.deleteDegenerateSchreierGeneratorsScript R).trace =
140 [ElementaryTietzeMove.Kind.replaceRelators,
141 ElementaryTietzeMove.Kind.deleteTrivialGenerators] := by
142 simp [deleteDegenerateSchreierGeneratorsScript,
143 VerifiedTietzeScript.replaceRelators,
144 VerifiedTietzeScript.deleteTrivialGeneratorsOfPredicate,
145 VerifiedTietzeScript.deleteTrivialGeneratorsAlongEquiv,
146 VerifiedTietzeScript.singleton, VerifiedTietzeScript.trans,
147 VerifiedTietzeScript.trace,
148 ElementaryTietzeMove.kind]
150/-- The deletion script's weighted cost is the cost of replacing relators plus the weighted
151cost of deleting each degenerate Schreier generator. -/
152theorem deleteDegenerateSchreierGeneratorsScript_cost
153 (R : Set (FreeGroup X))
154 [DecidablePred D.IsDegenerateSchreierSymbol]
155 (weight : ElementaryTietzeMove.Kind → ℕ) :
156 (D.deleteDegenerateSchreierGeneratorsScript R).cost weight =
157 weight ElementaryTietzeMove.Kind.replaceRelators +
158 weight ElementaryTietzeMove.Kind.deleteTrivialGenerators := by
159 simp [deleteDegenerateSchreierGeneratorsScript,
160 VerifiedTietzeScript.replaceRelators,
161 VerifiedTietzeScript.deleteTrivialGeneratorsOfPredicate,
162 VerifiedTietzeScript.deleteTrivialGeneratorsAlongEquiv,
163 VerifiedTietzeScript.singleton, VerifiedTietzeScript.trans,
164 VerifiedTietzeScript.cost,
165 VerifiedTietzeScript.trace, ElementaryTietzeMove.kind]
167/--
168Deleting degenerate finite Schreier generators produces the cleaned presentation on
169nondegenerate Schreier symbols.
170-/
171noncomputable def deleteDegenerateSchreierGenerators
172 (R : Set (FreeGroup X))
173 [DecidablePred D.IsDegenerateSchreierSymbol] :
174 PresentedGroup (D.presentationRelators R) ≃*
175 PresentedGroup
176 (D.presentationRelatorsAfterDeletingDegenerateSchreierGenerators R) :=
177 (D.deleteDegenerateSchreierGeneratorsScript R).toCertificate.presentedEquiv
179/--
180The homomorphism that deletes degenerate finite Schreier generators. A nondegenerate generator
181is kept, and a degenerate generator is sent to \(1\).
182-/
183def deleteDegenerateSchreierGeneratorHom
184 [DecidablePred D.IsDegenerateSchreierSymbol] :
185 FreeGroup (FiniteSchreierSymbol X Q) →*
186 FreeGroup D.NondegenerateSchreierSymbol :=
187 (Presented.trivializeGeneratorsHom
188 D.NondegenerateSchreierSymbol D.DegenerateSchreierSymbol).comp
189 (FreeGroup.freeGroupCongr
190 (Presented.GeneratorPartition.equiv D.IsDegenerateSchreierSymbol))
192omit [DecidableEq X] in
193/--
194The generator-deletion homomorphism sends a nondegenerate finite Schreier generator to the
195corresponding nondegenerate generator.
196-/
197@[simp]
198theorem deleteDegenerateSchreierGeneratorHom_of_not_degenerate
199 [DecidablePred D.IsDegenerateSchreierSymbol]
200 {z : FiniteSchreierSymbol X Q} (hz : ¬ D.IsDegenerateSchreierSymbol z) :
201 D.deleteDegenerateSchreierGeneratorHom (FreeGroup.of z) =
202 FreeGroup.of (⟨z, hz⟩ : D.NondegenerateSchreierSymbol) := by
203 simp only [deleteDegenerateSchreierGeneratorHom, MonoidHom.coe_comp, MonoidHom.coe_coe,
204 Function.comp_apply,
205 FreeGroup.freeGroupCongr_apply, FreeGroup.map.of,
206 Presented.GeneratorPartition.equiv_apply_of_not_delete D.IsDegenerateSchreierSymbol hz]
207 exact Presented.trivializeGeneratorsHom_inl
208 (X := D.NondegenerateSchreierSymbol)
209 (Y := D.DegenerateSchreierSymbol)
210 (⟨z, hz⟩ : D.NondegenerateSchreierSymbol)
212omit [DecidableEq X] in
213/--
214The generator-deletion homomorphism sends a degenerate finite Schreier generator to the
215identity.
216-/
217@[simp]
218theorem deleteDegenerateSchreierGeneratorHom_of_degenerate
219 [DecidablePred D.IsDegenerateSchreierSymbol]
220 {z : FiniteSchreierSymbol X Q} (hz : D.IsDegenerateSchreierSymbol z) :
221 D.deleteDegenerateSchreierGeneratorHom (FreeGroup.of z) = 1 := by
222 simp only [deleteDegenerateSchreierGeneratorHom, MonoidHom.coe_comp, MonoidHom.coe_coe,
223 Function.comp_apply,
224 FreeGroup.freeGroupCongr_apply, FreeGroup.map.of,
225 Presented.GeneratorPartition.equiv_apply_of_delete D.IsDegenerateSchreierSymbol hz]
226 exact Presented.trivializeGeneratorsHom_inr
227 (X := D.NondegenerateSchreierSymbol)
228 (Y := D.DegenerateSchreierSymbol)
229 (⟨z, hz⟩ : D.DegenerateSchreierSymbol)
231omit [DecidableEq X] in
232/-- A degenerate Schreier symbol evaluates to the identity. -/
233theorem symbolEval_eq_one_of_isDegenerateSchreierSymbol
234 {z : FiniteSchreierSymbol X Q} (hz : D.IsDegenerateSchreierSymbol z) :
235 D.symbolEval z = 1 := by
236 rcases z with ⟨q, x⟩
237 simp only [IsDegenerateSchreierSymbol, transition_eq, symbolEval, schreierGenerator] at hz ⊢
238 rw [hz]
239 group
241/-- The evaluation map on the nondegenerate finite Schreier generators. -/
242def nondegenerateSymbolEval
243 (z : D.NondegenerateSchreierSymbol) : FreeGroup X :=
244 D.symbolEval z.1
246/-- The evaluation homomorphism on nondegenerate finite Schreier symbols. -/
247def nondegenerateSymbolEvalHom :
248 FreeGroup D.NondegenerateSchreierSymbol →* FreeGroup X :=
249 FreeGroup.lift D.nondegenerateSymbolEval
251omit [DecidableEq X] in
252/--
253Evaluating after deleting degenerate Schreier generators agrees with ordinary symbol evaluation.
254-/
255theorem nondegenerateSymbolEvalHom_deleteDegenerateSchreierGeneratorHom
256 [DecidablePred D.IsDegenerateSchreierSymbol]
257 (w : FreeGroup (FiniteSchreierSymbol X Q)) :
258 D.nondegenerateSymbolEvalHom
259 (D.deleteDegenerateSchreierGeneratorHom w) =
260 D.symbolEvalHom w := by
261 let F : FreeGroup (FiniteSchreierSymbol X Q) →* FreeGroup X :=
262 D.nondegenerateSymbolEvalHom.comp D.deleteDegenerateSchreierGeneratorHom
263 have hF : F = D.symbolEvalHom := by
264 ext z
265 by_cases hz : D.IsDegenerateSchreierSymbol z
266 · simp only [MonoidHom.coe_comp, Function.comp_apply,
267 D.deleteDegenerateSchreierGeneratorHom_of_degenerate hz,
268 map_one, symbolEvalHom_of, D.symbolEval_eq_one_of_isDegenerateSchreierSymbol hz, F]
269 · simp only [MonoidHom.coe_comp, Function.comp_apply,
270 D.deleteDegenerateSchreierGeneratorHom_of_not_degenerate hz,
271 symbolEvalHom_of, F]
272 change D.nondegenerateSymbolEvalHom (FreeGroup.of ⟨z, hz⟩) =
273 D.symbolEval z
274 rw [nondegenerateSymbolEvalHom, FreeGroup.lift_apply_of]
275 rfl
276 exact congrArg (fun f : FreeGroup (FiniteSchreierSymbol X Q) →* FreeGroup X => f w) hF
278/-- A single finite Schreier generator after deleting degenerate generators. -/
279def cleanedSchreierSymbolWord
280 [DecidablePred D.IsDegenerateSchreierSymbol]
281 (z : FiniteSchreierSymbol X Q) :
282 FreeGroup D.NondegenerateSchreierSymbol :=
283 if hz : D.IsDegenerateSchreierSymbol z then
284 1
285 else
286 FreeGroup.of (⟨z, hz⟩ : D.NondegenerateSchreierSymbol)
288omit [DecidableEq X] in
289/-- A degenerate Schreier symbol is deleted by the cleaned Schreier-symbol word map. -/
290@[simp]
291theorem cleanedSchreierSymbolWord_of_degenerate
292 [DecidablePred D.IsDegenerateSchreierSymbol]
293 {z : FiniteSchreierSymbol X Q} (hz : D.IsDegenerateSchreierSymbol z) :
294 D.cleanedSchreierSymbolWord z = 1 := by
295 simp only [cleanedSchreierSymbolWord, hz, ↓reduceDIte]
297omit [DecidableEq X] in
298/--
299A nondegenerate Schreier symbol is kept as the corresponding generator by the cleaned
300Schreier-symbol word map.
301-/
302@[simp]
303theorem cleanedSchreierSymbolWord_of_not_degenerate
304 [DecidablePred D.IsDegenerateSchreierSymbol]
305 {z : FiniteSchreierSymbol X Q} (hz : ¬ D.IsDegenerateSchreierSymbol z) :
306 D.cleanedSchreierSymbolWord z =
307 FreeGroup.of (⟨z, hz⟩ : D.NondegenerateSchreierSymbol) := by
308 simp only [cleanedSchreierSymbolWord, hz, ↓reduceDIte]
309 congr
311omit [DecidableEq X] in
312/--
313The generator-deletion homomorphism sends a finite Schreier generator to its cleaned
314Schreier-symbol word.
315-/
316@[simp]
317theorem deleteDegenerateSchreierGeneratorHom_of
318 [DecidablePred D.IsDegenerateSchreierSymbol]
319 (z : FiniteSchreierSymbol X Q) :
320 D.deleteDegenerateSchreierGeneratorHom (FreeGroup.of z) =
321 D.cleanedSchreierSymbolWord z := by
322 by_cases hz : D.IsDegenerateSchreierSymbol z
323 · simp only [hz, deleteDegenerateSchreierGeneratorHom_of_degenerate,
324 cleanedSchreierSymbolWord_of_degenerate]
325 · simp only [hz, not_false_eq_true, deleteDegenerateSchreierGeneratorHom_of_not_degenerate,
326 cleanedSchreierSymbolWord_of_not_degenerate]
329end FiniteQuotientSchreierData
331end ReidemeisterSchreier.Discrete