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
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
WantedExt/GroupTheory/OuterAutomorphismGroupRealizationKourovka16Problem59Wanted.lean:40
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
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
def OutIsoTo (M G : Type*) [Group M] [Group G] : Prop :=
∃ φ : MulAut M →* G, Function.Surjective φ ∧ φ.ker = (MulAut.conj (G := M)).range
WantedExt/GroupTheory/OuterAutomorphismMetabelianKourovka11Problem26Wanted.lean:37
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
def groupNotOuterAutOfMetabelian : Prop :=
∃ (G : Type) (_ : Group G), ∀ (M : Type) [Group M], derivedSeries M 2 = ⊥ →
Subgroup.center M = ⊥ → ¬ OutIsoTo M G
WantedExt/GroupTheory/OuterAutomorphismMetabelianKourovka11Problem26Wanted.lean:42
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
Gthere is a metabelian groupMwith trivial center such thatOut M ≅ G", https://arxiv.org/abs/1401.0300v49.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.