TheoremStatement: AI-adaptedProof: 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.

Recognition theorem: $G = N H$ with $N ⊴ G$ , $N \cap H = 1$ exactly realises an external semidirect product

Statement

Let $N, H \leq G$ . The conditions

$N ⊴ G, G = N H, N \cap H = {1}$

hold if and only if both of the following hold: conjugation $α_{h} (n) = h n h^{- 1}$ restricts to an action $α : H \to Aut (N)$ , and the resulting map

$Φ : N ⋊_{α} H ⟶ G, (n, h) ⟼ n h$

is an isomorphism carrying the canonical factors onto $N$ and $H$ .

The first clause of the right-hand side is what makes $N ⋊_{α} H$ defined at all: without normality of $N$ , the map $α_{h}$ need not send $N$ into $N$ .

Facts & Assumptions

Given: Subgroups $N, H$ of a group $G$ .

[L1]

An internal semidirect product satisfies $N ⊴ G$ , $G = N H$ , and $N \cap H = {1}$ (An internal semidirect product and a complement to a normal subgroup).

[L2]

Conjugation is an automorphism; normality of $N$ makes conjugation by $H$ restrict to $N$ (Conjugation $x \mapsto g x g^{- 1}$ is an automorphism).

[L3]

The external semidirect product is a group ( The semidirect-product multiplication makes $N \times H$ a group).

[L4]

Its canonical factors have precisely the normality, product, intersection, and conjugation properties stated above (The canonical copy of $N$ is normal, the canonical copy of $H$ is a complement, and conjugation induces the action).

[L5]

An isomorphism is a bijective homomorphism (Group isomorphisms, automorphisms and the set $Aut (G)$ ).

Proof

technique · iff

1.1

[forward] Assume the three conditions in [L1]. By [L2], conjugation defines an action $α : H \to Aut (N)$ , so the domain of $Φ$ is a group by [L3].

L1L2L3

1.2

For $(n, h), (n^{'}, h^{'})$ one has

$Φ ((n, h) (n^{'}, h^{'})) = n (h n^{'} h^{- 1}) h h^{'} = n h n^{'} h^{'} = Φ (n, h) Φ (n^{'}, h^{'}),$

so $Φ$ is a homomorphism. It is surjective because $G = N H$ . [step 1.1, L1, algebra]

2.1

If $n h = n^{'} h^{'}$ , then $n^{- 1} n^{'} = h h^{' - 1} \in N \cap H$ , hence both sides are $1$ ; therefore $n = n^{'}$ and $h = h^{'}$ . Thus $Φ$ is injective, and step 1.2 makes it bijective and therefore an isomorphism by [L5].

step 1.2L1L5algebra

3.1

[reverse] Conversely, assume conjugation restricts to $α : H \to Aut (N)$ and that $Φ$ is such an isomorphism; the first assumption is what makes $N ⋊_{α} H$ , and hence $Φ$ , defined. Transport the canonical-factor properties from [L4] through $Φ$ . The images are $N, H$ , so the three conditions in [L1] hold.

L1L4L5∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 34 results over 15 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

Keith Conrad, Semidirect Products, Definition 3.1 and Theorem 4.1 (standard reference, not scraped)

Recognition theorem: G=NHG=NH with N⊴GN⊴G, N∩H=1N∩H=1 exactly realises an external semidirect product