TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03

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.

Actions of $G$ on $X$ correspond exactly to homomorphisms $G \to Sym (X)$

Statement

For groups $G$ and a set $X$ , left actions of $G$ on $X$ are in bijection with group homomorphisms $ρ : G \to Sym (X)$ . The action attached to $ρ$ is $g \cdot x : = ρ (g) (x)$ ; the homomorphism attached to an action sends $g$ to the permutation $x \mapsto g \cdot x$ .

Facts & Assumptions

Given: A group $G$ with identity $e$ and a set $X$ .

[L1]

A left action satisfies $e \cdot x = x$ and $(g h) \cdot x = g \cdot (h \cdot x)$ (Left group actions, transitive actions, and faithful actions).

[L2]

$Sym (X)$ is the group of bijections $X \to X$ under composition (The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition, $Sym (X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements).

[L3]

A group homomorphism preserves multiplication and sends the identity to the identity (Monoid homomorphism and group homomorphism, A group homomorphism automatically satisfies $f (e) = e^{'}$ and $f (g^{- 1}) = f (g)^{- 1}$ , and $f (g^{n}) = f (g)^{n}$ for every $n \in Z$ ; for monoid homomorphisms preservation of the identity must be assumed).

Proof

technique · direct

1.1

Given an action, define $ρ (g) (x) = g \cdot x$ . The maps $ρ (g)$ are bijective: $ρ (g^{- 1})$ is a two-sided inverse because the action laws give $g^{- 1} \cdot (g \cdot x) = x = g \cdot (g^{- 1} \cdot x)$ .

L1givenalgebra

1.2

Conversely, let $ρ : G \to Sym (X)$ be a homomorphism and set $g \cdot x = ρ (g) (x)$ . Then $e \cdot x = ρ (e) (x) = x$ , and $(g h) \cdot x = ρ (g) (ρ (h) (x)) = g \cdot (h \cdot x)$ .

L2L3given

2.1

The action law gives $ρ (g h) (x) = g \cdot (h \cdot x) = (ρ (g) \circ ρ (h)) (x)$ for every $x$ ; thus $ρ (g h) = ρ (g) \circ ρ (h)$ , so $ρ$ is a homomorphism into $Sym (X)$ .

step 1.1L1L2L3given

3.1

The two constructions recover their input pointwise, so they are mutually inverse correspondences.

step 2.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

23 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

Brosnan, Group actions (standard reference, not scraped)

Actions of GG on XX correspond exactly to homomorphisms G→Sym⁡(X)G→Sym(X)