Presentations and decision problems

Combinatorial group theory: presentations, one-relator groups, HNN extensions and embeddings, SQ-universality, finitely presented simple groups, the word and conjugacy problems (Novikov–Boone, Boone–Higman), Andrews–Curtis moves, generic properties of presentations and torsion quotients.

• Braid and Artin groups
• Andrews–Curtis moves
• Baumslag–Gersten group
• Coherence of one-relator groups
• Decision problems in free abelianized extensions
• Finite quotients of one-relator groups
• Finitely presented soluble groups
• Free subgroups of one-relator groups
• Generic properties of group presentations
• Involutions in quotient groups
• Just finite presentations
• Torsion length of finitely presented groups
• Torsion quotients of finitely presented groups
• Word problem for groups
• Boone–Higman theorem

TheoremHigman–Neumann–Neumann embedding theorem#✓fully proved

Every countable group \(G\) embeds in a group generated by two elements: there are a group \(H\), elements \(a, b \in H\) that generate \(H\), and an injective group homomorphism \(f \colon G \to H\).

theorem higman_neumann_neumann_embedding
    {G : Type u} [Group G] [Countable G] :
    ∃ (H : Type u) (hH : Group H) (a b : H), letI := hH; ∃ (f : G →* H),
      Function.Injective f ∧ Subgroup.closure ({a, b} : Set H) = ⊤

Sources

• G. Higman, B. H. Neumann, H. Neumann, J. London Math. Soc. 24 (1949) 247–254 via HNN extensions; Lean states countable embedding into 2-generator group including finite case.

TheoremInfinite finitely presented simple groups exist#●ready to prove

There exist a natural number \(n\) and a finite set \(R\) of elements of the free group on generators \(x_1, \dots, x_n\) such that the group \(\langle x_1, \dots, x_n \mid R \rangle\) presented by these generators and relators is simple and infinite.

public theorem_wanted higman_infinite_simple :
    ∃ (n : ℕ) (rels : Set (FreeGroup (Fin n))),
      rels.Finite ∧ IsSimpleGroup (PresentedGroup rels) ∧
        Infinite (PresentedGroup rels)

Sources

• G. Higman, 'A finitely generated infinite simple group', J. London Math. Soc. 26 (1951) 61–64; G. Higman, Finitely Presented Infinite Simple Groups, Notes on Pure Mathematics 8, Australian National University, 1974. §122 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem higman_infinite_simple of the lean-eval benchmark.

DefinitionSQ-universal group#✓fully proved

A group \(G\) is SQ-universal if every countable group is isomorphic to a subgroup of a quotient of \(G\): for every countable group \(C\) there are a group \(Q\), a surjective homomorphism \(G \to Q\) and an injective homomorphism \(C \to Q\).

def IsSQUniversal (G : Type*) [Group G] : Prop :=
  ∀ (C : Type) [Group C] [Countable C], ∃ (Q : Type) (_ : Group Q) (q : G →* Q),
    Function.Surjective q ∧ ∃ f : C →* Q, Function.Injective f

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.