TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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$ , $g G_{x} \mapsto g \cdot x$ , is a well-defined bijection

Statement

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

$Φ : G / G_{x} ⟶ G \cdot x, Φ (g G_{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 \leq G$ , the left coset represented by $g$ is $g H = {g h : h \in H}$ (Left and right cosets $g H$ and $H g$ of a subgroup).

[L4]

For $H \leq G$ , one has $g H = h H$ exactly when $g^{- 1} h \in H$ ( $x \in a H$ iff $a^{- 1} x \in H$ , and $a H = b H$ 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.1L1L2L3L4L5construct

Define $Φ (g G_{x}) = g \cdot x$ . If $g G_{x} = h G_{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 $Φ$ is well-defined.

2.1step 1.1L1

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

3.1step 1.1L1L4L5discharge-construct∎

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

Orbit-stabiliser: $G / G_{x} \to G \cdot x$ , $g G_{x} \mapsto g \cdot x$ , is a well-defined bijection

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Orbit-stabiliser: G/Gx→G⋅xG/Gx​→G⋅x, gGx↦g⋅xgGx​↦g⋅x, is a well-defined bijection

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Orbit-stabiliser: $G / G_{x} \to G \cdot x$ , $g G_{x} \mapsto g \cdot x$ , is a well-defined bijection