The compressed Miller--Tancer construction

When the normally generating word is a displayed generator x_k, the relations σ₁ and σ₄(x_k) permit two further uniform Tietze eliminations. The resulting presentation has n + 1 generators and m + 2 relators and presents the same group as the raw construction.

theorem Undecidability.MillerTancer.presentsTrivial_transform_iff {n m : ℕ} (P : FP n m) (z : Word n) (hz : P.NormallyGenerates z) (w : Word n) : (transform P z w).presentsTrivial ↔ P.wordProblem w

The raw Miller--Tancer triviality criterion.

def Undecidability.MillerTancer.Compressed.finalOldSlot {n : ℕ} (i : Fin n) : Fin (n + 1)

The slot retaining an original generator in the compressed presentation.

Equations

• Undecidability.MillerTancer.Compressed.finalOldSlot i = i.castSucc

def Undecidability.MillerTancer.Compressed.bWord {n : ℕ} (k : Fin n) : Word (n + 1)

The word representing the generator b in this presentation.

Equations

• Undecidability.MillerTancer.Compressed.bWord k = Undecidability.Word.generator (Undecidability.MillerTancer.Compressed.finalOldSlot k)

def Undecidability.MillerTancer.Compressed.qWord (n : ℕ) : Word (n + 1)

The word representing the new compression generator q.

Equations

• Undecidability.MillerTancer.Compressed.qWord n = Undecidability.Word.generator (Fin.last n)

def Undecidability.MillerTancer.Compressed.cWord {n : ℕ} (k : Fin n) : Word (n + 1)

The word representing the element c after the indicated substitutions.

Equations

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

def Undecidability.MillerTancer.Compressed.aWord {n : ℕ} (k : Fin n) : Word (n + 1)

The word representing the generator a in this presentation.

Equations

• Undecidability.MillerTancer.Compressed.aWord k = Undecidability.Word.product [(Undecidability.MillerTancer.Compressed.qWord n).inverse, Undecidability.MillerTancer.Compressed.cWord k]

def Undecidability.MillerTancer.Compressed.eliminatedWord {n : ℕ} (k : Fin n) : Word (n + 1)

The substitution word for the original generator eliminated by the compression.

Equations

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

def Undecidability.MillerTancer.Compressed.encodedOldGenerator {n : ℕ} (k i : Fin n) : Word (n + 1)

The substitution for an original generator, eliminating the distinguished one.

Equations

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

def Undecidability.MillerTancer.Compressed.thetaGenerator {n : ℕ} (k : Fin n) : Fin (n + 3) → Word (n + 1)

The generator substitution performing the ordered Tietze eliminations.

Equations

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

def Undecidability.MillerTancer.Compressed.thetaWord {n : ℕ} (k : Fin n) (w : Word (n + 3)) : Word (n + 1)

Extend the Tietze generator substitution to an arbitrary word.

Equations

• Undecidability.MillerTancer.Compressed.thetaWord k w = Undecidability.Word.substitute (Undecidability.MillerTancer.Compressed.thetaGenerator k) w

def Undecidability.MillerTancer.Compressed.keptAdditionalIndex : Fin 2 → Fin 4

The two additional relators retained after eliminating the redundant relations.

Equations

• Undecidability.MillerTancer.Compressed.keptAdditionalIndex = ![1, 2]

def Undecidability.MillerTancer.Compressed.retainedIndex (m : ℕ) : Fin (m + 2) → Fin (m + 4)

The indices of the original and additional relators retained by the compression.

Equations

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

def Undecidability.MillerTancer.Compressed.transform {n m : ℕ} (P : FP n m) (k : Fin n) (w : Word n) : FP (n + 1) (m + 2)

The presentation retaining the original relators and two additional relations after generator elimination.

Equations

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

@[simp]

theorem Undecidability.MillerTancer.Compressed.retainedIndex_old {m : ℕ} (i : Fin m) : retainedIndex m (Fin.castAdd 2 i) = Fin.castAdd 4 i

@[simp]

theorem Undecidability.MillerTancer.Compressed.retainedIndex_additional {m : ℕ} (j : Fin 2) : retainedIndex m (Fin.natAdd m j) = Fin.natAdd m (keptAdditionalIndex j)

@[simp]

theorem Undecidability.MillerTancer.Compressed.transform_old {n m : ℕ} (P : FP n m) (k : Fin n) (w : Word n) (i : Fin m) : (transform P k w).relator (Fin.castAdd 2 i) = thetaWord k (oldWord (P.relator i))

@[simp]

theorem Undecidability.MillerTancer.Compressed.transform_additional {n m : ℕ} (P : FP n m) (k : Fin n) (w : Word n) (j : Fin 2) : (transform P k w).relator (Fin.natAdd m j) = thetaWord k (additionalRelators (Word.generator k) w (keptAdditionalIndex j))

theorem Undecidability.MillerTancer.Compressed.thetaWord_primrec {n : ℕ} (k : Fin n) : Primrec (thetaWord k)

theorem Undecidability.MillerTancer.Compressed.transform_computable {n m : ℕ} (P : FP n m) (k : Fin n) : Computable₂ fun (w : Word n) (i : Fin (m + 2)) => (transform P k w).relator i

@[simp]

theorem Undecidability.MillerTancer.Compressed.eval_thetaWord {n : ℕ} {G : Type u_1} [Group G] (x : Fin (n + 1) → G) (k : Fin n) (w : Word (n + 3)) : Word.eval x (thetaWord k w) = Word.eval (fun (i : Fin (n + 3)) => Word.eval x (thetaGenerator k i)) w

@[simp]

theorem Undecidability.MillerTancer.Compressed.thetaGenerator_old {n : ℕ} (k i : Fin n) : thetaGenerator k (oldGenerator i) = encodedOldGenerator k i

theorem Undecidability.MillerTancer.Compressed.theta_sigma₁_eval_one {n : ℕ} {G : Type u_1} [Group G] (x : Fin (n + 1) → G) (k : Fin n) : Word.eval x (thetaWord k (sigma₁ n)) = 1

theorem Undecidability.MillerTancer.Compressed.theta_sigma₄_eval_one {n : ℕ} {G : Type u_1} [Group G] (x : Fin (n + 1) → G) (k : Fin n) : Word.eval x (thetaWord k (sigma₄ (Word.generator k))) = 1

def Undecidability.MillerTancer.Compressed.forwardHom {n m : ℕ} (P : FP n m) (k : Fin n) (w : Word n) : (MillerTancer.transform P (Word.generator k) w).Group →* (transform P k w).Group

The homomorphism from the original presentation to its compressed presentation.

Equations

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

def Undecidability.MillerTancer.Compressed.reverseGenerator {n m : ℕ} (P : FP n m) (k : Fin n) (w : Word n) : Fin (n + 1) → (MillerTancer.transform P (Word.generator k) w).Group

The original-group interpretations of the generators of the compressed presentation.

Equations

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

theorem Undecidability.MillerTancer.Compressed.eval_thetaGenerator_reverse {n m : ℕ} (P : FP n m) (k : Fin n) (w : Word n) (i : Fin (n + 3)) : Word.eval (reverseGenerator P k w) (thetaGenerator k i) = PresentedGroup.of i

def Undecidability.MillerTancer.Compressed.reverseHom {n m : ℕ} (P : FP n m) (k : Fin n) (w : Word n) : (transform P k w).Group →* (MillerTancer.transform P (Word.generator k) w).Group

The homomorphism interpreting the compressed presentation in the original group.

Equations

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

theorem Undecidability.MillerTancer.Compressed.reverse_forward {n m : ℕ} (P : FP n m) (k : Fin n) (w : Word n) : (reverseHom P k w).comp (forwardHom P k w) = MonoidHom.id (MillerTancer.transform P (Word.generator k) w).Group

theorem Undecidability.MillerTancer.Compressed.forward_reverse {n m : ℕ} (P : FP n m) (k : Fin n) (w : Word n) : (forwardHom P k w).comp (reverseHom P k w) = MonoidHom.id (transform P k w).Group

def Undecidability.MillerTancer.Compressed.transformEquiv {n m : ℕ} (P : FP n m) (k : Fin n) (w : Word n) : (MillerTancer.transform P (Word.generator k) w).Group ≃* (transform P k w).Group

The compressed presentation is isomorphic to the raw Miller--Tancer presentation.

Equations

• Undecidability.MillerTancer.Compressed.transformEquiv P k w = (Undecidability.MillerTancer.Compressed.forwardHom P k w).toMulEquiv (Undecidability.MillerTancer.Compressed.reverseHom P k w) ⋯ ⋯

theorem Undecidability.MillerTancer.Compressed.presentsTrivial_transform_iff_raw {n m : ℕ} (P : FP n m) (k : Fin n) (w : Word n) : (transform P k w).presentsTrivial ↔ (MillerTancer.transform P (Word.generator k) w).presentsTrivial

Compression preserves the presented group, hence triviality.

theorem Undecidability.MillerTancer.Compressed.presentsTrivial_transform_iff {n m : ℕ} (P : FP n m) (k : Fin n) (hk : P.NormallyGenerates (Word.generator k)) (w : Word n) : (transform P k w).presentsTrivial ↔ P.wordProblem w

The compressed Miller--Tancer triviality criterion.