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

Left multiplication on G/HG/H is transitive, has stabiliser HH at HH, and has kernel CoreG(H)\operatorname{Core}_G(H)

Statement

Let HGH\le G. Left multiplication defines a transitive action of GG on the coset set G/HG/H by

g(aH):=(ga)H.g\cdot(aH):=(ga)H.

The stabilizer of the point HH is HH. The corresponding homomorphism ρ:GSym(G/H)\rho:G\to\operatorname{Sym}(G/H) has

kerρ=CoreG(H).\ker\rho=\operatorname{Core}_G(H).

Facts & Assumptions

Given: A group GG and a subgroup HGH\le G.

[L1]

A left action satisfies the identity and multiplication laws and is transitive when some group element carries any chosen point to any other (Left group actions, transitive actions, and faithful actions).

[L2]

Every action yields a homomorphism into the symmetric group of the acted-on set (Actions of GG on XX correspond exactly to homomorphisms GSym(X)G\to\operatorname{Sym}(X)).

[L4]
[L5]

The kernel of a homomorphism consists of the elements mapped to the identity (The kernel and image of a group homomorphism).

[L6]

The core is CoreG(H)=aGaHa1\operatorname{Core}_G(H)=\bigcap_{a\in G}aHa^{-1} (The core CoreG(H)=gGgHg1\operatorname{Core}_G(H)=\bigcap_{g\in G}gHg^{-1} of a subgroup).

Proof

technique · direct
1.1

If aH=bHaH=bH, then a1bHa^{-1}b\in H by [L4], and (ga)1(gb)=a1bH(ga)^{-1}(gb)=a^{-1}b\in H, so (ga)H=(gb)H(ga)H=(gb)H and the rule is well-defined. It satisfies e(aH)=aHe\cdot(aH)=aH and g(k(aH))=(gk)aH=(gk)(aH)g\cdot(k\cdot(aH))=(gk)aH=(gk)\cdot(aH); moreover aH=aHa\cdot H=aH, so the action is transitive, and gH=Hg\cdot H=H exactly when gHg\in H.

L1L3L4
2.1

By [L2], the action defines ρ:GSym(G/H)\rho:G\to\operatorname{Sym}(G/H). By [L5], an element kk lies in kerρ\ker\rho exactly when k(aH)=aHk\cdot(aH)=aH for every aGa\in G, that is, when (ka)H=aH(ka)H=aH for every aa.

step 1.1L2L5
3.1

By [L4], (ka)H=aH(ka)H=aH is equivalent to a1kaHa^{-1}ka\in H, or to kaHa1k\in aHa^{-1}. Requiring this for every aa gives kaaHa1=CoreG(H)k\in\bigcap_a aHa^{-1}=\operatorname{Core}_G(H), so kerρ=CoreG(H)\ker\rho=\operatorname{Core}_G(H), which is normal by [L7].

step 2.1L4L6L7

Depends on

Used by

Dependency tree · next 3 levels

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