WordProblem.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

Effective finite presentations, decidable word problem in simple groups, and the reverse implication.

def OAI.FiniteAlgebraicEnvelopes.WordProblem.reduceStep line 17
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.reduceStep_primrec line 21
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.reduce_primrec line 37
abbrev OAI.FiniteAlgebraicEnvelopes.WordProblem.Factor line 45
Source documentation
A finite product of signed conjugates is a certificate for normal closure.
```
abbrev Factor (n m : ℕ) := Word n × Fin m × Bool
```
abbrev OAI.FiniteAlgebraicEnvelopes.WordProblem.Certificate line 46
def OAI.FiniteAlgebraicEnvelopes.WordProblem.factorWord line 48
def OAI.FiniteAlgebraicEnvelopes.WordProblem.certificateWord line 52
def OAI.FiniteAlgebraicEnvelopes.WordProblem.factorValue line 55
def OAI.FiniteAlgebraicEnvelopes.WordProblem.certificateValue line 59
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.mk_factorWord line 62
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.mk_certificateWord line 67
def OAI.FiniteAlgebraicEnvelopes.WordProblem.flipFactor line 76
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.factorValue_flip line 78
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.certificateValue_inv line 83
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.certificateValue_mem line 88
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.mem_normalClosure_iff_certificate line 99
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.invRev_primrec line 117
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.factorWord_primrec line 124
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.certificateWord_primrec line 136
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.verifies_primrec line 143
Source documentation
The certificate verifier is primitive recursive, including free reduction.
```
theorem verifies_primrec (n m : ℕ) : PrimrecPred
    (fun p : (Fin m → Word n) × Word n × Certificate n m =>
      certificateValue p.1 p.2.2 = FreeGroup.mk p.2.1) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.WordProblem.Certificate, OAI.FiniteAlgebraicEnvelopes.WordProblem.certificateValue

theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.re_exists line 155

Source documentation

Unbounded search over encoded certificates gives a genuine semidecision.

theorem re_exists {α β : Type*} [Primcodable α] [Primcodable β]
    {p : α × β → Prop} (hp : ComputablePred p) : REPred (fun a => ∃ b, p (a,b)) := by
…

theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.normalClosure_re line 178

Source documentation

Normal closure of any finite tuple of formal relators is uniformly r.e.

theorem normalClosure_re (n m : ℕ) : REPred
    (fun p : (Fin m → Word n) × Word n =>
      FreeGroup.mk p.2 ∈ Subgroup.normalClosure (Set.range fun i => FreeGroup.mk (p.1 i))) := by
…

theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.consRelators_primrec line 188
Source documentation
Add one relator, uniformly effectively in that relator.
```
theorem consRelators_primrec {n m} (r : Fin m → Word n) :
    Primrec (fun w : Word n => Fin.cons (α := fun _ : Fin (m+1) => Word n) w r) := by
…
```

theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.nontrivial_iff_normalClosure line 200

Source documentation

In a simple quotient, adjoining a nontrivial word to the defining relators kills every element, while adjoining a trivial word changes nothing.

theorem nontrivial_iff_normalClosure {H : Type*} [Group H] [IsSimpleGroup H]
    {n m} (φ : FreeGroup (Fin n) →* H) (hφ : Function.Surjective φ)
    (r : Fin m → Word n)
    (hr : Subgroup.normalClosure (Set.range fun i => FreeGroup.mk (r i)) = φ.ker)
    (v : Word n) (hv : φ (FreeGroup.mk v) ≠ 1) (w : Word n) :
    φ (FreeGroup.mk w) ≠ 1 ↔
      FreeGroup.mk v ∈ Subgroup.normalClosure
        (Set.range fun i => FreeGroup.mk (Fin.cons (α := fun _ : Fin (m+1) => Word n) w r i)) := by
…

theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.simple_presentation_computable line 242

Source documentation

Parallel enumeration of the two normal-closure certificates decides equality.

theorem simple_presentation_computable {H : Type*} [Group H] [IsSimpleGroup H]
    {n m} (φ : FreeGroup (Fin n) →* H) (hφ : Function.Surjective φ)
    (r : Fin m → Word n)
    (hr : Subgroup.normalClosure (Set.range fun i => FreeGroup.mk (r i)) = φ.ker) :
    ComputablePred (fun w : Word n => φ (FreeGroup.mk w) = 1) := by
…

theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.evalWord_eq_lift line 263
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.hom_mk_eval line 271
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.finitelyPresentedSimple_wordProblem line 277
Source documentation
The classical converse in Theorem 1.1, for the ambient simple group.
```
theorem finitelyPresentedSimple_wordProblem (H : Type*) [Group H]
    [Group.IsFinitelyPresented H] [IsSimpleGroup H] : HasDecidableWordProblem H := by
…
```
def OAI.FiniteAlgebraicEnvelopes.WordProblem.substitute line 302
Source documentation
Effective replacement of each generator by a fixed finite word.
```
def substitute {n m} (r : Fin n → Word m) (w : Word n) : Word m :=
…
```
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.substitute_primrec line 305
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.evalWord_append line 314
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.evalWord_invRev line 318
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.evalWord_substitute line 322
theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.evalWord_map line 336

theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.wordProblem_of_injective line 345

Source documentation

Word problem descends along embeddings of finitely generated groups.

theorem wordProblem_of_injective {G H : Type*} [Group G] [Group H] [Group.FG G]
    (f : G →* H) (hf : Function.Injective f) (hH : HasDecidableWordProblem H) :
    HasDecidableWordProblem G := by
…

theorem OAI.FiniteAlgebraicEnvelopes.main_reverse line 377

Source documentation

The complete reverse implication of the main theorem.

theorem main_reverse (G : Type u) [Group G] [Group.FG G]
    (hG : EmbedsInFinitelyPresentedSimpleGroup G) : HasDecidableWordProblem G := by
…