CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Frobenius semidirect product decomposition

Statement

Let $G$ be a finite Frobenius group with complement $H$ and kernel set $N = (G ∖ ⋃_{x \in G} x H x^{- 1}) \cup {1}$ . Then $G$ is the internal semidirect product $G = N ⋊ H$ , that is $N ⊴ G$ , $G = N H$ and $N \cap H = {1}$ ; moreover $∣ N ∣ = [G : H]$ , and $N$ is the unique normal subgroup $M ⊴ G$ with $M H = G$ and $M \cap H = {1}$ .

Facts & Assumptions

Given: A finite group $G$ with Frobenius complement ${1} < H < G$ , and the kernel set $N$ of Frobenius kernel set.

[F1]

$N ⊴ G$ (Frobenius kernel theorem).

[F2]

$∣ N ∣ = [G : H]$ and $N \cap H = {1}$ (Frobenius kernel cardinality).

[F3]

$N$ consists of $1$ and the elements lying in no conjugate of $H$ (Frobenius kernel set).

[F4]

If $H \leq G$ and $N ⊴ G$ then $H N$ is a subgroup of $G$ (If $H \leq G$ and $N ⊴ G$ , then $H N$ is a subgroup and $H \cap N ⊴ H$ ).

[F5]

If $N ⊴ G$ and $H \leq G$ then $H / (H \cap N) ≅ H N / N$ , hence $∣ H N ∣ ∣ H \cap N ∣ = ∣ H ∣ ∣ N ∣$ (Second isomorphism theorem for groups: $H / (H \cap N) ≅ H N / N$ , Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

[F6]

$∣ G ∣ = [G : H] ∣ H ∣$ (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

[F7]

$G$ is the internal semidirect product of $N$ by $H$ exactly when $N ⊴ G$ , $G = N H$ and $N \cap H = {1}$ (An internal semidirect product and a complement to a normal subgroup).

[F8]

If $M ⊴ G$ then $x M x^{- 1} = M$ for every $x \in G$ , so $M \cap x H x^{- 1} = x (x^{- 1} M x \cap H) x^{- 1} = x (M \cap H) x^{- 1}$ (Normal subgroup: invariance under conjugation).

[F9]

If $M ⊴ G$ , $M H = G$ and $M \cap H = {1}$ then every $g \in G$ has a unique expression $g = m h$ with $m \in M$ , $h \in H$ : from $m h = m^{'} h^{'}$ one gets $m^{' - 1} m = h^{'} h^{- 1} \in M \cap H = {1}$ (Subgroup).

Proof

technique · direct

1.1

$N H$ is a subgroup of $G$ , since $N ⊴ G$ and $H \leq G$ ; its order satisfies $∣ N H ∣ ∣ N \cap H ∣ = ∣ N ∣ ∣ H ∣$ by the second isomorphism theorem together with Lagrange.

F1F4F5

1.2

For uniqueness, let $M ⊴ G$ satisfy $M H = G$ and $M \cap H = {1}$ . By [F8], $M \cap x H x^{- 1} = x (M \cap H) x^{- 1} = {1}$ for every $x \in G$ , so no nonidentity element of $M$ lies in a conjugate of $H$ ; hence $M \subseteq N$ by the description [F3] of $N$ .

F3F8assume-hyp

2.1

Since $N \cap H = {1}$ , step 1.1 gives $∣ N H ∣ = ∣ N ∣ ∣ H ∣ = [G : H] ∣ H ∣ = ∣ G ∣$ by [F2] and [F6]; as $N H \subseteq G$ is a subgroup with as many elements as $G$ , it equals $G$ .

F2F6step 1.1algebra

3.1

Together with $N ⊴ G$ of [F1] and $N \cap H = {1}$ of [F2], step 2.1 exhibits $G$ as the internal semidirect product $N ⋊ H$ in the sense of [F7], and $∣ N ∣ = [G : H]$ is [F2].

F1F2F7step 2.1

4.1

Since $M \cap H = {1}$ and $M H = G$ , the uniqueness of the expression $g = m h$ of [F9] applies with $M$ in place of $N$ and gives $∣ G ∣ = ∣ M ∣ ∣ H ∣$ , so $∣ M ∣ = ∣ G ∣ / ∣ H ∣ = [G : H] = ∣ N ∣$ by [F2] and [F6]; with $M \subseteq N$ from step 1.2 this forces $M = N$ . ∎

F2F6F9step 1.2algebra

Depends on

Used by

Affine linear Frobenius groups over finite fields Example
S₃ as a Frobenius group Example
Frobenius groups and fixed point free actions Proposition

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Alex Bartel, Introduction to Representation Theory of Finite Groups, §6.1 (standard reference, not scraped)