Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 GG on XX correspond exactly to homomorphisms G→Sym⁡(X)G\to\operatorname{Sym}(X)

Statement

For groups GG and a set XX, left actions of GG on XX are in bijection with group homomorphisms ρ:G→Sym⁡(X)\rho:G\to\operatorname{Sym}(X). The action attached to ρ\rho is g⋅x:=ρ(g)(x)g\cdot x:=\rho(g)(x); the homomorphism attached to an action sends gg to the permutation x↦g⋅xx\mapsto g\cdot x.

Facts & Assumptions

Given: A group GG with identity ee and a set XX.

[L1]

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

[L2]

Sym⁡(X)\operatorname{Sym}(X) is the group of bijections X→XX\to X under composition (The symmetric group Sym⁡(X)\operatorname{Sym}(X): the bijections of a set XX under composition, Sym⁡(X)\operatorname{Sym}(X) is a group under composition, and it is non-abelian whenever XX 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′f(e) = e' and f(g−1)=f(g)−1f(g^{-1}) = f(g)^{-1}, and f(gn)=f(g)nf(g^{n}) = f(g)^{n} for every n∈Zn \in \mathbb{Z}; for monoid homomorphisms preservation of the identity must be assumed).

Proof

technique · direct
1.1

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

L1givenalgebra
1.2

Conversely, let ρ:G→Sym⁡(X)\rho:G\to\operatorname{Sym}(X) be a homomorphism and set g⋅x=ρ(g)(x)g\cdot x=\rho(g)(x). Then e⋅x=ρ(e)(x)=xe\cdot x=\rho(e)(x)=x, and (gh)⋅x=ρ(g)(ρ(h)(x))=g⋅(h⋅x)(gh)\cdot x=\rho(g)(\rho(h)(x))=g\cdot(h\cdot x).

L2L3given
2.1

The action law gives ρ(gh)(x)=g⋅(h⋅x)=(ρ(g)∘ρ(h))(x)\rho(gh)(x)=g\cdot(h\cdot x)=(\rho(g)\circ\rho(h))(x) for every xx; thus ρ(gh)=ρ(g)∘ρ(h)\rho(gh)=\rho(g)\circ\rho(h), so ρ\rho is a homomorphism into Sym⁡(X)\operatorname{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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 47 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