Linearity of IA-automorphism groups

DefinitionIA-automorphisms of a free group#✓fully proved

For a natural number \(n\), let \(F_n\) be the free group on \(n\) generators. \(\mathrm{IA}(F_n)\) is the subgroup of the automorphism group of \(F_n\) consisting of the automorphisms \(\varphi\) that act trivially on the abelianization \(F_n/[F_n, F_n]\), that is, such that \(\varphi(x)\) and \(x\) have the same image in \(F_n/[F_n, F_n]\) for every \(x \in F_n\).

def iaAut (n : ℕ) : Subgroup (MulAut (FreeGroup (Fin n))) where
  carrier := {φ | ∀ x, Abelianization.of (φ x) = Abelianization.of x}
  one_mem' _ := rfl
  mul_mem' {φ ψ} hφ hψ x := (hφ (ψ x)).trans (hψ x)
  inv_mem' {φ} hφ x := by
    have h := hφ (φ⁻¹ x)
    simp only [MulAut.apply_inv_self] at h
    exact h.symm

Used by 1

Used byKourovka Problem 15.10 (statement): linearity of IA-automorphism groups of free groups

DefinitionKourovka Problem 15.10 (statement): linearity of IA-automorphism groups of free groups#✓fully proved

The statement that for some \(n \ge 3\) the group \(\mathrm{IA}(F_n)\) of automorphisms of the free group \(F_n\) on \(n\) generators that act trivially on its abelianization \(F_n/[F_n, F_n]\) is linear, that is, there are a field \(K\), a natural number \(m\) and an injective group homomorphism \(\mathrm{IA}(F_n) \to \mathrm{GL}_m(K)\).

def iaAutLinear : Prop :=
  ∃ n : ℕ, 3 ≤ n ∧ ∃ (K : Type) (_ : Field K) (m : ℕ)
    (ρ : iaAut n →* Matrix.GeneralLinearGroup (Fin m) K), Function.Injective ρ

Uses 1 · Used by 1

Statement usesIA-automorphisms of a free group

Used byIA-automorphism group of a free group is not linear

TheoremIA-automorphism group of a free group is not linear#●ready to prove

Resolved false: the Kourovka Archive answers 15.10 No: IA(Fₙ) is not linear for n ≥ 5 (Pettet) and for every n ≥ 3 (Bardakov and Mikhailov). Source: E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 15.10 (Yu. I. Merzlyakov; V. G. Bardakov); resolution: V. G. Bardakov and R. Mikhailov, Commun. Algebra 36 (2008), no. 4, 1489-1499 (n ≥ 3); A. Pettet, Cohomology of some subgroups of the automorphism group of a free group, Ph.D. thesis, 2006 (n ≥ 5), Kourovka Archive, Problem 15.10.

public theorem_wanted iaAutLinear_refuted : ¬ iaAutLinear

Uses 1

Statement usesKourovka Problem 15.10 (statement): linearity of IA-automorphism groups of free groups

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.