The finitely presented non-sofic group

This file completes the finite-model obstruction and derives the headline existence theorem.

def SoficGroups.ThompsonFFiniteQuotient.conjugateTerm {G : Type u_1} [Group G] (a b : G) (n : ℕ) : G

The conjugate of b by the nth power of a.

Equations

• SoficGroups.ThompsonFFiniteQuotient.conjugateTerm a b n = (a ^ n)⁻¹ * b * a ^ n

theorem SoficGroups.exists_finitelyPresented_nonsofic_group : ∃ (G : Type) (x : Group G), Group.IsFinitelyPresented G ∧ ¬Sofic G

There exists a finitely presented group that is not sofic.