Alphabeta Math
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→N→iE→πQ→1

be a split group extension, and let C≤E be a complement to i(N). Then π∣C:C→Q is an isomorphism, and the formula

q⋅n=i−1 ⁣(c i(n) c−1)for the unique c∈C with π(c)=q

defines an action of Q on N by automorphisms.

Facts & Assumptions

Given: The displayed split extension and a complement C≤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↦gxg−1 is an automorphism).

Proof

technique · direct
1.1givenL1

By [L1], the restriction π∣C:C→Q is an isomorphism. Hence for each q∈Q there is a unique c∈C with π(c)=q, so the displayed formula is well defined.

2.1L2step 1.1

For each q∈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→i(N) gives the displayed automorphism of N. Thus the rule lands in Aut⁡(N).

3.1L1step 2.1algebra∎

If q1,q2∈Q correspond to c1,c2∈C, then q1q2 corresponds to c1c2∈C because π∣C is a homomorphism. Conjugation by c1c2 is the composite of conjugation by c1 and conjugation by c2; transporting across i gives (q1q2)⋅n=q1⋅(q2⋅n), and 1Q⋅n=n. So this is an action of Q on N by automorphisms.

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