Automorphisms of free groups

The groups Aut(F_n) and Out(F_n): fixed points and fixed subgroups of automorphisms, word problem, automaticity, linearity of IA-automorphisms, embeddings of free products into Aut(F_n).

AbbreviationOuter automorphism group of a free group#✓fully proved

For a natural number \(n\), let \(F_n\) be the free group on \(n\) generators. Its outer automorphism group \(\mathrm{Out}(F_n)\) is the quotient of the automorphism group \(\mathrm{Aut}(F_n)\) by the normal subgroup generated by the inner automorphisms. Since the inner automorphisms already form a normal subgroup \(\mathrm{Inn}(F_n)\), this is \(\mathrm{Aut}(F_n) / \mathrm{Inn}(F_n)\).

abbrev OutFreeGroup (n : ℕ) : Type :=
  MulAut (FreeGroup (Fin n)) ⧸ Subgroup.normalClosure
    (Set.range (MulAut.conj : FreeGroup (Fin n) →* MulAut (FreeGroup (Fin n))))

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.