Compression

Part of the dependency closure of the small undecidable group constructions.

def Undecidability.Host.Compression.oldGenerator : Fin 7 → OldGen

The seven Borisov generators, viewed in the nine-generator alphabet used immediately before the ordered Tietze eliminations.

Equations

• One or more equations did not get rendered due to their size.

def Undecidability.Host.Compression.generatorWord (i : Fin 7) : HostWord

The word substituted for each of Borisov's seven generators by the compression.

Equations

• Undecidability.Host.Compression.generatorWord i = Undecidability.Host.tau (Undecidability.Host.Compression.oldGenerator i)

def Undecidability.Host.Compression.word (w : Borisov.BorisovWord) : HostWord

Substitute the ordered words tau into a word on Borisov's seven generators.

Equations

• Undecidability.Host.Compression.word w = Undecidability.Word.substitute Undecidability.Host.Compression.generatorWord w

@[simp]

theorem Undecidability.Host.Compression.word_generator (i : Fin 7) : word (Word.generator i) = generatorWord i

@[simp]

theorem Undecidability.Host.Compression.word_mul (u v : Borisov.BorisovWord) : word (Word.mul u v) = Word.mul (word u) (word v)

@[simp]

theorem Undecidability.Host.Compression.word_inverse (u : Borisov.BorisovWord) : word (Word.inverse u) = Word.inverse (word u)

@[simp]

theorem Undecidability.Host.Compression.word_product (ws : List Borisov.BorisovWord) : word (Word.product ws) = Word.product (List.map word ws)

@[simp]

theorem Undecidability.Host.Compression.word_commutator (u v : Borisov.BorisovWord) : word (Word.commutator u v) = Word.commutator (word u) (word v)

@[simp]

theorem Undecidability.Host.Compression.word_positive (Q : List (Fin 2)) : word (Borisov.positiveWord Q) = positiveWord Q

@[simp]

theorem Undecidability.Host.Compression.word_testWord (Q : List (Fin 2)) : word (Borisov.testWord Q) = testWord Q

theorem Undecidability.Host.Compression.eval_word {G : Type u_1} [Group G] (x : Fin 3 → G) (u : Borisov.BorisovWord) : Word.eval x (word u) = Word.eval (fun (i : Fin 7) => Word.eval x (generatorWord i)) u

Evaluation commutes with the ordered word substitution.

theorem Undecidability.Host.Compression.relator_eq_one (datum : Thue.StandingDatum) (i : Fin 14) : Word.eval (fun (j : Fin 7) => Word.eval (fun (k : Fin 3) => PresentedGroup.of k) (generatorWord j)) ((Borisov.presentation datum).relator i) = 1

Every Borisov relator is satisfied after applying the ordered compression into the three-generator host.

def Undecidability.Host.Compression.hom (datum : Thue.StandingDatum) : (Borisov.presentation datum).Group →* (presentationOf datum).Group

The homomorphism from Borisov's group into the compressed host, induced by the ordered substitution.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Undecidability.Host.Compression.hom_of (datum : Thue.StandingDatum) (i : Fin 7) : (hom datum) (PresentedGroup.of i) = (presentationOf datum).evalWord (generatorWord i)

theorem Undecidability.Host.Compression.hom_evalWord (datum : Thue.StandingDatum) (u : Borisov.BorisovWord) : (hom datum) ((Borisov.presentation datum).evalWord u) = (presentationOf datum).evalWord (word u)

The compression homomorphism evaluates a Borisov word by first applying the syntactic substitution.

theorem Undecidability.Host.Compression.wordProblem_word_of_wordProblem (datum : Thue.StandingDatum) (u : Borisov.BorisovWord) (hu : (Borisov.presentation datum).wordProblem u) : (presentationOf datum).wordProblem (word u)

The elementary direction of preservation: any Borisov word which is one remains one after compression.

def Undecidability.Host.Compression.Injective (datum : Thue.StandingDatum) : Prop

The precise normal-form obligation. In the paper this follows because the two successive HNN extensions are proper, so the original Borisov group embeds in the final host; the six following Tietze eliminations are isomorphisms.

Equations

• Undecidability.Host.Compression.Injective datum = Function.Injective ⇑(Undecidability.Host.Compression.hom datum)

theorem Undecidability.Host.Compression.wordProblem_of_wordProblem_word (datum : Thue.StandingDatum) (hinj : Injective datum) (u : Borisov.BorisovWord) (hu : (presentationOf datum).wordProblem (word u)) : (Borisov.presentation datum).wordProblem u

Injectivity of the compression homomorphism gives reflection of the word problem.

theorem Undecidability.Host.Compression.wordProblem_iff_wordProblem_word (datum : Thue.StandingDatum) (hinj : Injective datum) (u : Borisov.BorisovWord) : (Borisov.presentation datum).wordProblem u ↔ (presentationOf datum).wordProblem (word u)

theorem Undecidability.Host.Compression.testWord_iff (datum : Thue.StandingDatum) (hinj : Injective datum) (Q : List (Fin 2)) : (Borisov.presentation datum).wordProblem (Borisov.testWord Q) ↔ (presentationOf datum).wordProblem (testWord Q)