LemmaStatement: AI-adaptedProof: 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.

The commutator pairing of an extraspecial $p$ -group has trivial radical

Statement

Let $P$ be an extraspecial $p$ -group with $Z (P) = ⟨ z ⟩$ and $V = P / Z (P)$ , and let $b_{z}$ be its commutator pairing. The radical of $b_{z}$ is trivial: if $\overset{ˉ}{x} \in V$ satisfies $b_{z} (\overset{ˉ}{x}, \overset{ˉ}{y}) = 0$ for every $\overset{ˉ}{y} \in V$ , then $\overset{ˉ}{x}$ is the identity of $V$ . Conversely the identity of $V$ pairs to zero with every element.

Facts & Assumptions

Given: An extraspecial $p$ -group $P$ with $Z (P) = ⟨ z ⟩$ , the quotient $V = P / Z (P)$ , and the commutator pairing $b_{z}$ .

[F1]

The commutator pairing of $P$ relative to $z$ is the map $b_{z} : V \times V \to F_{p}$ determined by $[x, y] = z^{b_{z} (\overset{ˉ}{x}, \overset{ˉ}{y})}$ , where $V = P / Z (P)$ (The commutator pairing of an extraspecial $p$ -group relative to a chosen generator of its centre).

[F2]

$Z (G) : = {z \in G : z g = g z for every g \in G}$ (The center $Z (G)$ of a group).

[F3]

The quotient group $G / N$ has the left cosets $g N$ as elements (The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ ).

[L1]

The commutator pairing is well defined on $V \times V$ , is $F_{p}$ -bilinear, and is alternating (The commutator pairing is well defined on the central quotient, is bilinear over $F_{p}$ , and is alternating).

[L2]

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).

Proof

technique · direct

1.1

Let $x \in P$ represent $\overset{ˉ}{x}$ and suppose $b_{z} (\overset{ˉ}{x}, \overset{ˉ}{y}) = 0$ for every $\overset{ˉ}{y} \in V$ . Since every element of $P$ represents some coset, this says $[x, y] = z^{0} = e$ for every $y \in P$ , that is $x y = y x$ for every $y \in P$ .

F1L1

2.1

Hence $x \in Z (P)$ , so $\overset{ˉ}{x} = x Z (P)$ is the identity coset of $V$ .

F2F3L2step 1.1

3.1

Conversely, if $\overset{ˉ}{x}$ is the identity of $V$ then $x \in Z (P)$ , so $[x, y] = e$ and $b_{z} (\overset{ˉ}{x}, \overset{ˉ}{y}) = 0$ for every $\overset{ˉ}{y}$ .

F1F2F3step 2.1∎

Remarks

Triviality of the radical, rather than merely its smallness, is exactly the statement that the centre is the whole kernel of the quotient map. It is what lets a single element of $V$ be detected by pairing it against the others, and it is used in that form by every counting argument below.

Depends on

Used by

Dependency tree · two levels

28 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

D. A. Craven, The Theory of p-Groups, §3.2 (standard reference, not scraped)
D. Kaur and A. Kulshrestha, Characters of real special 2-groups, §2 opening (standard reference, not scraped)

The commutator pairing of an extraspecial pp-group has trivial radical