TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

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 imprimitive action embeds modulo its kernel in an imprimitive wreath product

Statement

Let $G$ act transitively on $Ω$ , and let $B \subseteq Ω$ be a nontrivial block. Put $Σ : = {g \cdot B : g \in G}, G_{B} : = {g \in G : g \cdot B = B} .$ Let $K$ be the permutation group induced by $G$ on $Σ$ , and let $H$ be the permutation group induced by $G_{B}$ on $B$ .

Choose for each $C \in Σ$ an element $t_{C} \in G$ with $t_{C} \cdot B = C, t_{B} = e .$ Then there is a homomorphism $Φ : G ⟶ H ≀_{Σ} K$ whose kernel is exactly the kernel of the given action on $Ω$ .

In particular, if the action of $G$ on $Ω$ is faithful, then $Φ$ is an embedding.

Facts & Assumptions

Given: A transitive action of $G$ on $Ω$ , a block $B \subseteq Ω$ , the block system $Σ : = {g \cdot B : g \in G}$ , and a choice of $t_{C} \in G$ with $t_{C} \cdot B = C$ and $t_{B} = e$ .

[L1]

A block $B$ satisfies: for every $g \in G$ , either $g \cdot B = B$ or $(g \cdot B) \cap B = \emptyset$ (Blocks and block systems for a group action).

[L2]

The imprimitive wreath product $H ≀_{Σ} K$ is the semidirect product $H^{Σ} ⋊ K$ acting on $B \times Σ$ by $(f, k) \cdot (b, C) = (f (k \cdot C) \cdot b, k \cdot C) .$ (The imprimitive wreath product of permutation groups).

Proof

technique · constructive

1.1

For each $g \in G$ , let $k_{g}$ be the permutation of $Σ$ induced by $g$ , so $k_{g} (C) = g \cdot C$ . For each $C \in Σ$ , the element $t_{C}^{- 1} g t_{g^{- 1} \cdot C}$ stabilizes $B$ setwise because $t_{C}^{- 1} g t_{g^{- 1} \cdot C} \cdot B = t_{C}^{- 1} g \cdot (g^{- 1} \cdot C) = t_{C}^{- 1} \cdot C = B .$ Let $f_{g} (C) \in H$ be the induced permutation of $B$ defined by this element.

L1construct

2.1

Define $Φ (g) : = (f_{g}, k_{g})$ . For $C \in Σ$ , the function component of $Φ (g) Φ (h)$ at $C$ is $f_{g} (C) f_{h} (g^{- 1} \cdot C)$ , while $t_{C}^{- 1} g h t_{(g h)^{- 1} \cdot C} = (t_{C}^{- 1} g t_{g^{- 1} \cdot C}) (t_{g^{- 1} \cdot C}^{- 1} h t_{h^{- 1} g^{- 1} \cdot C}),$ so it induces the same permutation of $B$ as $f_{g h} (C)$ . Also $k_{g h} = k_{g} k_{h}$ . Hence $Φ (g h) = Φ (g) Φ (h)$ .

step 1.1L2algebra

3.1

Identify $Ω$ with $B \times Σ$ by $Ψ (b, C) : = t_{C} \cdot b$ . Then for every $g \in G$ one has $Ψ (Φ (g) \cdot (b, C)) = t_{g \cdot C} \cdot (f_{g} (g \cdot C) \cdot b) = g \cdot (t_{C} \cdot b) = g \cdot Ψ (b, C) .$ So $Φ (g) = 1$ exactly when $g$ fixes every point of $Ω$ .

step 1.1step 2.1L2algebra

4.1

Step 3.1 shows that $\ker Φ$ is the kernel of the given action. Therefore a faithful action makes $\ker Φ = 1$ , so in that case $Φ$ is an embedding into $H ≀_{Σ} K$ .

step 3.1discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. S. Milne, Group Theory, Chapter 4 (standard reference, not scraped)
P. J. Cameron, Permutation Groups, Chapter 2 (standard reference, not scraped)