TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

Orbit-stabiliser: $G/G_x\to G\cdot x$ , $gG_x\mapsto g\cdot x$ , is a well-defined bijection

Statement

Let $G$ act on $X$ and let $x\in X$ . The rule

$\Phi:G/G_x\longrightarrow G\cdot x,\qquad \Phi(gG_x)=g\cdot x,$

is well-defined and bijective. Thus every orbit is naturally in bijection with the left cosets of its stabilizer.

Facts & Assumptions

Given: A left action of a group $G$ on a set $X$ and a point $x\in X$ .

[L1]

The orbit and stabilizer are $G\cdot x=\{g\cdot x:g\in G\}$ and $G_x=\{g\in G:g\cdot x=x\}$ (The orbit $G\cdot x$ and stabilizer $G_x$ of a point in a group action).

[L2]

The stabilizer $G_x$ is a subgroup of $G$ (The stabilizer $G_x$ is a subgroup of $G$ ).

[L3]

For a subgroup $H\le G$ , the left coset represented by $g$ is $gH=\{gh:h\in H\}$ (Left and right cosets $gH$ and $Hg$ of a subgroup).

[L4]

For $H\le G$ , one has $gH=hH$ exactly when $g^{-1}h\in H$ ( $x\in aH$ iff $a^{-1}x\in H$ , and $aH=bH$ iff $a^{-1}b\in H$ ).

[L5]

A function is bijective exactly when it is injective and surjective (Injection, surjection, bijection).

Proof

technique · constructive

1.1

Define $\Phi(gG_x)=g\cdot x$ . If $gG_x=hG_x$ , then $g^{-1}h\in G_x$ by [L4], so $(g^{-1}h)\cdot x=x$ by [L1], and the action law gives $h\cdot x=g\cdot((g^{-1}h)\cdot x)=g\cdot x$ ; hence $\Phi$ is well-defined.

L1L2L3L4L5construct

2.1

Every $y\in G\cdot x$ has the form $y=g\cdot x=\Phi(gG_x)$ by [L1], so $\Phi$ is surjective.

step 1.1L1

3.1

If $\Phi(gG_x)=\Phi(hG_x)$ , then $g\cdot x=h\cdot x$ , so $(g^{-1}h)\cdot x=x$ and $g^{-1}h\in G_x$ ; [L4] gives $gG_x=hG_x$ , so $\Phi$ is injective and therefore bijective.

step 1.1L1L4L5discharge-construct∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 25 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

P. Brosnan, Undergraduate Algebra Notes, 3.14: G-Sets, Theorem 3.107 (standard reference, not scraped)
T. W. Judson, Abstract Algebra: Theory and Applications, 14.1 (standard reference, not scraped)

Orbit-stabiliser: G/Gx→G⋅xG/G_x\to G\cdot xG/Gx​→G⋅x, gGx↦g⋅xgG_x\mapsto g\cdot xgGx​↦g⋅x, is a well-defined bijection