Presentation

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

@[reducible, inline]

abbrev Undecidability.SignedGenerator (n : ℕ) : Type

A letter in a word on n generators. The Boolean records the sign.

Equations

• Undecidability.SignedGenerator n = (Fin n × Bool)

@[reducible, inline]

abbrev Undecidability.Word (n : ℕ) : Type

A word on n generators.

Equations

• Undecidability.Word n = List (Undecidability.SignedGenerator n)

def Undecidability.Word.one {n : ℕ} : Word n

The empty word.

Equations

• Undecidability.Word.one = []

def Undecidability.Word.generator {n : ℕ} (i : Fin n) : Word n

A positive generator as a one-letter word.

Equations

• Undecidability.Word.generator i = [(i, true)]

def Undecidability.Word.inverse {n : ℕ} (w : Word n) : Word n

Formal inverse of a word.

Equations

• w.inverse = List.map (fun (x : Undecidability.SignedGenerator n) => (x.1, !x.2)) (List.reverse w)

theorem Undecidability.Word.inverse_primrec (n : ℕ) : Primrec inverse

Formal word inversion is primitive recursive for the standard word encoding.

def Undecidability.Word.mul {n : ℕ} (u v : Word n) : Word n

Multiplication of words is concatenation.

Equations

• u.mul v = u ++ v

def Undecidability.Word.product {n : ℕ} (ws : List (Word n)) : Word n

Concatenate a finite list of words.

Equations

• Undecidability.Word.product ws = ws.flatten

def Undecidability.Word.pow {n : ℕ} (w : Word n) (k : ℕ) : Word n

A nonnegative power of a word.

Equations

• w.pow k = (List.replicate k w).flatten

def Undecidability.Word.mapGenerators {n k : ℕ} (f : Fin n → Fin k) (w : Word n) : Word k

Reindex the generators occurring in a word.

Equations

• Undecidability.Word.mapGenerators f w = List.map (fun (x : Undecidability.SignedGenerator n) => (f x.1, x.2)) w

def Undecidability.Word.substitutePositive {n : ℕ} (s₁ s₂ : Word n) (w : List (Fin 2)) : Word n

Interpret a positive two-letter word by substituting two group words.

Equations

• s₁.substitutePositive s₂ w = List.flatMap (fun (i : Fin 2) => if i = 0 then s₁ else s₂) w

def Undecidability.Word.substitute {n : ℕ} {A : Type u_1} (s : A → Word n) (w : List (A × Bool)) : Word n

Substitute a word for every signed generator in a word.

Equations

• Undecidability.Word.substitute s w = List.flatMap (fun (x : A × Bool) => if x.2 = true then s x.1 else (s x.1).inverse) w

def Undecidability.Word.relation {n : ℕ} (lhs rhs : Word n) : Word n

The relator corresponding to the equation lhs = rhs.

Equations

• lhs.relation rhs = lhs.mul rhs.inverse

def Undecidability.Word.commutator {n : ℕ} (u v : Word n) : Word n

The commutator convention [u,v] = u⁻¹v⁻¹uv used in the paper.

Equations

• u.commutator v = u.inverse.mul (v.inverse.mul (u.mul v))

@[simp]

theorem Undecidability.Word.inverse_mul {n : ℕ} (u v : Word n) : (u.mul v).inverse = v.inverse.mul u.inverse

@[simp]

theorem Undecidability.Word.inverse_inverse {n : ℕ} (w : Word n) : w.inverse.inverse = w

@[simp]

theorem Undecidability.Word.substitute_append {n : ℕ} {A : Type u_1} (s : A → Word n) (u v : List (A × Bool)) : substitute s (u ++ v) = (substitute s u).mul (substitute s v)

@[simp]

theorem Undecidability.Word.substitute_invRev {n : ℕ} {A : Type u_1} (s : A → Word n) (w : List (A × Bool)) : substitute s (FreeGroup.invRev w) = (substitute s w).inverse

@[simp]

theorem Undecidability.Word.substitute_flatten {n : ℕ} {A : Type u_1} (s : A → Word n) (ws : List (List (A × Bool))) : substitute s ws.flatten = product (List.map (substitute s) ws)

def Undecidability.Word.eval {n : ℕ} {G : Type u_1} [Group G] (x : Fin n → G) (w : Word n) : G

Evaluate a syntactic word after choosing values for its generators.

Equations

• Undecidability.Word.eval x w = (FreeGroup.lift x) (FreeGroup.mk w)

@[simp]

theorem Undecidability.Word.eval_generator {n : ℕ} {G : Type u_1} [Group G] (x : Fin n → G) (i : Fin n) : eval x (generator i) = x i

@[simp]

theorem Undecidability.Word.eval_mul {n : ℕ} {G : Type u_1} [Group G] (x : Fin n → G) (u v : Word n) : eval x (u.mul v) = eval x u * eval x v

@[simp]

theorem Undecidability.Word.eval_append {n : ℕ} {G : Type u_1} [Group G] (x : Fin n → G) (u v : Word n) : eval x (u ++ v) = eval x u * eval x v

theorem Undecidability.Word.mk_inverse {n : ℕ} (w : Word n) : FreeGroup.mk w.inverse = (FreeGroup.mk w)⁻¹

@[simp]

theorem Undecidability.Word.eval_inverse {n : ℕ} {G : Type u_1} [Group G] (x : Fin n → G) (w : Word n) : eval x w.inverse = (eval x w)⁻¹

@[simp]

theorem Undecidability.Word.eval_pow {n : ℕ} {G : Type u_1} [Group G] (x : Fin n → G) (w : Word n) (k : ℕ) : eval x (w.pow k) = eval x w ^ k

@[simp]

theorem Undecidability.Word.eval_product {n : ℕ} {G : Type u_1} [Group G] (x : Fin n → G) (ws : List (Word n)) : eval x (product ws) = (List.map (eval x) ws).prod

@[simp]

theorem Undecidability.Word.eval_mapGenerators {k n : ℕ} {G : Type u_1} [Group G] (x : Fin k → G) (f : Fin n → Fin k) (w : Word n) : eval x (mapGenerators f w) = eval (x ∘ f) w

theorem Undecidability.Word.map_eval {n : ℕ} {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (x : Fin n → G) (w : Word n) : f (eval x w) = eval (⇑f ∘ x) w

@[simp]

theorem Undecidability.Word.eval_substitutePositive {n : ℕ} {G : Type u_1} [Group G] (x : Fin n → G) (s₁ s₂ : Word n) (w : List (Fin 2)) : eval x (s₁.substitutePositive s₂ w) = (List.map (fun (i : Fin 2) => if i = 0 then eval x s₁ else eval x s₂) w).prod

@[simp]

theorem Undecidability.Word.eval_substitute {k n : ℕ} {G : Type u_1} [Group G] (x : Fin k → G) (s : Fin n → Word k) (w : Word n) : eval x (substitute s w) = eval (fun (i : Fin n) => eval x (s i)) w

@[simp]

theorem Undecidability.Word.eval_relation {n : ℕ} {G : Type u_1} [Group G] (x : Fin n → G) (lhs rhs : Word n) : eval x (lhs.relation rhs) = eval x lhs * (eval x rhs)⁻¹

theorem Undecidability.Word.eval_relation_eq_one_iff {n : ℕ} {G : Type u_1} [Group G] (x : Fin n → G) (lhs rhs : Word n) : eval x (lhs.relation rhs) = 1 ↔ eval x lhs = eval x rhs

@[simp]

theorem Undecidability.Word.eval_commutator {n : ℕ} {G : Type u_1} [Group G] (x : Fin n → G) (u v : Word n) : eval x (u.commutator v) = (eval x u)⁻¹ * (eval x v)⁻¹ * eval x u * eval x v

structure Undecidability.FP (n m : ℕ) : Type

Syntax for a finite group presentation with exactly n generator slots and exactly m relator slots.

• relator : Fin m → Word n

  The indexed list of relator words in a finite group presentation.

def Undecidability.FP.relSet {n m : ℕ} (P : FP n m) : Set (FreeGroup (Fin n))

The relators of a finite presentation, interpreted in the free group.

Equations

• P.relSet = Set.range fun (i : Fin m) => FreeGroup.mk (P.relator i)

@[reducible, inline]

abbrev Undecidability.FP.Group {n m : ℕ} (P : FP n m) : Type

The group defined by a finite presentation.

Equations

• P.Group = PresentedGroup P.relSet

def Undecidability.FP.wordProblem {n m : ℕ} (P : FP n m) (w : Word n) : Prop

The word problem for a finite presentation.

Equations

• P.wordProblem w = ((PresentedGroup.mk P.relSet) (FreeGroup.mk w) = 1)

def Undecidability.FP.evalWord {n m : ℕ} (P : FP n m) (w : Word n) : P.Group

Evaluate a word in the group defined by a presentation.

Equations

• P.evalWord w = Undecidability.Word.eval (fun (i : Fin n) => PresentedGroup.of i) w

theorem Undecidability.FP.evalWord_eq_mk {n m : ℕ} (P : FP n m) (w : Word n) : P.evalWord w = (PresentedGroup.mk P.relSet) (FreeGroup.mk w)

theorem Undecidability.FP.wordProblem_iff_evalWord_eq_one {n m : ℕ} (P : FP n m) (w : Word n) : P.wordProblem w ↔ P.evalWord w = 1

theorem Undecidability.FP.relator_eq_one {n m : ℕ} (P : FP n m) (i : Fin m) : P.evalWord (P.relator i) = 1

Every designated relator evaluates to one in the presented group.

def Undecidability.FP.homOfRelators {n m : ℕ} {G : Type u_1} [_root_.Group G] (P : FP n m) (x : Fin n → G) (h : ∀ (i : Fin m), Word.eval x (P.relator i) = 1) : P.Group →* G

Map a presented group by choosing images of its generators and proving that the designated relators hold.

Equations

• P.homOfRelators x h = PresentedGroup.toGroup ⋯

@[simp]

theorem Undecidability.FP.homOfRelators_of {n m : ℕ} {G : Type u_1} [_root_.Group G] (P : FP n m) (x : Fin n → G) (h : ∀ (i : Fin m), Word.eval x (P.relator i) = 1) (i : Fin n) : (P.homOfRelators x h) (PresentedGroup.of i) = x i

@[simp]

theorem Undecidability.FP.homOfRelators_evalWord {n m : ℕ} {G : Type u_1} [_root_.Group G] (P : FP n m) (x : Fin n → G) (h : ∀ (i : Fin m), Word.eval x (P.relator i) = 1) (w : Word n) : (P.homOfRelators x h) (P.evalWord w) = Word.eval x w

def Undecidability.FP.presentsTrivial {n m : ℕ} (P : FP n m) : Prop

A presentation presents the trivial group when every word represents 1.

Equations

• P.presentsTrivial = ∀ (w : Undecidability.Word n), P.wordProblem w

def Undecidability.FP.NormallyGenerates {n m : ℕ} (P : FP n m) (z : Word n) : Prop

A word normally generates the group defined by P.

Equations

• P.NormallyGenerates z = (Subgroup.normalClosure {(PresentedGroup.mk P.relSet) (FreeGroup.mk z)} = ⊤)

theorem Undecidability.FP.presentsTrivial_iff_subsingleton {n m : ℕ} (P : FP n m) : P.presentsTrivial ↔ Subsingleton P.Group

theorem Undecidability.FP.presentsTrivial_of_generator_eq_one {n m : ℕ} (P : FP n m) (h : ∀ (i : Fin n), PresentedGroup.of i = 1) : P.presentsTrivial

A finite presentation is trivial when all of its canonical generators are equal to one.

def Undecidability.FP.Effective {n m : ℕ} (A : ℕ → FP n m) : Prop

A family of finite presentations is effective when one algorithm computes the ith relator of the jth presentation from j and i.

Equations

• Undecidability.FP.Effective A = Computable₂ fun (j : ℕ) (i : Fin m) => (A j).relator i

def Undecidability.FP.IsAdianRabinFamily {n m : ℕ} (A : ℕ → FP n m) : Prop

An effective Adian--Rabin family for triviality: there is no algorithm deciding which member of the family presents the trivial group.

Equations

• Undecidability.FP.IsAdianRabinFamily A = (Undecidability.FP.Effective A ∧ ¬ComputablePred fun (j : ℕ) => (A j).presentsTrivial)