Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26
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.

An automorphism fixing the centre pointwise induces a pairing-preserving automorphism of the central quotient, with kernel the inner automorphisms

Statement

Let P be an extraspecial p-group with Z(P)=z and commutator pairing bz, and let αAut(P) fix Z(P) pointwise.

Then α induces an automorphism αˉ of P/Z(P) satisfying

bz(αˉ(xˉ),αˉ(yˉ))=bz(xˉ,yˉ)

for all xˉ,yˉP/Z(P). The kernel of the action of the centre-fixing automorphism subgroup on P/Z(P) is Inn(P).

Facts & Assumptions

Given: An extraspecial p-group P with Z(P)=z, its commutator pairing bz, and an automorphism α fixing Z(P) pointwise.

[F1]

For an extraspecial p-group P with Z(P)=z, the commutator pairing is the map bz(xˉ,yˉ)Z/p determined by [x,y]=zbz(xˉ,yˉ) (The commutator pairing of an extraspecial p-group relative to a chosen generator of its centre).

[L1]

For a finite p-group P the following are equivalent: P is extraspecial; P is nonabelian, Z(P)=p and P/Z(P) is elementary abelian; P is nonabelian and Z(P)=P=Φ(P) has order p (Three equivalent descriptions of an extraspecial p-group).

[L2]

Every extraspecial p-group has order p1+2n for some n1 (An extraspecial p-group has order p1+2n for some n1).

[L3]

For an extraspecial p-group of order p1+2n, an automorphism acting trivially on its Frattini quotient is inner (An automorphism of an extraspecial p-group acting trivially on its Frattini quotient is inner).

[L4]

Group isomorphisms, automorphisms and the set Aut(G). (Group isomorphisms, automorphisms and the set Aut(G)).

[L5]

Inner automorphisms and Inn(G). (Inner automorphisms and Inn(G)).

Proof

technique · direct
1.1

Because α fixes Z(P) pointwise, it sends each coset xZ(P) to α(x)Z(P); this is well defined, so α induces an automorphism αˉ of P/Z(P). Also [α(x),α(y)]=α([x,y])=α(zbz(xˉ,yˉ))=zbz(xˉ,yˉ), so bz(αˉ(xˉ),αˉ(yˉ))=bz(xˉ,yˉ) for all xˉ,yˉP/Z(P).

F1L4L6
2.1

If αˉ is the identity on P/Z(P), then α acts trivially on the central quotient. Since P is extraspecial, [L1] gives Φ(P)=Z(P) and [L2] supplies the order hypothesis of [L3], so α acts trivially on the Frattini quotient and is inner. Conversely, every inner automorphism cg(x)=gxg1 acts trivially on P/Z(P) because gxg1x1=[g,x][P,P]=Z(P) by [L1] and [L6]. Hence the kernel of the action on P/Z(P) is exactly Inn(P).

L1L2L3L5L6step 1.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 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