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.

Every transitive $G$ -set is equivariantly isomorphic to $G/G_x$ for any chosen point $x$

Statement

Let $X$ be a transitive $G$ -set and choose $x\in X$ . Then the orbit map

$G/G_x\longrightarrow X,\qquad gG_x\longmapsto g\cdot x,$

is an equivariant isomorphism from the left-coset action on $G/G_x$ to the given action on $X$ .

Facts & Assumptions

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

[L1]

An isomorphism of $G$ -sets is an equivariant bijection (Equivariant maps and isomorphisms of group actions).

[L2]

Transitivity means that for every $y\in X$ there is $g\in G$ with $g\cdot x=y$ (Left group actions, transitive actions, and faithful actions).

[L3]

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

[L4]

The left-coset action is $a\cdot(gG_x)=(ag)G_x$ (Left multiplication on $G/H$ is transitive, has stabiliser $H$ at $H$ , and has kernel $\operatorname{Core}_G(H)$ ).

Proof

technique · constructive

1.1

Define $\Phi(gG_x)=g\cdot x$ . By [L3], this is a bijection from $G/G_x$ onto $G\cdot x$ .

L1L3construct

2.1

For $a,g\in G$ , one has $\Phi(a\cdot(gG_x))=\Phi((ag)G_x)=(ag)\cdot x=a\cdot(g\cdot x)=a\cdot\Phi(gG_x)$ , so $\Phi$ is equivariant.

step 1.1L1L4

3.1

By transitivity [L2], $G\cdot x=X$ . Thus $\Phi:G/G_x\to X$ is an equivariant bijection and hence an isomorphism of $G$ -sets.

step 1.1step 2.1L1L2discharge-construct∎

Depends on

Used by

A transitive action is faithful exactly when a point stabiliser is core-free Corollary

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 41 results over 16 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, Lemma 3.105 and Theorem 3.107 (standard reference, not scraped)

Every transitive GGG-set is equivariantly isomorphic to G/GxG/G_xG/Gx​ for any chosen point xxx