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

If y=g⋅xy=g\cdot x, then Gy=gGxg−1G_y=gG_xg^{-1}

Statement

Let GG act on XX. If y=g⋅xy=g\cdot x, then

Gy=gGxg−1.G_y=gG_xg^{-1}.

In particular, stabilizers of points in the same orbit are conjugate and hence isomorphic.

Facts & Assumptions

Given: A left action of GG on XX, points x,y∈Xx,y\in X, and g∈Gg\in G with y=g⋅xy=g\cdot x.

[L1]

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

[L2]

A left action satisfies (ab)⋅z=a⋅(b⋅z)(ab)\cdot z=a\cdot(b\cdot z) and e⋅z=ze\cdot z=z (Left group actions, transitive actions, and faithful actions).

[L3]

Conjugation h↦ghg−1h\mapsto ghg^{-1} is an automorphism of GG (Conjugation x↦gxg−1x\mapsto gxg^{-1} is an automorphism).

Proof

technique · direct
1.1

For h∈Gh\in G, one has h∈Gyh\in G_y exactly when h⋅(g⋅x)=g⋅xh\cdot(g\cdot x)=g\cdot x, which by [L2] is equivalent, after applying g−1g^{-1}, to (g−1hg)⋅x=x(g^{-1}hg)\cdot x=x, that is, to g−1hg∈Gxg^{-1}hg\in G_x.

L1L2L3
2.1

The last condition is equivalent to h∈gGxg−1h\in gG_xg^{-1}, so Gy=gGxg−1G_y=gG_xg^{-1}; [L3] also makes conjugation an isomorphism from GxG_x onto GyG_y.

step 1.1L3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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