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 conjugates of are in bijection with and, for finite , number
Statement
Let . The rule
is a well-defined bijection. If is finite, the number of distinct conjugates of is .
Facts & Assumptions
Given: A group and a subgroup .
Orbit-stabiliser identifies an orbit with the cosets of its stabilizer (Orbit-stabiliser: , , is a well-defined bijection).
The cardinality of a finite orbit is the index of its stabilizer (Orbit-stabiliser cardinality: whenever either side is finite, and for finite ).
The normalizer is (The normalizer of a subgroup).
The normalizer is a subgroup of ( and are subgroups of ).
Conjugation by each is an automorphism of (Conjugation is an automorphism).
Proof
Let act on the set of subgroups of by . By [L5], conjugation sends subgroups to subgroups, and the conjugation identities give the action laws.
The orbit of is its set of conjugates, while [L3] says that its stabilizer is , a subgroup by [L4].
Applying [L1] gives the displayed bijection, and [L2] gives the finite count .
Depends on
- Orbit-stabiliser: $G/G_x\to G\cdot x$, $gG_x\mapsto g\cdot x$, is a well-defined bijection
- Orbit-stabiliser cardinality: $|G\cdot x|=[G:G_x]$ whenever either side is finite, and $|G|=|G_x|\,|G\cdot x|$ for finite $G$
- The normalizer $N_G(H)=\{g\in G:gHg^{-1}=H\}$ of a subgroup
- $C_G(x)$ and $N_G(H)$ are subgroups of $G$
- Conjugation $x\mapsto gxg^{-1}$ is an automorphism
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 43 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, Corollary 3.110 (standard reference, not scraped)