TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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 semidirect-product multiplication makes $N \times H$ a group

Statement

Let $α : H \to Aut (N)$ be an action by automorphisms. The multiplication

$(n, h) (n^{'}, h^{'}) = (n α_{h} (n^{'}), h h^{'})$

makes $N \times H$ a group with identity $(1_{N}, 1_{H})$ and inverse

$(n, h)^{- 1} = (α_{h^{- 1}} (n^{- 1}), h^{- 1}) .$

Facts & Assumptions

Given: Groups $N, H$ and a homomorphism $α : H \to Aut (N)$ .

[L1]

The external semidirect-product multiplication is $(n, h) (n^{'}, h^{'}) = (n α_{h} (n^{'}), h h^{'})$ ( The external semidirect product $N ⋊_{α} H$ ).

[L2]

An action by automorphisms satisfies $α_{h h^{'}} = α_{h} \circ α_{h^{'}}$ and $α_{1} = {id}_{N}$ , with every $α_{h}$ an automorphism of $N$ (An action of a group $H$ on a group $N$ by automorphisms).

[L3]

A homomorphism preserves identities and inverses (A group homomorphism automatically satisfies $f (e) = e^{'}$ and $f (g^{- 1}) = f (g)^{- 1}$ , and $f (g^{n}) = f (g)^{n}$ for every $n \in Z$ ; for monoid homomorphisms preservation of the identity must be assumed).

Proof

technique · direct

1.1

For three pairs, multiplication in either parenthesisation gives $(n α_{h} (n^{'}) α_{h h^{'}} (n^{''}), h h^{'} h^{''})$ because $α_{h}$ is a homomorphism and $α_{h h^{'}} = α_{h} α_{h^{'}}$ . Thus the operation is associative.

L1L2algebra

1.2

Since $α_{1}$ is the identity and every $α_{h}$ preserves $1_{N}$ , the pair $(1_{N}, 1_{H})$ is a two-sided identity.

L1L2L3

2.1

Put $y = α_{h^{- 1}} (n^{- 1})$ . Then $(n, h) (y, h^{- 1}) = (n α_{h} (y), 1_{H}) = (1_{N}, 1_{H})$ and $(y, h^{- 1}) (n, h) = (y α_{h^{- 1}} (n), 1_{H}) = (1_{N}, 1_{H})$ . Hence the displayed pair is the two-sided inverse.

L1L2L3algebra∎

Depends on

Used by

Cited to discharge well-definedness by The external semidirect product N rtimes_α H.

Dependency tree · next 3 levels

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

The semidirect-product multiplication makes N×HN×H a group