Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck 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∈H. In that case N⋊αH is the external direct product N×H.

Facts & Assumptions

Given: An external semidirect product N⋊αH with its canonical factors Nˉ and 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×H with componentwise multiplication).

[L3]

A subgroup M≤G is normal when gMg−1=M for every g∈G (Normal subgroup: invariance under conjugation).

Proof

technique · iff
1.1L1L2

[reverse] Suppose the action is trivial. The semidirect law becomes (n,h)(n′,h′)=(nn′,hh′), which is the direct-product law from [L2].

1.2L1L3algebra

[forward] Suppose the canonical decomposition is an internal direct product, so Hˉ as well as Nˉ is normal. For x∈Nˉ and y∈Hˉ, normality gives xyx−1y−1∈Hˉ and also xyx−1y−1=x(yx−1y−1)∈Nˉ. Thus this commutator lies in Nˉ∩Hˉ={1} by [L1], so x and y commute.

2.1step 1.2L1∎

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

Depends on

Used by

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