Groups as outer automorphism groups

DefinitionKourovka Problem 16.59 (finite groups as outer automorphism groups)#✓fully proved

The statement that for every finite group \(K\) there are a finite group \(G\) and a surjective homomorphism \(\mathrm{Aut}(G) \to K\) whose kernel is the group \(\mathrm{Inn}(G)\) of inner automorphisms of \(G\), that is, \(K\) is isomorphic to \(\mathrm{Out}(G) = \mathrm{Aut}(G) / \mathrm{Inn}(G)\).

def everyFiniteGroupIsOuterAutomorphismGroup : Prop :=
  ∀ (K : Type) [Group K] [Finite K], ∃ (G : Type) (_ : Group G) (_ : Finite G)
    (φ : MulAut G →* K), Function.Surjective φ ∧ φ.ker = (MulAut.conj : G →* MulAut G).range
Used by 1

TheoremEvery finite group is the outer automorphism group of a finite group#●ready to prove

For every finite group \(K\) there are a finite group \(G\) and a surjective homomorphism \(\mathrm{Aut}(G) \to K\) whose kernel is the group \(\mathrm{Inn}(G)\) of inner automorphisms of \(G\); equivalently, \(\mathrm{Out}(G) = \mathrm{Aut}(G) / \mathrm{Inn}(G)\) is isomorphic to \(K\). That is, the answer to Kourovka Problem 16.59 is positive.

The Kourovka Archive records the answer "Yes, it does", citing Cornulier's MathOverflow answer.

public theorem_wanted everyFiniteGroupIsOuterAutomorphismGroup_holds :
    everyFiniteGroupIsOuterAutomorphismGroup
Sources
  • 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 16.59 (D. MacHale); resolution: Y. Cornulier, answer to MathOverflow question 372480 (Is every finite group the outer automorphism group of a finite group?), 2020, Kourovka Archive, Problem 16.59 (Yes, it does), https://mathoverflow.net/questions/372480/is-every-finite-group-the-outer-automorphism-group-of-a-finite-group/372563.
Uses 1

DefinitionOuter automorphism group isomorphic to a given group#✓fully proved

For groups \(M\) and \(G\), the statement that \(\operatorname{Out}(M) \cong G\), expressed without forming the quotient: there is a surjective homomorphism \(\operatorname{Aut}(M) \to G\) whose kernel is exactly the inner automorphism group \(\operatorname{Inn}(M)\), the image of the conjugation map \(M \to \operatorname{Aut}(M)\).

def OutIsoTo (M G : Type*) [Group M] [Group G] : Prop :=
  ∃ φ : MulAut M →* G, Function.Surjective φ ∧ φ.ker = (MulAut.conj (G := M)).range
Used by 1

DefinitionA group that is not an outer automorphism group of a centreless metabelian group#✓fully proved

The statement (Kourovka Problem 11.26, Göbel) that there is a group \(G\) such that for every metabelian group \(M\) (one whose second derived subgroup \(M''\) is trivial) with trivial centre, the outer automorphism group \(\operatorname{Out}(M)\) is not isomorphic to \(G\).

def groupNotOuterAutOfMetabelian : Prop :=
  ∃ (G : Type) (_ : Group G), ∀ (M : Type) [Group M], derivedSeries M 2 = ⊥ →
    Subgroup.center M = ⊥ → ¬ OutIsoTo M G
Uses 1 · Used by 1

TheoremEvery group is the outer automorphism group of a centreless metabelian group#●ready to prove

For every group \(G\) there is a metabelian group \(M\) (one whose second derived subgroup \(M''\) is trivial) with trivial centre such that the outer automorphism group \(\operatorname{Out}(M) = \operatorname{Aut}(M)/\operatorname{Inn}(M)\) is isomorphic to \(G\). This answers Kourovka Problem 11.26 (Göbel) in the negative (Göbel and Paras).

public theorem_wanted groupNotOuterAutOfMetabelian_refuted : ¬ groupNotOuterAutOfMetabelian
Sources
  • 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 11.26 (R. Göbel); resolution: R. Göbel and A. Paras, J. Pure Appl. Algebra 149, no. 3 (2000), 251-266, Kourovka Archive, Problem 11.26: "No, given any group G there is a metabelian group M with trivial center such that Out M ≅ G", https://arxiv.org/abs/1401.0300v49.
Uses 1
3 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.