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.

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} ⟶ X, g G_{x} ⟼ 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$ , $g G_{x} \mapsto g \cdot x$ , is a bijection (Orbit-stabiliser: $G / G_{x} \to G \cdot x$ , $g G_{x} \mapsto g \cdot x$ , is a well-defined bijection).

[L4]

The left-coset action is $a \cdot (g G_{x}) = (a g) G_{x}$ (Left multiplication on $G / H$ is transitive, has stabiliser $H$ at $H$ , and has kernel ${Core}_{G} (H)$ ).

Proof

technique · constructive

1.1

Define $Φ (g G_{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 $Φ (a \cdot (g G_{x})) = Φ ((a g) G_{x}) = (a g) \cdot x = a \cdot (g \cdot x) = a \cdot Φ (g G_{x})$ , so $Φ$ is equivariant.

step 1.1L1L4

3.1

By transitivity [L2], $G \cdot x = X$ . Thus $Φ : 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 · two levels

16 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

P. Brosnan, Undergraduate Algebra Notes, 3.14: G-Sets, Lemma 3.105 and Theorem 3.107 (standard reference, not scraped)

Every transitive GG-set is equivariantly isomorphic to G/GxG/Gx​ for any chosen point xx