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

The canonical semidirect decomposition is an internal direct product if and only if the defining action is trivial

Statement

The canonical factors of $N ⋊_{α} H$ form an internal direct product if and only if $α_{h} = {id}_{N}$ for every $h \in H$ . In that case $N ⋊_{α} H$ is the external direct product $N \times H$ .

Facts & Assumptions

Given: An external semidirect product $N ⋊_{α} H$ with its canonical factors $\overset{ˉ}{N}$ and $\overset{ˉ}{H}$ .

[L1]

The canonical factors have trivial intersection, multiply to the whole group, and satisfy $(1, h) (n, 1) (1, h)^{- 1} = (α_{h} (n), 1)$ (The canonical copy of $N$ is normal, the canonical copy of $H$ is a complement, and conjugation induces the action).

[L2]

The external direct product has coordinatewise multiplication (The external direct product $G \times H$ with componentwise multiplication).

[L3]

A subgroup $M \leq G$ is normal when $g M g^{- 1} = M$ for every $g \in G$ (Normal subgroup: invariance under conjugation).

Proof

technique · iff

1.1

[reverse] Suppose the action is trivial. The semidirect law becomes $(n, h) (n^{'}, h^{'}) = (n n^{'}, h h^{'})$ , which is the direct-product law from [L2].

L1L2

1.2

[forward] Suppose the canonical decomposition is an internal direct product, so $\overset{ˉ}{H}$ as well as $\overset{ˉ}{N}$ is normal. For $x \in \overset{ˉ}{N}$ and $y \in \overset{ˉ}{H}$ , normality gives $x y x^{- 1} y^{- 1} \in \overset{ˉ}{H}$ and also $x y x^{- 1} y^{- 1} = x (y x^{- 1} y^{- 1}) \in \overset{ˉ}{N}$ . Thus this commutator lies in $\overset{ˉ}{N} \cap \overset{ˉ}{H} = {1}$ by [L1], so $x$ and $y$ commute.

L1L3algebra

2.1

The conjugation formula in [L1] now gives $(α_{h} (n), 1) = (n, 1)$ for every $n, h$ . Hence every $α_{h}$ is the identity.

step 1.2L1∎

Depends on

Used by

The reflection complement in C₃ rtimes C₂≅ S₃ is not normal Counterexample
Dih(C₂× C₂) is the direct product (C₂× C₂)× C₂ Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 15 results over 10 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 (standard reference, not scraped)