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.
A transitive action is faithful exactly when a point stabiliser is core-free
Statement
Let act transitively on a nonempty set , and let . The action is faithful if and only if
Equivalently, faithful transitive -sets are precisely the coset actions for core-free subgroups .
Facts & Assumptions
Given: A transitive action of on a nonempty set and a point .
An action is faithful when the only group element fixing every point is the identity (Left group actions, transitive actions, and faithful actions).
The action on is equivariantly isomorphic to the left-coset action on (Every transitive -set is equivariantly isomorphic to for any chosen point ).
The kernel of the action on is (Left multiplication on is transitive, has stabiliser at , and has kernel ).
The core is the intersection of all conjugates of the subgroup (The core of a subgroup).
Proof
By [L2], the equivariant isomorphism identifies the given action with the action on .
A group element fixes every point of exactly when it fixes every point of the equivariantly isomorphic coset set; by [L3] and [L4], the set of such elements is .
By [L1], the action is faithful exactly when this kernel is , proving both directions.
Depends on
- Left group actions, transitive actions, and faithful actions
- Every transitive $G$-set is equivariantly isomorphic to $G/G_x$ for any chosen point $x$
- Left multiplication on $G/H$ is transitive, has stabiliser $H$ at $H$, and has kernel $\operatorname{Core}_G(H)$
- The core $\operatorname{Core}_G(H)=\bigcap_{g\in G}gHg^{-1}$ of a subgroup
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: 37 results over 14 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
- P. Brosnan, Undergraduate Algebra Notes, 3.14: G-Sets (standard reference, not scraped)