Alphabeta Math
LemmaStatement: 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.

The stabilizer GxG_x is a subgroup of GG

Statement

For every left action of a group GG on a set XX and every x∈Xx\in X, the stabilizer GxG_x is a subgroup of GG.

Facts & Assumptions

Given: A left action of GG on XX and x∈Xx\in X.

[L1]

Gx={g∈G:g⋅x=x}G_x=\{g\in G:g\cdot x=x\} (The orbit G⋅xG\cdot x and stabilizer GxG_x of a point in a group action).

[L2]

The 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).

[L3]

A nonempty subset HH of a group is a subgroup exactly when ab−1∈Hab^{-1}\in H for all a,b∈Ha,b\in H (One-step subgroup test: a nonempty H⊆GH \subseteq G is a subgroup iff gh−1∈Hgh^{-1} \in H for all g,h∈Hg, h \in H; the identity and the inverses of HH are then those of GG, Subgroup).

Proof

technique · direct
1.1

The identity lies in GxG_x, since e⋅x=xe\cdot x=x. Thus GxG_x is nonempty.

L1L2given
1.2

If a,b∈Gxa,b\in G_x, then (ab−1)⋅x=a⋅(b−1⋅x)=a⋅x=x(ab^{-1})\cdot x=a\cdot(b^{-1}\cdot x)=a\cdot x=x: indeed b⋅x=xb\cdot x=x implies b−1⋅x=b−1⋅(b⋅x)=xb^{-1}\cdot x=b^{-1}\cdot(b\cdot x)=x. Therefore ab−1∈Gxab^{-1}\in G_x.

L1L2givenalgebra
2.1

The subgroup criterion now gives Gx≤GG_x\le G.

step 1.1step 1.2L3∎

Depends on

Used by

Cited to discharge well-definedness by The orbit G· x and stabilizer Gₓ of a point in a group action.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 15 results over 11 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