Free products in automorphism groups of free groups

DefinitionBardakov's question on free products in \(\mathrm{Aut}(F_n)\) (Kourovka 18.11)#✓fully proved

The statement that for every natural number \(n \ge 2\) and all subgroups \(G\) and \(H\) of the automorphism group \(\mathrm{Aut}(F_n)\) of the free group \(F_n\) of rank \(n\), there are a natural number \(m\) and an injective group homomorphism from the free product \(G \ast H\) to \(\mathrm{Aut}(F_m)\).

def freeProductAutFreeGroupEmbeds : Prop :=
  ∀ n : ℕ, 2 ≤ n → ∀ G H : Subgroup (MulAut (FreeGroup (Fin n))),
    ∃ (m : ℕ) (f : Monoid.Coprod G H →* MulAut (FreeGroup (Fin m))), Function.Injective f
Used by 1

TheoremFree products of subgroups of \(\mathrm{Aut}(F_n)\) embed in some \(\mathrm{Aut}(F_m)\)#●ready to prove

For every natural number \(n \ge 2\) and all subgroups \(G\) and \(H\) of the automorphism group \(\mathrm{Aut}(F_n)\) of the free group \(F_n\) of rank \(n\), there are a natural number \(m\) and an injective group homomorphism from the free product \(G \ast H\) to \(\mathrm{Aut}(F_m)\).

Jayadevan constructs, for subgroups \(G \le \mathrm{Aut}(F_n)\) and \(H \le \mathrm{Aut}(F_k)\) with no finite-generation hypothesis, an embedding of \(G \ast H\) in \(\mathrm{Aut}(F_{n+k+3})\); the Kourovka Notebook (21st issue) answers 18.11 "Yes, it is true" (AI solution confirmed by V. G. Bardakov).

public theorem_wanted freeProductAutFreeGroupEmbeds_holds : freeProductAutFreeGroupEmbeds
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 18.11 (V. G. Bardakov); resolution: A. Jayadevan, Free products of free-group automorphism groups: a finite-rank embedding by separating cocycles, preprint, Zenodo record 22722085 (2026), abstract (for G ≤ Aut(F_n), H ≤ Aut(F_m), G ∗ H embeds in Aut(F_{n+m+3}); no finite-generation hypothesis); the Kourovka Notebook (21st issue) marks 18.11 solved (Yes, it is true; AI solution confirmed by V. G. Bardakov), https://zenodo.org/records/22722085.
Uses 1
1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.