Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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 group extension induces a well-defined outer action on its kernel

Statement

Every group extension

1→N→iE→πQ→1

determines a homomorphism

ωE:Q→Out⁡(N)

that depends only on the extension up to equivalence with fixed kernel and fixed quotient.

Facts & Assumptions

Given: The displayed group extension.

[L1]

The outer automorphism group is the quotient Aut⁡(N)/Inn⁡(N) ( The outer automorphism group Out⁡(G)=Aut⁡(G)/Inn⁡(G)).

[L2]

Conjugation by an element of a group is an automorphism (Conjugation x↦gxg−1 is an automorphism).

[L3]

Equivalence of extensions fixes the chosen copies of the kernel and quotient (Equivalence of group extensions with fixed kernel and fixed quotient).

Proof

technique · direct
1.1givenL1L2choose

For q∈Q, choose x∈E with π(x)=q. Since i(N)=ker⁡π is normal, conjugation by x restricts to an automorphism of i(N), hence of N, by [L2]. Let ωE(q) be its class in Out⁡(N) from [L1].

2.1L1step 1.1algebra

If x′=xi(n) is another lift of q, then for m∈N, x′i(m)x′−1=x i(nmn−1) x−1. Thus the automorphism from x′ differs from the automorphism from x by the inner automorphism of N defined by n. So step 1.1 is independent of the chosen lift as an element of Out⁡(N).

3.1L1step 2.1algebra

If q1,q2∈Q are lifted by x1,x2∈E, then x1x2 lifts q1q2, and conjugation by x1x2 is the composite of conjugation by x1 and by x2. Passing to classes modulo inner automorphisms with [L1], ωE(q1q2)=ωE(q1)ωE(q2). So ωE is a homomorphism.

4.1L3step 1.1step 3.1∎

If φ:E→E′ is an equivalence of extensions as in [L3], then φ identifies the chosen copy of N with itself and carries lifts of q in E to lifts of q in E′. Therefore the conjugation automorphisms correspond and define the same class in Out⁡(N). Hence ωE depends only on the extension class.

Depends on

Used by

Dependency tree · two levels

9 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