PropositionStatement: 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 permutation action characterization

Statement

Let $G$ be a finite group and let ${1} < H < G$ be a subgroup. Then $H$ is a Frobenius complement of $G$ if and only if the left action of $G$ on the coset space $G / H$ by left multiplication is transitive, is nonregular (that is, not free), and every nonidentity element of $G$ fixes at most one coset.

Facts & Assumptions

Given: A finite group $G$ , a subgroup ${1} < H < G$ , and the rule $g \cdot x H : = g x H$ for $g, x \in G$ .

[F1]

A left action of $G$ on a set $X$ is a map $G \times X \to X$ with $e \cdot x = x$ and $(g h) \cdot x = g \cdot (h \cdot x)$ for all $g, h \in G$ , $x \in X$ ; the action is transitive when some element of $G$ carries any given point to any other (Left group actions, transitive actions, and faithful actions).

[F2]

For $g \in G$ the left coset is $g H = {g h : h \in H}$ , and $g H = x H$ holds exactly when $x \in g H$ (Left and right cosets $g H$ and $H g$ of a subgroup).

[F3]

The orbit and stabilizer of a point $x$ of a $G$ -set $X$ are $G \cdot x = {g \cdot x : g \in G}$ and $G_{x} = {g \in G : g \cdot x = x}$ ; the stabilizer is a subgroup (The orbit $G \cdot x$ and stabilizer $G_{x}$ of a point in a group action).

[F4]

An action is free when $g \cdot x = x$ implies $g = e$ for all $g \in G$ and all $x \in X$ ; equivalently, no nonidentity element fixes any point (A free group action has no nonidentity element fixing a point).

[F5]

For $g \in G$ the fixed-point set is $X^{g} = {x \in X : g \cdot x = x}$ ; writing "an element fixes at most one coset" means $∣ (G / H)^{g} ∣ \leq 1$ for every $g \neq 1$ (The fixed-point sets $X^{g}$ and $X^{G}$ of a group action).

[F6]

A subgroup ${1} < H < G$ is a Frobenius complement exactly when $H \cap g H g^{- 1} = {1}$ for every $g \notin H$ (Frobenius complement and frobenius group).

[F7]

Every orbit of a $G$ -set is in bijection with the left cosets of the stabilizer of a point of it, by $g G_{x} \mapsto g \cdot x$ (Orbit-stabiliser: $G / G_{x} \to G \cdot x$ , $g G_{x} \mapsto g \cdot x$ , is a well-defined bijection).

[F8]

A subgroup $H \leq G$ contains $e$ , is closed under products, and is closed under inverses (Subgroup).

[F9]

For $a, b \in G$ one has $a H = b H$ if and only if $a^{- 1} b \in H$ , and $x \in a H$ if and only if $a^{- 1} x \in H$ ( $x \in a H$ iff $a^{- 1} x \in H$ , and $a H = b H$ iff $a^{- 1} b \in H$ ).

Proof

technique · direct

1.1F1F2given

The rule $g \cdot x H : = g x H$ defines a left action of $G$ on $G / H$ : $e \cdot x H = x H$ and $(g h) \cdot x H = g h x H = g \cdot (h \cdot x H)$ for all $g, h, x \in G$ , by associativity of the product in $G$ .

2.1F1F2step 1.1algebra

The action of step 1.1 is transitive: given cosets $x H$ and $y H$ , the element $g : = y x^{- 1}$ satisfies $g \cdot x H = y x^{- 1} x H = y H$ .

2.2F2F3F5F8F9step 1.1algebra

For $k \in G$ and a coset $x H$ one has $k \cdot x H = x H$ if and only if $x^{- 1} k x \in H$ : indeed the coset equality $k x H = x H$ is equivalent to $(k x)^{- 1} x = x^{- 1} k^{- 1} x \in H$ by [F9], and $x^{- 1} k^{- 1} x = (x^{- 1} k x)^{- 1}$ is invertible in $H$ exactly when $x^{- 1} k x \in H$ , by [F8], so the displayed criterion follows. Consequently the fixed-point set of $k$ is $(G / H)^{k} = {x H \in G / H : k \in x H x^{- 1}}$ , and $k$ fixes a coset precisely when $k$ lies in the corresponding conjugate $x H x^{- 1}$ of $H$ .

2.3F1F4F8givenchoose

The action of step 1.1 is nonregular whenever ${1} < H$ : choose $h \in H$ with $h \neq 1$ ; then $h \cdot H = H$ , so some nonidentity element fixes a point of $G / H$ and the action is not free. Conversely, if $H = {1}$ then every stabilizer is trivial and the action is free, so nonregularity is exactly the clause ${1} < H$ .

3.1F6F9step 2.2algebra

Suppose $H$ is a Frobenius complement. Let $1 \neq k \in G$ and suppose $k$ fixes two distinct cosets $x H \neq y H$ . By step 2.2 there are $u \in H$ and $v \in H$ with $k = x u x^{- 1} = y v y^{- 1}$ . Then $u = x^{- 1} y v (x^{- 1} y)^{- 1}$ , so $u \in H \cap s H s^{- 1}$ where $s : = x^{- 1} y$ . Since $x H \neq y H$ we have $s = x^{- 1} y \notin H$ by [F9], so [F6] gives $H \cap s H s^{- 1} = {1}$ and $u = 1$ ; hence $k = x u x^{- 1} = 1$ , contradicting $k \neq 1$ . Therefore every nonidentity element fixes at most one coset.

3.2F6F2F9step 2.2assume-hyp

Suppose conversely that every nonidentity element of $G$ fixes at most one coset of $H$ , and let $g \notin H$ and $z \in H \cap g H g^{- 1}$ . By [F6] it suffices to show $z = 1$ . The element $z$ lies in $H$ , so $z \cdot H = H$ ; it also lies in $g H g^{- 1}$ , so $z \cdot g H = g H$ by step 2.2. Since $g \notin H$ the cosets $H$ and $g H$ are distinct by [F9]. Thus the nonidentity element $z$ would fix two distinct cosets, so the hypothesis forces $z = 1$ .

4.1F6F7step 3.1step 3.2step 2.3

Combining the clauses: if $H$ is a Frobenius complement then the action is transitive (step 2.1), nonregular (step 2.3, as ${1} < H$ ), and at most one coset is fixed by each nonidentity element (step 3.1). Conversely, if the action has the three listed properties then the "at most one fixed coset" clause is available and step 3.2 gives $H \cap g H g^{- 1} = {1}$ for every $g \notin H$ , that is, $H$ is a Frobenius complement by [F6]. This proves both directions of the stated equivalence. ∎

Depends on

Used by

A transitive action need not be Frobenius Counterexample
Frobenius kernel set Definition

Dependency tree · two levels

18 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)
Hans Kurzweil and Bernd Stellmacher, The Theory of Finite Groups, §§7.1–7.2 (standard reference, not scraped)