LemmaStatement: 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 kernel is an intersection of character kernels

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}$ . For every nontrivial irreducible complex character $φ$ of $H$ let $\tilde{φ}$ be its extension, and put $I : = {φ \in Irr (H) : φ \neq 1_{H}}, M : = ⋂_{φ \in I} \ker \tilde{φ},$ where $\ker \tilde{φ} = {g \in G : \tilde{φ} (g) = \tilde{φ} (1)}$ . Then $I$ is nonempty and $N = M$ .

Facts & Assumptions

Given: A finite group $G$ with Frobenius complement ${1} < H < G$ , the kernel set $N$ of Frobenius kernel set, and the family $I$ of nontrivial irreducible complex characters of $H$ with extensions $\tilde{φ}$ .

[F1]

$N$ consists of $1$ and the elements of $G$ that lie in no conjugate $x H x^{- 1}$ of $H$ (Frobenius kernel set).

[F2]

For each $φ \in I$ the class function $\tilde{φ}$ satisfies $\tilde{φ} ∣_{H} = φ$ , $\tilde{φ} (1) = φ (1)$ and $\tilde{φ} (g) = φ (1)$ for every $g \in G$ lying in no conjugate of $H$ (Frobenius character extension construction).

[F3]

For each $φ \in I$ the class function $\tilde{φ}$ is an irreducible complex character of $G$ (Frobenius character extension is irreducible).

[F4]

For a finite-dimensional complex representation $ρ$ with character $χ$ one has $\ker χ = \ker ρ$ , and $\ker ρ$ is a normal subgroup of $G$ ; in particular $\ker \tilde{φ}$ is a normal subgroup of $G$ for each $φ \in I$ (The kernel of a complex character agrees with the kernel of any representation affording it).

[F5]

The intersection of a nonempty family of normal subgroups of $G$ is a normal subgroup of $G$ (The intersection of a nonempty family of normal subgroups is normal).

[F6]

For a finite group $H$ , a subgroup $N_{0} \leq H$ is normal if and only if it is an intersection of kernels of irreducible complex characters of $H$ ; applying this to $N_{0} = {1}$ gives $⋂_{ψ \in Irr (H)} \ker ψ = {1}$ , since the intersection over all irreducible characters is contained in any such sub-intersection (The normal subgroups of a finite group are exactly the intersections of kernels of irreducible complex characters).

[F7]

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

Proof

technique · direct

1.1

The family $I$ is nonempty: if $Irr (H) = {1_{H}}$ were a singleton, then [F6] would give ${1} = ⋂_{ψ \in Irr (H)} \ker ψ = \ker 1_{H} = H$ , contradicting ${1} < H$ ; hence there is an irreducible character of $H$ different from $1_{H}$ .

F6given

1.2

$N \subseteq M$ : let $g \in N$ . If $g = 1$ then $\tilde{φ} (1) = \tilde{φ} (1)$ for every $φ$ , so $g \in \ker \tilde{φ}$ for all $φ \in I$ . If $g \neq 1$ then by [F1] the element $g$ lies in no conjugate of $H$ , so [F2] gives $\tilde{φ} (g) = φ (1) = \tilde{φ} (1)$ for every $φ \in I$ , that is $g \in \ker \tilde{φ}$ for every such $φ$ .

F1F2cases

1.3

$M \cap H = {1}$ : if $h \in M \cap H$ then for every $φ \in I$ one has $φ (h) = \tilde{φ} (h) = \tilde{φ} (1) = φ (1)$ by [F2], so $h \in \ker φ$ , and $h \in \ker 1_{H}$ holds trivially as well; hence $h \in ⋂_{ψ \in Irr (H)} \ker ψ = {1}$ by [F6].

F2F6algebra

1.4

Every normal subgroup $M^{'}$ of $G$ with $M^{'} \cap H = {1}$ satisfies $M^{'} \subseteq N$ : for $x \in G$ one has $M^{'} \cap x H x^{- 1} = x (x^{- 1} M^{'} x \cap H) x^{- 1} = x (M^{'} \cap H) x^{- 1} = {1}$ by [F7], so each nonidentity element of $M^{'}$ lies in no conjugate of $H$ and therefore belongs to $N$ by [F1].

F1F7algebra

2.1

By [F3] each $\tilde{φ}$ with $φ \in I$ is an irreducible character, so by [F4] each $\ker \tilde{φ}$ is a normal subgroup of $G$ ; since $I$ is nonempty by step 1.1, [F5] makes $M$ a normal subgroup of $G$ .

F3F4F5step 1.1

3.1

Applying step 1.4 to the normal subgroup $M$ of step 2.1, whose intersection with $H$ is trivial by step 1.3, yields $M \subseteq N$ ; together with step 1.2 this gives $N = M$ , as claimed. ∎

step 1.2step 2.1step 1.3step 1.4

Depends on

Used by

Frobenius kernel theorem Theorem

Dependency tree · two levels

33 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)