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
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
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
WantedExt/GroupTheory/FreeProductAutFreeGroupEmbeddingKourovka18Problem11Wanted.lean:39
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.