LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

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 complement determines the conjugation action on the kernel

Statement

Let

$1 \to N \overset{i}{\to} E \overset{π}{\to} Q \to 1$

be a split group extension, and let $C \leq E$ be a complement to $i (N)$ . Then $π ∣_{C} : C \to Q$ is an isomorphism, and the formula

$q \cdot n = i^{- 1} ⁣ (c i (n) c^{- 1}) for the unique c \in C with π (c) = q$

defines an action of $Q$ on $N$ by automorphisms.

Facts & Assumptions

Given: The displayed split extension and a complement $C \leq E$ to $i (N)$ .

[L1]

In a split extension, a complement to the kernel is equivalent to a semidirect-product model, and the quotient map restricts to an isomorphism from the complement onto the quotient (A group extension splits exactly when it has a complement or a compatible semidirect-product model, and a kernel retraction forces a direct product).

[L2]

Conjugation by a group element is an automorphism of the group (Conjugation $x \mapsto g x g^{- 1}$ is an automorphism).

Proof

technique · direct

1.1

By [L1], the restriction $π ∣_{C} : C \to Q$ is an isomorphism. Hence for each $q \in Q$ there is a unique $c \in C$ with $π (c) = q$ , so the displayed formula is well defined.

givenL1

2.1

For each $q \in Q$ , conjugation by the corresponding $c$ restricts to an automorphism of $i (N)$ by [L2], because $i (N) ⊴ E$ and so $c i (N) c^{- 1} = i (N)$ . Transporting that automorphism across the isomorphism $i : N \to i (N)$ gives the displayed automorphism of $N$ . Thus the rule lands in $Aut (N)$ .

L2step 1.1

3.1

If $q_{1}, q_{2} \in Q$ correspond to $c_{1}, c_{2} \in C$ , then $q_{1} q_{2}$ corresponds to $c_{1} c_{2} \in C$ because $π ∣_{C}$ is a homomorphism. Conjugation by $c_{1} c_{2}$ is the composite of conjugation by $c_{1}$ and conjugation by $c_{2}$ ; transporting across $i$ gives $(q_{1} q_{2}) \cdot n = q_{1} \cdot (q_{2} \cdot n)$ , and $1_{Q} \cdot n = n$ . So this is an action of $Q$ on $N$ by automorphisms.

L1step 2.1algebra∎

Depends on

Used by

A split extension is a direct product exactly when its complement centralizes the kernel Proposition

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 (standard reference, not scraped)