TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

Splitting lemma for groups: a section, a complement, and a semidirect-product decomposition are equivalent

Statement

For a short exact sequence

$1 \to N \to^{i} G \to^{π} H \to 1,$

the following are equivalent:

there is a homomorphic section $s : H \to G$ of $π$ ;
$\ker π$ has a complement $K$ in $G$ ;
$G$ is isomorphic to $(\ker π) ⋊ H$ by an isomorphism compatible with the injection and quotient maps.

For a section $s$ , the action is $h \cdot n = s (h) n s (h)^{- 1}$ .

Facts & Assumptions

Given: The displayed short exact sequence.

[L1]

A section satisfies $π s = {id}_{H}$ , and a complement $K$ satisfies $G = (\ker π) K$ and $(\ker π) \cap K = {1}$ (Group extensions, sections, complements, and split extensions).

[L2]

An internal semidirect product is isomorphic to the external product defined by its conjugation action ( Recognition theorem: $G = N H$ with $N ⊴ G$ , $N \cap H = 1$ exactly realises an external semidirect product).

[L3]

The first isomorphism theorem identifies the quotient by a kernel with the image (First isomorphism theorem for groups: $G / \ker f ≅ im f$ ).

[L4]

A homomorphism is injective exactly when its kernel is trivial (A group homomorphism is injective if and only if its kernel is trivial).

Proof

technique · iff

1.1

Suppose $s$ is a section and put $K = s (H)$ . If $s (h) \in \ker π$ , then $h = π s (h) = 1$ , so $s$ is injective by [L4] and $K \cap \ker π = {1}$ .

L1L4

1.2

Conversely, suppose $K$ is a complement. The restriction $π ∣_{K}$ is injective because its kernel is $K \cap \ker π$ , and it is surjective because $G = (\ker π) K$ and $π$ kills the first factor. Thus it is an isomorphism by [L3] and [L4].

L1L3L4

2.1

For $g \in G$ , put $h = π (g)$ . Then $g s (h)^{- 1} \in \ker π$ , so $g \in (\ker π) K$ . Hence $K$ is a complement, and [L2] gives the compatible semidirect-product decomposition with the stated conjugation action.

step 1.1L1L2

3.1

The inverse $s = (π ∣_{K})^{- 1} : H \to K ↪ G$ is a homomorphic section. Finally, any compatible external semidirect decomposition supplies its canonical complement and hence a section by the same construction.

step 1.2L1L2∎

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: 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

J. S. Milne, Group Theory (standard reference, not scraped)